-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma coeff_minpolyDiv_sub_pow_mem_span {i} (hi : i ≤ natDegree (minpolyDiv R x)) :
    coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i ∈
      Submodule.span R ((x ^ ·) '' Set.Iio i)

Proof state:
case succ.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio (i + 1))

Tactic:
apply SetLike.le_def.mp ?_
  (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
    (Submodule.mem_span_singleton_self x))

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i) * Submodule.span R {x} ≤
    Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio (i + 1))

Proof state:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1)) - x ^ (i + 1) ∈
    Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio (i + 1))

Tactic:
rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]

Result:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio (i + 1))

Proof state:
case zero
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
hi : 0 ≤ (minpolyDiv R x).natDegree
⊢ (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - 0) - x ^ 0 ∈ Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio 0)

Tactic:
simp [(minpolyDiv_monic hx).leadingCoeff]

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 => x ^ x_1 * x) '' Set.Iio i) ≤ Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio (i + 1))

Tactic:
apply Submodule.span_mono

Result:
case h
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (fun x_1 => x ^ x_1 * x) '' Set.Iio i ⊆ (fun x_1 => x ^ x_1) '' Set.Iio (i + 1)

Proof state:
case h.intro.intro
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
j : ℕ
hj : j < i
⊢ (fun x_1 => x ^ x_1 * x) j ∈ (fun x_1 => x ^ x_1) '' Set.Iio (i + 1)

Tactic:
exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩

Result:
no goals

Proof state:
case succ.refine_1.h.a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ 1 ∈ (fun x_1 => x ^ x_1) '' Set.Iio (i + 1)

Tactic:
exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩

Result:
no goals