[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ IsAlgebraic S ↔ Algebra.IsAlgebraic R { x // x ∈ S }
[PROOFSTEP]
delta Algebra.IsAlgebraic Subalgebra.IsAlgebraic
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : A), x ∈ S → _root_.IsAlgebraic R x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
[PROOFSTEP]
rw [Subtype.forall']
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : { a // a ∈ S }), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
[PROOFSTEP]
refine' forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl _
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
have h : Function.Injective S.val := Subtype.val_injective
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
conv_rhs => rw [← h.eq_iff, AlgHom.map_zero]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
| ↑(aeval x) p = 0
[PROOFSTEP]
rw [← h.eq_iff, AlgHom.map_zero]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
| ↑(aeval x) p = 0
[PROOFSTEP]
rw [← h.eq_iff, AlgHom.map_zero]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
| ↑(aeval x) p = 0
[PROOFSTEP]
rw [← h.eq_iff, AlgHom.map_zero]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(val S) (↑(aeval x) p) = 0
[PROOFSTEP]
rw [← aeval_algHom_apply, S.val_apply]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ IsAlgebraic R A ↔ Subalgebra.IsAlgebraic ⊤
[PROOFSTEP]
delta Algebra.IsAlgebraic Subalgebra.IsAlgebraic
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ (∀ (x : A), _root_.IsAlgebraic R x) ↔ ∀ (x : A), x ∈ ⊤ → _root_.IsAlgebraic R x
[PROOFSTEP]
simp only [Algebra.mem_top, forall_prop_of_true, iff_self_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ IsAlgebraic R x ↔ ¬Function.Injective ↑(aeval x)
[PROOFSTEP]
simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
x : R
⊢ ↑(aeval (↑(algebraMap R A) x)) (X - ↑C x) = 0
[PROOFSTEP]
rw [_root_.map_sub, aeval_X, aeval_C, sub_self]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
⊢ IsAlgebraic R 1
[PROOFSTEP]
rw [← _root_.map_one (algebraMap R A)]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
⊢ IsAlgebraic R (↑(algebraMap R A) 1)
[PROOFSTEP]
exact isAlgebraic_algebraMap 1
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R ↑n
[PROOFSTEP]
rw [← map_natCast (_ : R →+* A) n]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R (↑?m.103292 ↑n)
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
n : ℕ
⊢ R →+* A
[PROOFSTEP]
exact isAlgebraic_algebraMap (Nat.cast n)
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ↑n
[PROOFSTEP]
rw [← _root_.map_intCast (algebraMap R A)]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R (↑(algebraMap R A) ↑n)
[PROOFSTEP]
exact isAlgebraic_algebraMap (Int.cast n)
[GOAL]
R✝ : Type u
S : Type u_1
A✝ : Type v
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S
inst✝⁷ : Ring A✝
inst✝⁶ : Algebra R✝ A✝
inst✝⁵ : Algebra R✝ S
inst✝⁴ : Algebra S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n
[PROOFSTEP]
rw [← map_ratCast (algebraMap R A)]
[GOAL]
R✝ : Type u
S : Type u_1
A✝ : Type v
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S
inst✝⁷ : Ring A✝
inst✝⁶ : Algebra R✝ A✝
inst✝⁵ : Algebra R✝ S
inst✝⁴ : Algebra S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R (↑(algebraMap R A) ↑n)
[PROOFSTEP]
exact isAlgebraic_algebraMap (Rat.cast n)
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
x✝ : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval a) f = 0
⊢ ↑(aeval (↑(algebraMap S A) a)) f = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, hf₂, map_zero]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : ↑(aeval a) p = 0
⊢ ↑(aeval (↑f a)) p = 0
[PROOFSTEP]
rw [aeval_algHom, f.comp_apply, ha, map_zero]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ IsAlgebraic R b
[PROOFSTEP]
convert ← isAlgebraic_algHom_of_isAlgebraic e.toAlgHom (h _)
[GOAL]
case h.e'_6
R : Type u
S : Type u_1
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ ↑↑e ?m.164018 = b
R : Type u
S : Type u_1
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ A
[PROOFSTEP]
refine e.apply_symm_apply ?_
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ↑(algebraMap S A)
x✝ : IsAlgebraic R (↑(algebraMap S A) a)
p : R[X]
hp0 : p ≠ 0
hp : ↑(aeval (↑(algebraMap S A) a)) p = 0
⊢ ↑(algebraMap S A) (↑(aeval a) p) = ↑(algebraMap S A) 0
[PROOFSTEP]
rwa [map_zero, ← aeval_algebraMap_apply]
[GOAL]
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
⊢ IsAlgebraic R r
[PROOFSTEP]
obtain ⟨p, p_nonzero, hp⟩ := ht
[GOAL]
case intro.intro
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ IsAlgebraic R r
[PROOFSTEP]
refine ⟨Polynomial.expand _ n p, ?_, ?_⟩
[GOAL]
case intro.intro.refine_1
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(expand R n) p ≠ 0
[PROOFSTEP]
rwa [Polynomial.expand_ne_zero hn]
[GOAL]
case intro.intro.refine_2
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(aeval r) (↑(expand R n) p) = 0
[PROOFSTEP]
rwa [Polynomial.expand_aeval n p r]
[GOAL]
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x
[PROOFSTEP]
refine' ⟨_, IsIntegral.isAlgebraic K⟩
[GOAL]
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x → IsIntegral K x
[PROOFSTEP]
rintro ⟨p, hp, hpx⟩
[GOAL]
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ IsIntegral K x
[PROOFSTEP]
refine' ⟨_, monic_mul_leadingCoeff_inv hp, _⟩
[GOAL]
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap K A) x (p * ↑C (leadingCoeff p)⁻¹) = 0
[PROOFSTEP]
rw [← aeval_def, AlgHom.map_mul, hpx, zero_mul]
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ↑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : ↑(aeval x) p = 0
⊢ map (algebraMap R S) p ≠ 0
[PROOFSTEP]
rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ↑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : ↑(aeval x) p = 0
⊢ ↑(aeval x) (map (algebraMap R S) p) = 0
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing A
inst✝³ : Algebra K L
inst✝² : Algebra L A
inst✝¹ : Algebra K A
inst✝ : IsScalarTower K L A
L_alg : IsAlgebraic K L
A_alg : IsAlgebraic L A
⊢ IsAlgebraic K A
[PROOFSTEP]
simp only [IsAlgebraic, isAlgebraic_iff_isIntegral] at L_alg A_alg ⊢
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing A
inst✝³ : Algebra K L
inst✝² : Algebra L A
inst✝¹ : Algebra K A
inst✝ : IsScalarTower K L A
L_alg : ∀ (x : L), IsIntegral K x
A_alg : ∀ (x : A), IsIntegral L x
⊢ ∀ (x : A), IsIntegral K x
[PROOFSTEP]
exact isIntegral_trans L_alg A_alg
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
f : L →ₐ[K] L
⊢ Function.Bijective ↑f
[PROOFSTEP]
refine' ⟨f.toRingHom.injective, fun b => _⟩
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
f : L →ₐ[K] L
b : L
⊢ ∃ a, ↑f a = b
[PROOFSTEP]
obtain ⟨p, hp, he⟩ := ha b
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : ↑(aeval b) p = 0
⊢ ∃ a, ↑f a = b
[PROOFSTEP]
let f' : p.rootSet L → p.rootSet L := (rootSet_maps_to' (fun x => x) f).restrict f _ _
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : ↑(aeval b) p = 0
f' : ↑(rootSet p L) → ↑(rootSet p L) :=
  Set.MapsTo.restrict (↑f) (rootSet p L) (rootSet p L) (_ : Set.MapsTo (↑f) (rootSet p L) (rootSet p L))
