awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])) p
have a : Membership.mem (γ := Submodule R R[X])
  (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
  (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
Tactic: rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
have a : ∀ (k : ℕ) (hk : k ∈ p.support),
  Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
Tactic: refine Submodule.sum_mem _ fun k hk => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
have this : k ≤ (↑n : ℕ)
Tactic: have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k ≤ (↑n : ℕ)
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
have a : Membership.mem (γ := Submodule R R[X])
  (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
  (p.coeff k • HPow.hPow (α := R[X]) X k)
Tactic: rw [← C_mul_X_pow_eq_monomial, C_mul']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]) ≤
    degreeLE R (↑n : WithBot ℕ)
have a : (↑(range (n + 1)) : Set ℕ) ⊆ (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLE R (↑n : WithBot ℕ)) : Set R[X])
Tactic: rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range (n + 1)) : Set ℕ)
⊢ Membership.mem (γ := Set ℕ)
    ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLE R (↑n : WithBot ℕ)) : Set R[X])) k
have a : degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) ≤ (↑n : WithBot ℕ)
Tactic: apply mem_degreeLE.2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ degreeLT R n = Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])
have a : degreeLT R n ≤ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a : degreeLT R n ≤ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])
⊢ degreeLT R n = Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])
have a₁ : Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]) ≤ degreeLT R n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])) p
have hp₁ : p.degree < (↑n : WithBot ℕ)
Tactic: replace hp := mem_degreeLT.1 hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])) p
have a : Membership.mem (γ := Submodule R R[X])
  (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
  (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
Tactic: rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
have a : ∀ (k : ℕ) (hk : k ∈ p.support),
  Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
Tactic: refine Submodule.sum_mem _ fun k hk => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
have this : k < n
Tactic: have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
have a : Membership.mem (γ := Submodule R R[X])
  (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
  (p.coeff k • HPow.hPow (α := R[X]) X k)
Tactic: rw [← C_mul_X_pow_eq_monomial, C_mul']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]) ≤ degreeLT R n
have a : (↑(range n) : Set ℕ) ⊆ (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLT R n) : Set R[X])
Tactic: rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range n) : Set ℕ)
⊢ Membership.mem (γ := Set ℕ) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLT R n) : Set R[X])) k
have a : degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) < (↑n : WithBot ℕ)
Tactic: apply mem_degreeLT.2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
⊢ (fun (n_1 : Fin n) ↦ (↑(p + q) : R[X]).coeff (↑n_1 : ℕ)) =
    HAdd.hAdd (α := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) fun (n_1 : Fin n) ↦
      (↑q : R[X]).coeff (↑n_1 : ℕ)
have h : ∀ (x : Fin n),
  (↑(p + q) : R[X]).coeff (↑x : ℕ) =
    HAdd.hAdd (α := Fin n → R) (β := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      (fun (n_1 : Fin n) ↦ (↑q : R[X]).coeff (↑n_1 : ℕ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x : Fin n
⊢ (↑(p + q) : R[X]).coeff (↑x : ℕ) =
    HAdd.hAdd (α := Fin n → R) (β := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      (fun (n_1 : Fin n) ↦ (↑q : R[X]).coeff (↑n_1 : ℕ)) x
have h : ((↑p : R[X]) + (↑q : R[X])).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x : Fin n
⊢ ((↑p : R[X]) + (↑q : R[X])).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)
have h : (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)
Tactic: rw [coeff_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
⊢ (fun (n_1 : Fin n) ↦ (↑(x • p) : R[X]).coeff (↑n_1 : ℕ)) =
    HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R) fun (n_1 : Fin n) ↦
      (↑p : R[X]).coeff (↑n_1 : ℕ)
have h : ∀ (x_1 : Fin n),
  (↑(x • p) : R[X]).coeff (↑x_1 : ℕ) =
    HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x_1 : Fin n
⊢ (↑(x • p) : R[X]).coeff (↑x_1 : ℕ) =
    HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) x_1
have h : (x • (↑p : R[X])).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x_1 : Fin n
⊢ (x • (↑p : R[X])).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)
have h : x • (↑p : R[X]).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)
Tactic: rw [coeff_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ (fun (f : Fin n → R) ↦
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
            (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
          ↥(degreeLT R n)))
      ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp)) =
    Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp
