[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
pb : PowerBasis K S
⊢ FiniteDimensional.finrank K S = pb.dim
[PROOFSTEP]
rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
[PROOFSTEP]
have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) :=
  by
  ext n
  simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
  exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
⊢ (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (n ∈ Set.range fun i => x ^ ↑i) ↔ n ∈ (fun i => x ^ i) '' ↑(Finset.range d)
[PROOFSTEP]
simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
[GOAL]
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1, x_1 < d ∧ x ^ x_1 = n
[PROOFSTEP]
exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
[PROOFSTEP]
simp only [this, Finsupp.mem_span_image_iff_total, degree_lt_iff_coeff_zero, exists_iff_exists_finsupp, coeff, aeval,
  eval₂RingHom', eval₂_eq_sum, Polynomial.sum, support, Finsupp.mem_supported', Finsupp.total, Finsupp.sum,
  Algebra.smul_def, eval₂_zero, exists_prop, LinearMap.id_coe, eval₂_one, id.def, not_lt, Finsupp.coe_lsum,
  LinearMap.coe_smulRight, Finset.mem_range, AlgHom.coe_mks, Finset.mem_coe]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ y = Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1
[PROOFSTEP]
simp_rw [@eq_comm _ y]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ (Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1) = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
[PROOFSTEP]
rw [mem_span_pow']
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, degree f < ↑d ∧ y = ↑(aeval x) f) ↔ ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, degree f < ↑d ∧ y = ↑(aeval x) f) → ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
[PROOFSTEP]
rintro ⟨f, h, hy⟩
[GOAL]
case mp.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : degree f < ↑d
hy : y = ↑(aeval x) f
⊢ ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
[PROOFSTEP]
refine' ⟨f, _, hy⟩
[GOAL]
case mp.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : degree f < ↑d
hy : y = ↑(aeval x) f
⊢ natDegree f < d
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : degree f < ↑d
hy : y = ↑(aeval x) f
hf : f = 0
⊢ natDegree f < d
[PROOFSTEP]
simp only [hf, natDegree_zero, degree_zero] at h ⊢
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : ⊥ < ↑d
⊢ 0 < d
[PROOFSTEP]
first
| exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
| exact WithBot.bot_lt_coe d
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : ⊥ < ↑d
⊢ 0 < d
[PROOFSTEP]
exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : degree f < ↑d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ natDegree f < d
[PROOFSTEP]
simp_all only [degree_eq_natDegree hf]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : ↑(natDegree f) < ↑d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ natDegree f < d
[PROOFSTEP]
first
| exact WithBot.coe_lt_coe.1 h
| exact WithBot.coe_lt_coe.2 h
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : ↑(natDegree f) < ↑d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ natDegree f < d
[PROOFSTEP]
exact WithBot.coe_lt_coe.1 h
[GOAL]
case mpr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, natDegree f < d ∧ y = ↑(aeval x) f) → ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
[PROOFSTEP]
rintro ⟨f, h, hy⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
[PROOFSTEP]
refine' ⟨f, _, hy⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ degree f < ↑d
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : f = 0
⊢ degree f < ↑d
[PROOFSTEP]
simp only [hf, natDegree_zero, degree_zero] at h ⊢
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
[PROOFSTEP]
first
| exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
| exact WithBot.bot_lt_coe d
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
[PROOFSTEP]
exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
[PROOFSTEP]
exact WithBot.bot_lt_coe d
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ degree f < ↑d
[PROOFSTEP]
simp_all only [degree_eq_natDegree hf]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
[PROOFSTEP]
first
| exact WithBot.coe_lt_coe.1 h
| exact WithBot.coe_lt_coe.2 h
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
[PROOFSTEP]
exact WithBot.coe_lt_coe.1 h
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
[PROOFSTEP]
exact WithBot.coe_lt_coe.2 h
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i => pb.gen ^ ↑i)
[PROOFSTEP]
simpa using pb.basis.mem_span y
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
pb : PowerBasis R S
y : S
⊢ ∃ f, y = ↑(aeval pb.gen) f
[PROOFSTEP]
nontriviality S
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
pb : PowerBasis R S
y : S
✝ : Nontrivial S
⊢ ∃ f, y = ↑(aeval pb.gen) f
[PROOFSTEP]
obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type u_6
inst✝ : Field K
pb : PowerBasis R S
y : S
✝ : Nontrivial S
f : R[X]
left✝ : natDegree f < pb.dim
hf : y = ↑(aeval pb.gen) f
⊢ ∃ f, y = ↑(aeval pb.gen) f
[PROOFSTEP]
exact ⟨f, hf⟩
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : ↑f pb.gen = ↑g pb.gen
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case H
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : ↑f pb.gen = ↑g pb.gen
x : S
⊢ ↑f x = ↑g x
[PROOFSTEP]
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
[GOAL]
case H.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : ↑f✝ pb.gen = ↑g pb.gen
f : R[X]
⊢ ↑f✝ (↑(aeval pb.gen) f) = ↑g (↑(aeval pb.gen) f)
[PROOFSTEP]
rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ↑(aeval pb.gen) (minpolyGen pb) = 0
[PROOFSTEP]
simp_rw [minpolyGen, AlgHom.map_sub, AlgHom.map_sum, AlgHom.map_mul, AlgHom.map_pow, aeval_C, ← Algebra.smul_def,
  aeval_X]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.gen ^ pb.dim - ∑ x : Fin pb.dim, ↑(↑pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x = 0
[PROOFSTEP]
refine' sub_eq_zero.mpr ((pb.basis.total_repr (pb.gen ^ pb.dim)).symm.trans _)
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ↑(Finsupp.total (Fin pb.dim) S A ↑pb.basis) (↑pb.basis.repr (pb.gen ^ pb.dim)) =
    ∑ x : Fin pb.dim, ↑(↑pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.sum_fintype]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ∑ i : Fin pb.dim, ↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i • ↑pb.basis i =
    ∑ x : Fin pb.dim, ↑(↑pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x
[PROOFSTEP]
simp only [pb.coe_basis, zero_smul, eq_self_iff_true, imp_true_iff]
[GOAL]
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ∀ (i : Fin pb.dim), 0 • ↑pb.basis i = 0
[PROOFSTEP]
simp only [pb.coe_basis, zero_smul, eq_self_iff_true, imp_true_iff]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ Monic (minpolyGen pb)
[PROOFSTEP]
nontriviality A
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ Monic (minpolyGen pb)
[PROOFSTEP]
apply (monic_X_pow _).sub_of_left _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < degree (X ^ pb.dim)
[PROOFSTEP]
rw [degree_X_pow]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
[PROOFSTEP]
exact degree_sum_fin_lt _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
⊢ pb.dim ≤ natDegree p
[PROOFSTEP]
refine' le_of_not_lt fun hlt => ne_zero _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ p = 0
[PROOFSTEP]
rw [p.as_sum_range' _ hlt, Finset.sum_range]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ ∑ i : Fin pb.dim, ↑(monomial ↑i) (coeff p ↑i) = 0
[PROOFSTEP]
refine' Fintype.sum_eq_zero _ fun i => _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
[PROOFSTEP]
simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root 
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
[PROOFSTEP]
have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
this : ∀ (i : Fin pb.dim), coeff p ↑i = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
[PROOFSTEP]
rw [this, monomial_zero_right]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval h.gen) p = 0
⊢ ↑h.dim ≤ degree p
[PROOFSTEP]
rw [degree_eq_natDegree ne_zero]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval h.gen) p = 0
⊢ ↑h.dim ≤ ↑(natDegree p)
[PROOFSTEP]
exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (minpolyGen pb) = ↑pb.dim
[PROOFSTEP]
unfold minpolyGen
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (X ^ pb.dim - ∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) = ↑pb.dim
[PROOFSTEP]
rw [degree_sub_eq_left_of_degree_lt]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (X ^ pb.dim) = ↑pb.dim
[PROOFSTEP]
rw [degree_X_pow]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < degree (X ^ pb.dim)
[PROOFSTEP]
rw [degree_X_pow]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
[PROOFSTEP]
apply degree_sum_fin_lt
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ minpolyGen pb = minpoly A pb.gen
[PROOFSTEP]
nontriviality A
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ minpolyGen pb = minpoly A pb.gen
[PROOFSTEP]
refine' minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq => or_iff_not_imp_left.2 fun hn0 h0 => _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
q : A[X]
hq : degree q < degree (minpolyGen pb)
hn0 : ¬q = 0
h0 : ↑(aeval pb.gen) q = 0
⊢ False
[PROOFSTEP]
exact (pb.dim_le_degree_of_root hn0 h0).not_lt (pb.degree_minpolyGen ▸ hq)
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (minpoly A pb.gen) = ↑pb.dim
[PROOFSTEP]
rw [← minpolyGen_eq, degree_minpolyGen]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ natDegree (minpoly A pb.gen) = pb.dim
[PROOFSTEP]
rw [← minpolyGen_eq, natDegree_minpolyGen]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
[PROOFSTEP]
cases subsingleton_or_nontrivial A
[GOAL]
case inl
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
[PROOFSTEP]
rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.lmul A S) pb.gen =
    ↑(Matrix.toLin pb.basis pb.basis)
      (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0)
