R : Type ?u.96690
S : Type u_2
T : Type ?u.96696
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.97002
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.97424
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
R : Type ?u.96690
S : Type u_2
T : Type ?u.96696
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.97002
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.97424
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ↑(aeval pb.gen) (minpolyGen pb) = 0
simp_rw [minpolyGen, AlgHom.map_sub, AlgHom.map_sum, AlgHom.map_mul, AlgHom.map_pow, aeval_C, ←
  Algebra.smul_def, aeval_X]
R : Type ?u.96690
S : Type u_2
T : Type ?u.96696
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.97002
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.97424
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
R : Type ?u.96690
S : Type u_2
T : Type ?u.96696
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.97002
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.97424
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
refine' sub_eq_zero.mpr ((pb.basis.total_repr (pb.gen ^ pb.dim)).symm.trans _)
no goals
R : Type ?u.96690
S : Type u_2
T : Type ?u.96696
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.97002
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.97424
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
rw [Finsupp.total_apply, Finsupp.sum_fintype] <;>
  simp only [pb.coe_basis, zero_smul, eq_self_iff_true, imp_true_iff]