-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {x : A} {p : K[X]}
    (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : (x⁻¹ : L) ∈ A

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ (aeval ↑x) p = 0

Tactic:
rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]

Result:
no goals

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

Tactic:
have : aeval (x : L) p = 0 := by rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)

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

Tactic:
rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * (aeval ↑x) p.divX) = (algebraMap K L) (-p.coeff 0)⁻¹ * ↑((aeval x) p.divX)

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

Tactic:
simp only [aeval_coe, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, coe_toSubsemiring,
  coe_algebraMap]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)) = (algebraMap K L) (-p.coeff 0)⁻¹ * ↑((aeval x) p.divX)

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
  rw [this]
  exact A.smul_mem (aeval x _).2 _

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)

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

Tactic:
rw [map_inv₀, map_neg, inv_neg, neg_mul]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)
⊢ (↑x)⁻¹ ∈ A

Tactic:
rw [this]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)
⊢ (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX) ∈ A

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)
⊢ (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX) ∈ A

Tactic:
exact A.smul_mem (aeval x _).2 _

Result:
no goals