case inl
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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

case inr
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
cases subsingleton_or_nontrivial A
case inr
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
case inr
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
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]
case pos
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)

case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
case inr
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
by_cases hf : f %ₘ minpoly A pb.gen = 0
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
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)
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, LinearMap.map_sum]
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
refine' Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => _
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
rw [Finset.mem_range] at hi
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
rw [LinearMap.map_smul]
case neg.e_a
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
case neg
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
congr
no goals
case neg.e_a
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
no goals
case inl
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]
no goals
case pos
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
simp only [hf, AlgHom.map_zero, LinearMap.map_zero]
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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
rw [← pb.natDegree_minpoly]
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
apply natDegree_lt_natDegree hf
no goals
R : Type ?u.172809
S : Type u_2
T : Type ?u.172815
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.173121
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.173543
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
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)
exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)