[PROOFSTEP]
refine' pb.basis.ext fun k => _
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (↑pb.basis k) =
    ↑(↑(Matrix.toLin pb.basis pb.basis)
          (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0))
      (↑pb.basis k)
[PROOFSTEP]
simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
[PROOFSTEP]
apply (pow_succ _ _).symm.trans
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, -coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x
[PROOFSTEP]
simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = 0
[PROOFSTEP]
convert pb.aeval_minpolyGen
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = ↑(aeval pb.gen) (minpolyGen pb)
[PROOFSTEP]
rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff, pb.minpolyGen_monic.leadingCoeff, one_smul,
  natDegree_minpolyGen, Finset.sum_range]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
[PROOFSTEP]
rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
[GOAL]
case neg.hc
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑{ val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } = ↑k + 1
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim),
    x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
[PROOFSTEP]
intro x hx
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
[PROOFSTEP]
rw [if_neg, zero_smul]
[GOAL]
case neg.hnc
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ ¬↑x = ↑k + 1
[PROOFSTEP]
apply mt Fin.ext hx
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f) = ↑(aeval y) f
[PROOFSTEP]
cases subsingleton_or_nontrivial A
[GOAL]
case inl
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Subsingleton A
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f) = ↑(aeval y) f
[PROOFSTEP]
rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f) = ↑(aeval y) f
[PROOFSTEP]
rw [← aeval_modByMonic_eq_self_of_root (minpoly.monic pb.isIntegral_gen) (minpoly.aeval _ _), ←
  @aeval_modByMonic_eq_self_of_root _ _ _ _ _ f _ (minpoly.monic pb.isIntegral_gen) y hy]