⊢ ∃ a, ↑f a = b
[PROOFSTEP]
have : Function.Surjective f' :=
  Finite.injective_iff_surjective.1 fun _ _ h => Subtype.eq <| f.toRingHom.injective <| Subtype.ext_iff.1 h
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : ↑(aeval b) p = 0
f' : ↑(rootSet p L) → ↑(rootSet p L) :=
  Set.MapsTo.restrict (↑f) (rootSet p L) (rootSet p L) (_ : Set.MapsTo (↑f) (rootSet p L) (rootSet p L))
this : Function.Surjective f'
⊢ ∃ a, ↑f a = b
[PROOFSTEP]
obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩
[GOAL]
case intro.intro.intro
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha✝ : IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : ↑(aeval b) p = 0
f' : ↑(rootSet p L) → ↑(rootSet p L) :=
  Set.MapsTo.restrict (↑f) (rootSet p L) (rootSet p L) (_ : Set.MapsTo (↑f) (rootSet p L) (rootSet p L))
this : Function.Surjective f'
a : ↑(rootSet p L)
ha : f' a = { val := b, property := (_ : b ∈ rootSet p L) }
⊢ ∃ a, ↑f a = b
[PROOFSTEP]
exact ⟨a, Subtype.ext_iff.1 ha⟩
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
x✝ : L ≃ₐ[K] L
⊢ (fun ϕ => AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)) ((fun ϕ => ↑ϕ) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
x✝ : L ≃ₐ[K] L
a✝ : L
⊢ ↑((fun ϕ => AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)) ((fun ϕ => ↑ϕ) x✝)) a✝ = ↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
x✝ : L →ₐ[K] L
⊢ (fun ϕ => ↑ϕ) ((fun ϕ => AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case H
K : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ha : IsAlgebraic K L
x✝¹ : L →ₐ[K] L
x✝ : L
⊢ ↑((fun ϕ => ↑ϕ) ((fun ϕ => AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)) x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
hz : IsAlgebraic R z
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
[PROOFSTEP]
rcases hz with ⟨p, p_ne_zero, px⟩
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
[PROOFSTEP]
set a := p.leadingCoeff
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
[PROOFSTEP]
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
[PROOFSTEP]
have x_integral : IsIntegral R (z * algebraMap R S a) :=
  ⟨p.integralNormalization, monic_integralNormalization p_ne_zero, integralNormalization_aeval_eq_zero px inj⟩
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
x_integral : IsIntegral R (z * ↑(algebraMap R S) a)
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
[PROOFSTEP]
exact ⟨⟨_, x_integral⟩, a, a_ne_zero, rfl⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
⊢ ∃ c d x, d • a = b * c
[PROOFSTEP]
obtain ⟨c, d, d_ne, hx⟩ :=
  exists_integral_multiple (h (algebraMap _ L a / algebraMap _ L b)) ((injective_iff_map_eq_zero _).mp inj)
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ∃ c d x, d • a = b * c
[PROOFSTEP]
refine' ⟨IsIntegralClosure.mk' S (c : L) c.2, d, d_ne, IsIntegralClosure.algebraMap_injective S R L _⟩
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) (d • a) = ↑(algebraMap S L) (b * mk' S ↑c (_ : ↑c ∈ integralClosure R L))
[PROOFSTEP]
simp only [Algebra.smul_def, RingHom.map_mul, IsIntegralClosure.algebraMap_mk', ← hx, ← IsScalarTower.algebraMap_apply]
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap R L) d * ↑(algebraMap S L) a =
    ↑(algebraMap S L) b * (↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d)
[PROOFSTEP]
rw [← mul_assoc _ (_ / _), mul_div_cancel' (algebraMap S L a), mul_comm]
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) b ≠ 0
[PROOFSTEP]
exact mt ((injective_iff_map_eq_zero _).mp (IsIntegralClosure.algebraMap_injective S R L) _) hb
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ x⁻¹ = ↑(aeval x) (divX p) / (↑(aeval x) p - ↑(algebraMap K L) (coeff p 0))
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) p = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
[PROOFSTEP]
conv_lhs => rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p * X + ↑C (coeff p 0)) = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
[PROOFSTEP]
rw [AlgHom.map_add, AlgHom.map_mul, aeval_X, aeval_C]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
[PROOFSTEP]
exact aeval_ne
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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))
[PROOFSTEP]
convert inv_eq_of_aeval_divX_ne_zero (p := p) (L := L) (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using
  1
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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))
[PROOFSTEP]
rw [aeval_eq, zero_sub, div_neg]
[GOAL]
case convert_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
case convert_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
convert aeval_eq
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
conv_rhs => rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
| ↑(aeval x) p
[PROOFSTEP]
rw [← divX_mul_X_add p]
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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))
[PROOFSTEP]
rw [AlgHom.map_add, AlgHom.map_mul, h, zero_mul, zero_add, aeval_C]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ (↑x)⁻¹ ∈ A
[PROOFSTEP]
suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
  rw [this]
  exact A.smul_mem (aeval x _).2 _
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
⊢ (↑x)⁻¹ ∈ A
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
⊢ ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p)) ∈ A
[PROOFSTEP]
exact A.smul_mem (aeval x _).2 _
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
[PROOFSTEP]
have : aeval (x : L) p = 0 := by
  rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
    -- porting note: this was a long sequence of `rw`.
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ ↑(aeval ↑x) p = 0
[PROOFSTEP]
rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
  -- porting note: this was a long sequence of `rw`.
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
[PROOFSTEP]
rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(aeval ↑x) (divX p)) =
    ↑(↑(algebraMap K ((fun x => { x // x ∈ A }) (divX p))) (-coeff p 0)⁻¹ * ↑(aeval x) (divX p))
[PROOFSTEP]
simp only [aeval_coe, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, coe_toSubsemiring, coe_algebraMap]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(↑(aeval x) (divX p))) =
    ↑(algebraMap K L) (-coeff p 0)⁻¹ * ↑(↑(aeval x) (divX p))
[PROOFSTEP]
rw [map_inv₀, map_neg, inv_neg, neg_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
obtain ⟨p, ne_zero, aeval_eq⟩ := hx
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq 
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
revert ne_zero aeval_eq
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
refine' p.recOnHorner _ _ _
[GOAL]
case intro.intro.refine'_1
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
intro h
[GOAL]
case intro.intro.refine'_1
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.refine'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
intro p a hp ha _ih _ne_zero aeval_eq
[GOAL]
case intro.intro.refine'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
refine' A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq _
[GOAL]
case intro.intro.refine'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
[GOAL]
case intro.intro.refine'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
intro p hp ih _ne_zero aeval_eq
[GOAL]
case intro.intro.refine'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rw [AlgHom.map_mul, aeval_X, mul_eq_zero] at aeval_eq 
[GOAL]
case intro.intro.refine'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
cases' aeval_eq with aeval_eq x_eq
[GOAL]
case intro.intro.refine'_3.inl
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
exact ih hp aeval_eq
[GOAL]
case intro.intro.refine'_3.inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rw [x_eq, Subalgebra.coe_zero, inv_zero]
[GOAL]
case intro.intro.refine'_3.inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
exact A.zero_mem
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
hKL : Algebra.IsAlgebraic K L
⊢ Nontrivial { x // x ∈ A }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
⊢ (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
z : S'
⊢ (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 z = OfNat.ofNat 1 z
[PROOFSTEP]
simp only [Polynomial.aeval_one, Pi.one_apply, map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
f g : R'[X]
⊢ OneHom.toFun
      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
      (f * g) =
    OneHom.toFun
        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
        f *
      OneHom.toFun
        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
        g
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
f g : R'[X]
z : S'
⊢ OneHom.toFun
      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
      (f * g) z =
    (OneHom.toFun
          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
          f *
        OneHom.toFun
          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
          g)
      z
[PROOFSTEP]
simp only [Pi.mul_apply, map_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (f g : R'[X]),
                OneHom.toFun
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                    (f * g) =
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      f *
                    OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      g) })
      0 =
    0
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
z : S'
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (f g : R'[X]),
                OneHom.toFun
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                    (f * g) =
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      f *
                    OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      g) })
      0 z =
    OfNat.ofNat 0 z
[PROOFSTEP]
simp only [Polynomial.aeval_zero, Pi.zero_apply, map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
f g : R'[X]
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (f g : R'[X]),
                OneHom.toFun
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                    (f * g) =
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      f *
                    OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      g) })
      (f + g) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (f g : R'[X]),
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      (f * g) =
                    OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        f *
                      OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        g) })
        f +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (f g : R'[X]),
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      (f * g) =
                    OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        f *
                      OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        g) })
        g
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
f g : R'[X]
z : S'
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (f g : R'[X]),
                OneHom.toFun
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                    (f * g) =
                  OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      f *
                    OneHom.toFun
                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                      g) })
      (f + g) z =
    (OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : R'[X]),
                    OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          g) })
          f +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : R'[X]),
                    OneHom.toFun
                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          g) })
          g)
      z
