R : Type u_1
S : Type u_2
T : Type ?u.46692
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.46995
B : Type ?u.46998
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.47420
inst✝ : Field K
pb : PowerBasis R S
y : S
✝ : Nontrivial S
⊢ ∃ f, y = ↑(aeval pb.gen) f
R : Type u_1
S : Type u_2
T : Type ?u.46692
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.46995
B : Type ?u.46998
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.47420
inst✝ : Field K
pb : PowerBasis R S
y : S
⊢ ∃ f, y = ↑(aeval pb.gen) f
nontriviality S
case intro.intro
R : Type u_1
S : Type u_2
T : Type ?u.46692
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.46995
B : Type ?u.46998
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.47420
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
R : Type u_1
S : Type u_2
T : Type ?u.46692
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.46995
B : Type ?u.46998
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.47420
inst✝ : Field K
pb : PowerBasis R S
y : S
✝ : Nontrivial S
⊢ ∃ f, y = ↑(aeval pb.gen) f
obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
no goals
case intro.intro
R : Type u_1
S : Type u_2
T : Type ?u.46692
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.46995
B : Type ?u.46998
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.47420
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
exact ⟨f, hf⟩