[GOAL]
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) (f %ₘ minpoly A pb.gen)) =
    ↑(aeval y) (f %ₘ minpoly A pb.gen)
[PROOFSTEP]
by_cases hf : f %ₘ minpoly A pb.gen = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : f %ₘ minpoly A pb.gen = 0
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) (f %ₘ minpoly A pb.gen)) =
    ↑(aeval y) (f %ₘ minpoly A pb.gen)
[PROOFSTEP]
simp only [hf, AlgHom.map_zero, LinearMap.map_zero]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) (f %ₘ minpoly A pb.gen)) =
    ↑(aeval y) (f %ₘ minpoly A pb.gen)
[PROOFSTEP]
have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim :=
  by
  rw [← pb.natDegree_minpoly]
  apply natDegree_lt_natDegree hf
  exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ natDegree (f %ₘ minpoly A pb.gen) < pb.dim
[PROOFSTEP]
rw [← pb.natDegree_minpoly]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ natDegree (f %ₘ minpoly A pb.gen) < natDegree (minpoly A pb.gen)
[PROOFSTEP]
apply natDegree_lt_natDegree hf
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ degree (f %ₘ minpoly A pb.gen) < degree (minpoly A pb.gen)
[PROOFSTEP]
exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) (f %ₘ minpoly A pb.gen)) =
    ↑(aeval y) (f %ₘ minpoly A pb.gen)
[PROOFSTEP]
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, LinearMap.map_sum]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
⊢ (Finset.sum (Finset.range pb.dim) fun i =>
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (coeff (f %ₘ minpoly A pb.gen) i • pb.gen ^ i)) =
    Finset.sum (Finset.range pb.dim) fun i => coeff (f %ₘ minpoly A pb.gen) i • y ^ i
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => _
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
i : ℕ
hi : i ∈ Finset.range pb.dim
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (coeff (f %ₘ minpoly A pb.gen) i • pb.gen ^ i) =
    coeff (f %ₘ minpoly A pb.gen) i • y ^ i
[PROOFSTEP]
rw [Finset.mem_range] at hi 
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (coeff (f %ₘ minpoly A pb.gen) i • pb.gen ^ i) =
    coeff (f %ₘ minpoly A pb.gen) i • y ^ i
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
i : ℕ
hi : i < pb.dim
⊢ coeff (f %ₘ minpoly A pb.gen) i • ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (pb.gen ^ i) =
    coeff (f %ₘ minpoly A pb.gen) i • y ^ i
