case intro
R : Type ?u.455322
S : Type u_2
T : Type ?u.455328
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.455634
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.456056
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
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'
R : Type ?u.455322
S : Type u_2
T : Type ?u.455328
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.455634
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.456056
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
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'
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
case intro.intro
R : Type ?u.455322
S : Type u_2
T : Type ?u.455328
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.455634
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.456056
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 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)
case intro
R : Type ?u.455322
S : Type u_2
T : Type ?u.455328
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.455634
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.456056
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
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'
obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
no goals
case intro.intro
R : Type ?u.455322
S : Type u_2
T : Type ?u.455328
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.455634
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.456056
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 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)
simp only [← aeval_mul, pb.constr_pow_aeval hy]