have a : (↑((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) sorry :
            ↥(degreeLT R n)))
        ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
    R[X]) =
  (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ (↑((fun (f : Fin n → R) ↦
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
                (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
              ↥(degreeLT R n)))
          ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])
have a : ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have pos : ∀ (hp0 : p = 0), ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
pos : ∀ (hp0 : p = 0), ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have neg : ∀ (hp0 : ¬p = 0), ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
hp0 : p = 0
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have pos : ∀ (hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) 0),
  Eq.{u_2 + 1} (α := R[X]) (∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (coeff 0 (↑x : ℕ))) 0
Tactic: subst hp0
Cleared hypotheses: p, hp, hp0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
hp0 : ¬p = 0
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have hp₁ : p.natDegree < n
Tactic: rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp
Cleared hypotheses: hp, hp0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : p.natDegree < n
hp0 : ¬p = 0
| p
have rw : ∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (p.coeff (↑i : ℕ))
Tactic: rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : p.natDegree < n
hp0 : ¬p = 0
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have conv_rhs : ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
Tactic: conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : p.natDegree < n
hp0 : ¬p = 0
conv_rhs : ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
have neg : Eq.{u_2 + 1} (α := R[X]) (∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)))
  (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (p.coeff (↑i : ℕ)))
Tactic: conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
⊢ (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      ((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
            ↥(degreeLT R n)))
        f) =
    f
have h : ∀ (i : Fin n),
  (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      ((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) sorry :
            ↥(degreeLT R n)))
        f)
      i =
    f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
⊢ (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      ((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
            ↥(degreeLT R n)))
        f)
      i =
    f i
have h : ∑ b : Fin n, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ) = f i
Tactic: simp only [finsetSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
⊢ ∑ b : Fin n, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ) = f i
have h : ∀ (b : Fin n),
  Membership.mem (γ := Finset (Fin n)) univ b →
    b ≠ i → Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ)) 0
Tactic: rw [Finset.sum_eq_single i, coeff_monomial, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
h :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) univ b →
      b ≠ i → Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ)) 0
⊢ ∑ b : Fin n, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ) = f i
have h₁ : i ∉ univ → Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) (↑i : ℕ)) 0
Tactic: rw [Finset.sum_eq_single i, coeff_monomial, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i j : Fin n
hji : j ≠ i
⊢ Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑j : ℕ) : (a : R) → R[X]) (f j)) (↑i : ℕ)) 0
have h : ¬(↑j : ℕ) = (↑i : ℕ)
Tactic: rw [coeff_monomial, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i j : Fin n
hji : j ≠ i
⊢ ¬(↑j : ℕ) = (↑i : ℕ)
have h : ¬j = i
Tactic: rwa [← Fin.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
x : R
⊢ eval x p =
    ∑ i : Fin n,
      HMul.hMul (α := R)
        ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) i :
          R)
        (x ^ (↑i : ℕ))
have simp_rw : Eq (α := R) (p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
  (∑ i : Fin n,
    HMul.hMul (α := R)
      ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) i :
        R)
      (x ^ (↑i : ℕ)))
Tactic: simp_rw [eval_eq_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
x : R
⊢ ∀ (i : ℕ), 0 * x ^ i = 0
have simp_rw : ∀ (i : ℕ), True
Tactic: simp_rw [zero_mul, forall_const]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq (α := Submodule R R[X]) (degreeLT R (n + 1)) (degreeLE R (↑n : WithBot ℕ))
have h : ∀ (x : R[X]),
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have pos : ∀ (x_zero : x = 0),
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
Tactic: by_cases x_zero : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
pos :
  ∀ (x_zero : x = 0),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
      Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg : ∀ (x_zero : ¬x = 0),
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
Tactic: by_cases x_zero : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have pos : Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) 0 ↔
  Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) 0
Tactic: simp_rw [x_zero, Submodule.zero_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
Tactic: rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg₁ : x.degree < (↑(n + 1) : WithBot ℕ) ↔ x.degree ≤ (↑n : WithBot ℕ)
Tactic: rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]