case h.e'_3
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ -(↑(aeval x) (divX p) / ↑(algebraMap K L) (coeff p 0)) =
    ↑(aeval x) (divX p) / (↑(aeval x) p - ↑(algebraMap K L) (coeff p 0))

case convert_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(algebraMap K L) 0
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ x⁻¹ = -(↑(aeval x) (divX p) / ↑(algebraMap K L) (coeff p 0))
convert inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
  (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
case convert_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = 0
case convert_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(algebraMap K L) 0
rw [RingHom.map_zero]
case h.e'_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(aeval x) p
case convert_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = 0
convert aeval_eq
case h.e'_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(aeval x) (divX p * X + ↑C (coeff p 0))
case h.e'_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(aeval x) p
conv_rhs => rw [← divX_mul_X_add p]
no goals
case h.e'_2
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
h : ↑(aeval x) (divX p) = 0
⊢ ↑(algebraMap K L) (coeff p 0) = ↑(aeval x) (divX p * X + ↑C (coeff p 0))
rw [AlgHom.map_add, AlgHom.map_mul, h, MulZeroClass.zero_mul, zero_add, aeval_C]
no goals
case h.e'_3
R : Type ?u.658329
S : Type ?u.658332
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ -(↑(aeval x) (divX p) / ↑(algebraMap K L) (coeff p 0)) =
    ↑(aeval x) (divX p) / (↑(aeval x) p - ↑(algebraMap K L) (coeff p 0))
rw [aeval_eq, zero_sub, div_neg]