-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem exists_eq_spanSingleton_mul (I : FractionalIdeal R₁⁰ K) :
    ∃ (a : R₁) (aI : Ideal R₁), a ≠ 0 ∧ I = spanSingleton R₁⁰ (algebraMap R₁ K a)⁻¹ * aI

Proof state:
case intro.intro.refine_2.intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
y : K
hy : y ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * y ∈ I

Tactic:
obtain ⟨x', hx', rfl⟩ := (mem_coeIdeal _).mp hy

Result:
case intro.intro.refine_2.intro.intro.intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx' : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I

Proof state:
case intro.intro.refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Tactic:
obtain ⟨x', hx'⟩ := ha x hx

Result:
case intro.intro.refine_1.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = a_inv • x
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Proof state:
case intro.intro.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ (∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y') →
    x ∈ I

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case intro.intro.refine_2.intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
y : K
hy : y ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * y ∈ I

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Tactic:
obtain ⟨a_inv, nonzero, ha⟩ := I.isFractional

Result:
case intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Proof state:
case intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Tactic:
have nonzero := mem_nonZeroDivisors_iff_ne_zero.mp nonzero

Result:
case intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Proof state:
case intro.intro.refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ x ∈ I →
    ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Tactic:
intro hx

Result:
case intro.intro.refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Proof state:
case intro.intro.refine_1.intro.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ x = ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x'

Tactic:
rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]

Result:
no goals

Proof state:
case intro.intro.refine_2.intro.intro.intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx' : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I

Tactic:
obtain ⟨y', hy', hx'⟩ := mem_singleton_mul.mp hx'

Result:
case intro.intro.refine_2.intro.intro.intro.intro.intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (Algebra.linearMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I