case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
ne_zero : p ≠ 0
aeval_eq : ↑(aeval ↑x) p = 0
⊢ (↑x)⁻¹ ∈ A
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
hx : _root_.IsAlgebraic K ↑x
⊢ (↑x)⁻¹ ∈ A
obtain ⟨p, ne_zero, aeval_eq⟩ := hx
case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
ne_zero : p ≠ 0
aeval_eq : ↑(aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A
case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
ne_zero : p ≠ 0
aeval_eq : ↑(aeval ↑x) p = 0
⊢ (↑x)⁻¹ ∈ A
rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq
case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
ne_zero : p ≠ 0
aeval_eq : ↑(aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A
revert ne_zero aeval_eq
case intro.intro.refine'_1
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ 0 ≠ 0 → ↑(aeval x) 0 = 0 → (↑x)⁻¹ ∈ A

case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    coeff p 0 = 0 →
      a ≠ 0 → (p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + ↑C a ≠ 0 → ↑(aeval x) (p + ↑C a) = 0 → (↑x)⁻¹ ∈ A

case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → ↑(aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
case intro.intro
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
refine' p.recOnHorner _ _ _
case intro.intro.refine'_1
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
h : 0 ≠ 0
⊢ ↑(aeval x) 0 = 0 → (↑x)⁻¹ ∈ A
case intro.intro.refine'_1
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ 0 ≠ 0 → ↑(aeval x) 0 = 0 → (↑x)⁻¹ ∈ A
intro h
no goals
case intro.intro.refine'_1
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
h : 0 ≠ 0
⊢ ↑(aeval x) 0 = 0 → (↑x)⁻¹ ∈ A
contradiction
case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
a : K
hp : coeff p 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + ↑C a ≠ 0
aeval_eq : ↑(aeval x) (p + ↑C a) = 0
⊢ (↑x)⁻¹ ∈ A
case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    coeff p 0 = 0 →
      a ≠ 0 → (p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + ↑C a ≠ 0 → ↑(aeval x) (p + ↑C a) = 0 → (↑x)⁻¹ ∈ A
intro p a hp ha _ih _ne_zero aeval_eq
case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
a : K
hp : coeff p 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + ↑C a ≠ 0
aeval_eq : ↑(aeval x) (p + ↑C a) = 0
⊢ coeff (p + ↑C a) 0 ≠ 0
case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
a : K
hp : coeff p 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + ↑C a ≠ 0
aeval_eq : ↑(aeval x) (p + ↑C a) = 0
⊢ (↑x)⁻¹ ∈ A
refine' A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq _
no goals
case intro.intro.refine'_2
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
a : K
hp : coeff p 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + ↑C a ≠ 0
aeval_eq : ↑(aeval x) (p + ↑C a) = 0
⊢ coeff (p + ↑C a) 0 ≠ 0
rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) (p * X) = 0
⊢ (↑x)⁻¹ ∈ A
case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → ↑(aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
intro p hp ih _ne_zero aeval_eq
case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) p = 0 ∨ x = 0
⊢ (↑x)⁻¹ ∈ A
case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) (p * X) = 0
⊢ (↑x)⁻¹ ∈ A
rw [AlgHom.map_mul, aeval_X, mul_eq_zero] at aeval_eq
case intro.intro.refine'_3.inl
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A

case intro.intro.refine'_3.inr
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A
case intro.intro.refine'_3
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) p = 0 ∨ x = 0
⊢ (↑x)⁻¹ ∈ A
cases' aeval_eq with aeval_eq x_eq
no goals
case intro.intro.refine'_3.inl
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : ↑(aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A
exact ih hp aeval_eq
case intro.intro.refine'_3.inr
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A
case intro.intro.refine'_3.inr
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A
rw [x_eq, Subalgebra.coe_zero, inv_zero]
no goals
case intro.intro.refine'_3.inr
R : Type ?u.864898
S : Type ?u.864901
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → ↑(aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A
exact A.zero_mem