case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
constructor
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
intro H x
case mp.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y)⁻¹
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x
case mp.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
this : ↑(algebraMap R K) y ≠ 0
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y)⁻¹
case mp.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y)⁻¹
have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
case mp.intro.intro.intro.intro.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : ↑(algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) (x * s))⁻¹

case mp.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : ↑(algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) (y * s) / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) (y * s) / ↑(algebraMap R K) y)⁻¹
case mp.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
this : ↑(algebraMap R K) y ≠ 0
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) y)⁻¹
obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
no goals
case mp.intro.intro.intro.intro.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : ↑(algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) x / ↑(algebraMap R K) (x * s))⁻¹
exact Or.inr
  ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : ↑(algebraMap R K) (x * s) ≠ 0
⊢ ↑(algebraMap R K) s * (↑(algebraMap R K) x / ↑(algebraMap R K) (x * s)) = 1
rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]
no goals
case mp.intro.intro.intro.intro.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : ↑(algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R (↑(algebraMap R K) (y * s) / ↑(algebraMap R K) y) ∨
    IsLocalization.IsInteger R (↑(algebraMap R K) (y * s) / ↑(algebraMap R K) y)⁻¹
exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : ↑(algebraMap R K) y ≠ 0
s : R
⊢ ↑(algebraMap R K) s = ↑(algebraMap R K) (y * s) / ↑(algebraMap R K) y
rwa [eq_div_iff, map_mul, mul_comm]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
intro H
case mpr.cond'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ∀ (a b : R), ∃ c, a * c = b ∨ b * c = a
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R
constructor
case mpr.cond'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a
case mpr.cond'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ∀ (a b : R), ∃ c, a * c = b ∨ b * c = a
intro a b
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
⊢ ∃ c, a * c = b ∨ b * c = a
case mpr.cond'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a
by_cases ha : a = 0
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ c, a * c = b ∨ b * c = a
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
⊢ ∃ c, a * c = b ∨ b * c = a
by_cases hb : b = 0
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
hb : ¬b = 0
ha : ↑(algebraMap R K) a ≠ 0
⊢ ∃ c, a * c = b ∨ b * c = a
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ c, a * c = b ∨ b * c = a
replace ha := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr ha
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
⊢ ∃ c, a * c = b ∨ b * c = a
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
hb : ¬b = 0
ha : ↑(algebraMap R K) a ≠ 0
⊢ ∃ c, a * c = b ∨ b * c = a
replace hb := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr hb
case neg.inl.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : ↑(algebraMap R K) c = ↑(algebraMap R K) a / ↑(algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a

case neg.inr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : ↑(algebraMap R K) c = (↑(algebraMap R K) a / ↑(algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
⊢ ∃ c, a * c = b ∨ b * c = a
obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
b : R
⊢ ∃ c, 0 * c = b ∨ b * c = 0
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : a = 0
⊢ ∃ c, a * c = b ∨ b * c = a
subst ha
no goals
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
b : R
⊢ ∃ c, 0 * c = b ∨ b * c = 0
exact ⟨0, Or.inr <| MulZeroClass.mul_zero b⟩
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
ha : ¬a = 0
⊢ ∃ c, a * c = 0 ∨ 0 * c = a
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a
subst hb
no goals
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
ha : ¬a = 0
⊢ ∃ c, a * c = 0 ∨ 0 * c = a
exact ⟨0, Or.inl <| MulZeroClass.mul_zero a⟩
case neg.inl.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : b * c = a
⊢ ∃ c, a * c = b ∨ b * c = a
case neg.inl.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : ↑(algebraMap R K) c = ↑(algebraMap R K) a / ↑(algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a
rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
no goals
case neg.inl.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : b * c = a
⊢ ∃ c, a * c = b ∨ b * c = a
exact ⟨c, Or.inr e⟩
case neg.inr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : a * c = b
⊢ ∃ c, a * c = b ∨ b * c = a
case neg.inr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : ↑(algebraMap R K) c = (↑(algebraMap R K) a / ↑(algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a
rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e
no goals
case neg.inr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ↑(algebraMap R K) a ≠ 0
hb : ↑(algebraMap R K) b ≠ 0
c : R
e : a * c = b
⊢ ∃ c, a * c = b ∨ b * c = a
exact ⟨c, Or.inl e⟩