-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem inv_eq_of_root_of_coeff_zero_ne_zero {x : L} {p : K[X]} (aeval_eq : aeval x p = 0)
    (coeff_zero_ne : p.coeff 0 ≠ 0) : x⁻¹ = -(aeval x (divX p) / algebraMap _ _ (p.coeff 0))

Proof state:
case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (algebraMap K L) 0

Tactic:
rw [RingHom.map_zero]

Result:
case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = 0

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ x⁻¹ = -((aeval x) p.divX / (algebraMap K L) (p.coeff 0))

Tactic:
convert inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
  (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1

Result:
case h.e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (algebraMap K L) 0

Proof state:
case h.e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

Tactic:
rw [aeval_eq, zero_sub, div_neg]

Result:
no goals

Proof state:
case h.e'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) p

Tactic:
conv_rhs => rw [← divX_mul_X_add p]

Result:
case h.e'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) (p.divX * X + C (p.coeff 0))

Proof state:
case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = 0

Tactic:
convert aeval_eq

Result:
case h.e'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) p

Proof state:
case h.e'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) (p.divX * X + C (p.coeff 0))

Tactic:
rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]

Result:
no goals