-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem span_singleton_annIdealGenerator (a : A) :
    Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]

Result:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (C (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹)

Proof state:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹ ≠ 0

Tactic:
apply inv_eq_zero.not.mpr

Result:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬(IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
by_cases h : annIdealGenerator 𝕜 a = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Proof state:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬(IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff = 0

Tactic:
apply Polynomial.leadingCoeff_eq_zero.not.mpr

Result:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬IsPrincipal.generator (annIdeal 𝕜 a) = 0

Proof state:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (C (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹)

Tactic:
apply Polynomial.isUnit_C.mpr

Result:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]

Result:
no goals

Proof state:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹

Tactic:
apply IsUnit.mk0

Result:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹ ≠ 0

Proof state:
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬IsPrincipal.generator (annIdeal 𝕜 a) = 0

Tactic:
apply (mul_ne_zero_iff.mp h).1

Result:
no goals