[PROOFSTEP]
simp only [Polynomial.aeval_add, Pi.add_apply, map_add]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
p : R'[X]
f : (fun x => S' → T') p
⊢ ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (f g : R'[X]),
                      OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          (f * g) =
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            f *
                          OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            g) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (f g : R'[X]),
                              OneHom.toFun
                                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                  (f * g) =
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    f *
                                  OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    g) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (f g : R'[X]),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      (f + g) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        f +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        g) }
        p *
      f =
    f *
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (f g : R'[X]),
                      OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          (f * g) =
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            f *
                          OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            g) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (f g : R'[X]),
                              OneHom.toFun
                                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                  (f * g) =
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    f *
                                  OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    g) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (f g : R'[X]),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      (f + g) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        f +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        g) }
        p
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
p : R'[X]
f : (fun x => S' → T') p
z : S'
⊢ (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (f g : R'[X]),
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            (f * g) =
                          OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              f *
                            OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              g) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (f g : R'[X]),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        (f + g) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          f +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          g) }
          p *
        f)
      z =
    (f *
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (f g : R'[X]),
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            (f * g) =
                          OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              f *
                            OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              g) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (f g : R'[X]),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        (f + g) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          f +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          g) }
          p)
      z
[PROOFSTEP]
exact mul_comm _ _
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
p : R'[X]
f : (fun x => S' → T') p
⊢ p • f =
    ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (f g : R'[X]),
                      OneHom.toFun
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                          (f * g) =
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            f *
                          OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            g) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (f g : R'[X]),
                              OneHom.toFun
                                  { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                    map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                  (f * g) =
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    f *
                                  OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    g) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (f g : R'[X]),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      (f + g) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        f +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        g) }
        p *
      f
[PROOFSTEP]
funext z
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing S
R' : Type u
S' : Type v
T' : Type w
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra S' T'
src✝ : SMul R'[X] (S' → T') := hasSMulPi' R' S' T'
p : R'[X]
f : (fun x => S' → T') p
z : S'
⊢ (p • f) z =
    (↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (f g : R'[X]),
                        OneHom.toFun
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                            (f * g) =
                          OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              f *
                            OneHom.toFun
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                              g) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                              map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : R'[X]),
                                OneHom.toFun
                                    { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                      map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      g) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (f g : R'[X]),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : R'[X]),
                                  OneHom.toFun
                                      { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                        map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        g) })
                        (f + g) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          f +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                  map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : R'[X]),
                                    OneHom.toFun
                                        { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                          map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun p z => ↑(algebraMap S' T') (↑(aeval z) p),
                                            map_one' := (_ : (fun p z => ↑(algebraMap S' T') (↑(aeval z) p)) 1 = 1) }
                                          g) })
                          g) }
          p *
        f)
      z
[PROOFSTEP]
simp only [polynomial_smul_apply', Algebra.algebraMap_eq_smul_one, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
  Pi.mul_apply, Algebra.smul_mul_assoc, one_mul]
