[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]


[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
classical exact isPrincipal_of_FG (Ideal.span { x, y }) ⟨{ x, y }, by simp⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
exact isPrincipal_of_FG (Ideal.span { x, y }) ⟨{ x, y }, by simp⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Ideal.span ↑{x, y} = Ideal.span {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
classical
constructor
· intro H x y; infer_instance
· intro H
  constructor
  apply Submodule.fg_induction
  · exact fun _ => ⟨⟨_, rfl⟩⟩
  · rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩; rw [← Submodule.span_insert]; exact H _ _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
intro H x y
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R
[PROOFSTEP]
constructor
[GOAL]
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), Ideal.FG I → Submodule.IsPrincipal I
[PROOFSTEP]
apply Submodule.fg_induction
[GOAL]
case mpr.isPrincipal_of_FG.h₁
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (x : R), Submodule.IsPrincipal (Submodule.span R {x})
[PROOFSTEP]
exact fun _ => ⟨⟨_, rfl⟩⟩
[GOAL]
case mpr.isPrincipal_of_FG.h₂
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (M₁ M₂ : Submodule R R), Submodule.IsPrincipal M₁ → Submodule.IsPrincipal M₂ → Submodule.IsPrincipal (M₁ ⊔ M₂)
[PROOFSTEP]
rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
[GOAL]
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ Submodule.IsPrincipal (Submodule.span R {x} ⊔ Submodule.span R {y})
[PROOFSTEP]
rw [← Submodule.span_insert]
[GOAL]
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ Submodule.IsPrincipal (Submodule.span R {x, y})
[PROOFSTEP]
exact H _ _
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ x ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y
[PROOFSTEP]
rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}
[PROOFSTEP]
rw [span_gcd, Ideal.span_insert, sup_le_iff]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
[PROOFSTEP]
exact ⟨hx, hy⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {x, y}
[PROOFSTEP]
rw [← span_gcd]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {gcd x y}
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ {gcd x y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsBezout R
⊢ IsIntegrallyClosed R
[PROOFSTEP]
classical exact GCDMonoid.toIsIntegrallyClosed
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsBezout R
⊢ IsIntegrallyClosed R
[PROOFSTEP]
exact GCDMonoid.toIsIntegrallyClosed
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ IsBezout S
[PROOFSTEP]
rw [iff_span_pair_isPrincipal]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ ∀ (x y : S), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : S
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y
[GOAL]
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {↑f x, ↑f y})
[PROOFSTEP]
use f (gcd x y)
[GOAL]
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
trans Ideal.map f (Ideal.span {gcd x y})
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Ideal.map f (Ideal.span {gcd x y})
[PROOFSTEP]
rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
rw [Ideal.map_span, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f (gcd x y)} = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
classical
tfae_have 1 → 2
· intro H; exact ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩
tfae_have 2 → 3
· intro; infer_instance
tfae_have 3 → 4
· intro; infer_instance
tfae_have 4 → 1
· rintro ⟨h⟩
  rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
  apply RelEmbedding.wellFounded _ h
  have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span { x } := fun ⟨I, hI⟩ =>
    (IsBezout.isPrincipal_of_FG I hI).1
  choose f hf using this
  exact
    { toFun := f
      inj' := fun x y e => by ext1; rw [hf, hf, e]
      map_rel_iff' := by
        dsimp
        intro a b
        rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
        rfl }
tfae_finish
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ IsNoetherianRing R → IsPrincipalIdealRing R
[PROOFSTEP]
intro H
[GOAL]
case tfae_1_to_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
H : IsNoetherianRing R
⊢ IsPrincipalIdealRing R
[PROOFSTEP]
exact ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R → UniqueFactorizationMonoid R
[PROOFSTEP]
intro
[GOAL]
case tfae_2_to_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
✝ : IsPrincipalIdealRing R
⊢ UniqueFactorizationMonoid R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
⊢ UniqueFactorizationMonoid R → WfDvdMonoid R
[PROOFSTEP]
intro
[GOAL]
case tfae_3_to_4
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
✝ : UniqueFactorizationMonoid R
⊢ WfDvdMonoid R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 4 → 1
[GOAL]
case tfae_4_to_1
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
⊢ WfDvdMonoid R → IsNoetherianRing R
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case tfae_4_to_1.mk
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ IsNoetherianRing R
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
[GOAL]
case tfae_4_to_1.mk
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
apply RelEmbedding.wellFounded _ h
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span { x } := fun ⟨I, hI⟩ =>
  (IsBezout.isPrincipal_of_FG I hI).1
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
this : ∀ (I : { J // Ideal.FG J }), ∃ x, ↑I = Ideal.span {x}
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
choose f hf using this
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
exact
  { toFun := f
    inj' := fun x y e => by ext1; rw [hf, hf, e]
    map_rel_iff' := by
      dsimp
      intro a b
      rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
      rfl }
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
x y : { N // Submodule.FG N }
e : f x = f y
⊢ x = y
[PROOFSTEP]
ext1
[GOAL]
case a
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
x y : { N // Submodule.FG N }
e : f x = f y
⊢ ↑x = ↑y
[PROOFSTEP]
rw [hf, hf, e]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ ∀ {a b : { N // Submodule.FG N }},
    DvdNotUnit (↑{ toFun := f, inj' := (_ : ∀ (x y : { N // Submodule.FG N }), f x = f y → x = y) } a)
        (↑{ toFun := f, inj' := (_ : ∀ (x y : { N // Submodule.FG N }), f x = f y → x = y) } b) ↔
      a > b
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ ∀ {a b : { N // Submodule.FG N }}, DvdNotUnit (f a) (f b) ↔ a > b
[PROOFSTEP]
intro a b
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
a b : { N // Submodule.FG N }
⊢ DvdNotUnit (f a) (f b) ↔ a > b
[PROOFSTEP]
rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
a b : { N // Submodule.FG N }
⊢ ↑b < ↑a ↔ a > b
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
tfae_4_to_1 : WfDvdMonoid R → IsNoetherianRing R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_finish