[PROOFSTEP]
congr
[GOAL]
case neg.e_a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : natDegree (f %ₘ minpoly A pb.gen) < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (pb.gen ^ i) = y ^ i
[PROOFSTEP]
rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) pb.gen = y
[PROOFSTEP]
convert pb.constr_pow_aeval hy X
[GOAL]
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
⊢ pb.gen = ↑(aeval pb.gen) X
[PROOFSTEP]
rw [aeval_X]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
⊢ y = ↑(aeval y) X
[PROOFSTEP]
rw [aeval_X]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(algebraMap A S) x) = ↑(algebraMap A S') x
[PROOFSTEP]
convert pb.constr_pow_aeval hy (C x)
[GOAL]
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ↑(algebraMap A S) x = ↑(aeval pb.gen) (↑C x)
[PROOFSTEP]
rw [aeval_C]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ↑(algebraMap A S') x = ↑(aeval y) (↑C x)
[PROOFSTEP]
rw [aeval_C]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x x' : S
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (x * x') =
    ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) x * ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) x'
[PROOFSTEP]
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
[GOAL]
case intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x' : S
f : A[X]
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f * x') =
    ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f) * ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) x'
[PROOFSTEP]
obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
[GOAL]
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
f g : A[X]
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f * ↑(aeval pb.gen) g) =
    ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) f) *
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(aeval pb.gen) g)
[PROOFSTEP]
simp only [← aeval_mul, pb.constr_pow_aeval hy]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ AddHom.toFun src✝.toAddHom 1 = 1
[PROOFSTEP]
convert pb.constr_pow_algebraMap hy 1 using 2
[GOAL]
case h.e'_2.h.e'_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ 1 = ↑(algebraMap A S) 1
[PROOFSTEP]
rw [RingHom.map_one]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ 1 = ↑(algebraMap A S') 1
[PROOFSTEP]
rw [RingHom.map_one]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x x' : S),
                ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (x * x') =
                  ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) x * ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) x') })
      0 =
    0
