-- Mathlib/RingTheory/PowerBasis.lean
theorem IsIntegral.mem_span_pow [Nontrivial R] {x y : S} (hx : IsIntegral R x)
    (hy : ∃ f : R[X], y = aeval x f) :
    y ∈ Submodule.span R (Set.range fun i : Fin (minpoly R x).natDegree => x ^ (i : ℕ))

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1

Tactic:
have := minpoly.monic hx

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ ∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ (aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = (aeval x) (f %ₘ minpoly R x)

Tactic:
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ (aeval x) f = (aeval x) (f %ₘ minpoly R x)

Tactic:
conv_lhs => rw [← modByMonic_add_div f this]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ (aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = (aeval x) (f %ₘ minpoly R x)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
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)

Tactic:
obtain ⟨f, rfl⟩ := hy

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ (aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ ∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1

Tactic:
refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ (aeval x) f = (aeval x) (f %ₘ minpoly R x)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ (aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)

Tactic:
apply mem_span_pow'.mpr _

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1