-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem degreeLT_eq_span_X_pow [DecidableEq R] {n : ℕ} :
    degreeLT R n = Submodule.span R ↑((Finset.range n).image fun n => X ^ n : Finset R[X])

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
refine
  Submodule.smul_mem _ _
    (Submodule.subset_span <|
      Finset.mem_coe.2 <| Finset.mem_image.2 ⟨_, Finset.mem_range.2 this, rfl⟩)

Result:
no goals

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
replace hp := mem_degreeLT.1 hp

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ p ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
intro p hp

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ ↑(range n) ⊆ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)

Tactic:
intro k hk

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ k ∈ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ ((fun n => X ^ n) k).degree < ↑n

Tactic:
exact lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n = Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
apply le_antisymm

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n => X ^ n) (range n))

case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n => X ^ n) (range n)) ≤ degreeLT R n

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ p ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
rw [← C_mul_X_pow_eq_monomial, C_mul']

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ k ∈ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)

Tactic:
apply mem_degreeLT.2

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ ((fun n => X ^ n) k).degree < ↑n

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n => X ^ n) (range n)) ≤ degreeLT R n

Tactic:
rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ ↑(range n) ⊆ (fun n => X ^ n) ⁻¹' ↑(degreeLT R n)

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))

Tactic:
refine Submodule.sum_mem _ fun k hk => ?_

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n => X ^ n) (range n))