[PROOFSTEP]
convert pb.constr_pow_algebraMap hy 0 using 2
[GOAL]
case h.e'_2.h.e'_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ 0 = ↑(algebraMap A S) 0
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
src✝ : (fun x => S →ₗ[A] S') fun i => y ^ ↑i := ↑(Basis.constr pb.basis A) fun i => y ^ ↑i
⊢ 0 = ↑(algebraMap A S') 0
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
f : S →ₐ[A] S'
⊢ ↑(aeval (↑f pb.gen)) (minpoly A pb.gen) = 0
[PROOFSTEP]
rw [aeval_algHom_apply, minpoly.aeval, f.map_zero]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
x : B
⊢ ↑(aeval x) (minpoly A pb.gen) = 0 ↔ ↑(Equiv.refl B) x ∈ roots (map (algebraMap A B) (minpoly A pb.gen))
[PROOFSTEP]
rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
x : B
⊢ ↑(aeval x) (minpoly A pb.gen) = 0 ↔ ↑(aeval x) (map (algebraMap A B) (minpoly A pb.gen)) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
x : B
⊢ map (algebraMap A B) (minpoly A pb.gen) ≠ 0
[PROOFSTEP]
exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ AlgHom.comp (lift pb pb'.gen h₂) (lift pb' pb.gen h₁) = AlgHom.id A S'
[PROOFSTEP]
ext x
[GOAL]
case H
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
x : S'
⊢ ↑(AlgHom.comp (lift pb pb'.gen h₂) (lift pb' pb.gen h₁)) x = ↑(AlgHom.id A S') x
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x
[GOAL]
case H.intro.refl
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(AlgHom.comp (lift pb pb'.gen h₂) (lift pb' pb.gen h₁)) (↑(aeval pb'.gen) f) = ↑(AlgHom.id A S') (↑(aeval pb'.gen) f)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ AlgHom.comp (lift pb' pb.gen h₁) (lift pb pb'.gen h₂) = AlgHom.id A S
[PROOFSTEP]
ext x
[GOAL]
case H
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
x : S
⊢ ↑(AlgHom.comp (lift pb' pb.gen h₁) (lift pb pb'.gen h₂)) x = ↑(AlgHom.id A S) x
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval' x
[GOAL]
case H.intro.refl
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : ↑(aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : ↑(aeval pb'.gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(AlgHom.comp (lift pb' pb.gen h₁) (lift pb pb'.gen h₂)) (↑(aeval pb.gen) f) = ↑(AlgHom.id A S) (↑(aeval pb.gen) f)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
by_cases IsIntegral K x
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
by_cases IsIntegral K x
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
rw [minpoly.eq_zero h, natDegree_zero]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
exact linearIndependent_empty_type
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
[PROOFSTEP]
refine' Fintype.linearIndependent_iff.2 fun g hg i => _
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
[PROOFSTEP]
simp only at hg 
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
[PROOFSTEP]
simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg 
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
[PROOFSTEP]
apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_lt).mtr
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) < degree (minpoly K x)
[PROOFSTEP]
simp_rw [← C_mul_X_pow_eq_monomial]
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑C (g x_1) * X ^ ↑x_1) < degree (minpoly K x)
[PROOFSTEP]
exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
[PROOFSTEP]
apply_fun lcoeff K i at h0 
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : ↑(lcoeff K ↑i) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = ↑(lcoeff K ↑i) 0
⊢ g i = 0
[PROOFSTEP]
simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0 
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (if i ∈ Finset.univ then g i else 0) = coeff 0 ↑i
⊢ g i = 0
[PROOFSTEP]
exact (if_pos <| Finset.mem_univ _).symm.trans h0
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ f, y = ↑(aeval x) f
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
[PROOFSTEP]
obtain ⟨f, rfl⟩ := hy
[GOAL]
case intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ↑(aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
[PROOFSTEP]
apply mem_span_pow'.mpr _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
[PROOFSTEP]
have := minpoly.monic hx
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
[PROOFSTEP]
refine' ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, _⟩
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) f = ↑(aeval x) (f %ₘ minpoly R x)
[PROOFSTEP]
conv_lhs => rw [← modByMonic_add_div f this]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
| ↑(aeval x) f
[PROOFSTEP]
rw [← modByMonic_add_div f this]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
| ↑(aeval x) f
[PROOFSTEP]
rw [← modByMonic_add_div f this]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
| ↑(aeval x) f
[PROOFSTEP]
rw [← modByMonic_add_div f this]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_6
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = ↑(aeval x) (f %ₘ minpoly R x)
[PROOFSTEP]
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, AlgHom.map_mul]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ ↑(Basis.map pb.basis (AlgEquiv.toLinearEquiv e)) i = ↑e pb.gen ^ ↑i
[PROOFSTEP]
rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, e.map_pow]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
S' : Type u_7
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ minpolyGen (map pb e) = minpolyGen pb
[PROOFSTEP]
dsimp only [minpolyGen, map_dim]
  -- Turn `Fin (pb.map e).dim` into `Fin pb.dim`
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
S' : Type u_7
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (X ^ pb.dim - Finset.sum Finset.univ fun i => ↑C (↑(↑(map pb e).basis.repr ((map pb e).gen ^ pb.dim)) i) * X ^ ↑i) =
    X ^ pb.dim - Finset.sum Finset.univ fun i => ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i
[PROOFSTEP]
simp only [LinearEquiv.trans_apply, map_basis, Basis.map_repr, map_gen, AlgEquiv.toLinearEquiv_apply,
  e.toLinearEquiv_symm, AlgEquiv.map_pow, AlgEquiv.symm_apply_apply, sub_right_inj]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
S' : Type u_7
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
⊢ equivOfRoot pb (map pb e) h₁ h₂ = e
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
S' : Type u_7
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
x : S
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) x = ↑e x
[PROOFSTEP]
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
[GOAL]
case h.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
S' : Type u_7
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) (↑(aeval pb.gen) f) = ↑e (↑(aeval pb.gen) f)
[PROOFSTEP]
simp [aeval_algEquiv]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
⊢ adjoin R {B.gen} = ⊤
[PROOFSTEP]
rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
⊢ Set.range ↑B.basis ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
[PROOFSTEP]
rintro x ⟨i, rfl⟩
[GOAL]
case intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ ↑B.basis i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
[PROOFSTEP]
rw [B.basis_eq_pow i]
[GOAL]
case intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
[PROOFSTEP]
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {x} = ⊤
[PROOFSTEP]
rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {B.gen} ≤ adjoin R {x}
[PROOFSTEP]
refine' adjoin_le _
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type u_6
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ {B.gen} ⊆ ↑(adjoin R {x})
[PROOFSTEP]
simp [hx]
