awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
⊢ Subset (α := Finset R) (coeffs 1) {1}
have simp_rw : ∀ x ∈ support.{u} (R := R) 1, Membership.mem (γ := Finset R) {1} (coeff 1 x)
Tactic: simp_rw [coeffs, Finset.image_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
⊢ Subset (α := Finset R) (coeffs 1) {1}
have simp_rw : Subset (α := Finset R) (image (fun (n : ℕ) ↦ coeff 1 n) (support.{u} (R := R) 1)) {1}
Tactic: classical
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
simp_rw : Subset (α := Finset R) (image (fun (n : ℕ) ↦ coeff 1 n) (support.{u} (R := R) 1)) {1}
⊢ Subset (α := Finset R) (coeffs 1) {1}
have simp_rw₁ : ∀ x ∈ support.{u} (R := R) 1, Membership.mem (γ := Finset R) {1} (coeff 1 x)
Tactic: classical
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ p.coeff n ∈ p.coeffs
have simp : ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n
Tactic: simp only [coeffs, mem_support_iff, Finset.mem_image, Ne]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ p.coeff n ∈ p.coeffs
have simp : ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n
Tactic: classical
  simp only [coeffs, mem_support_iff, Finset.mem_image, Ne]
  exact ⟨n, h, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeffs = ∅ ↔ p = 0
have refine : p.coeffs = ∅ → p = 0
Tactic: refine ⟨?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeffs = ∅ → p = 0
have contrapose! : p ≠ 0 → p.coeffs.Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.coeffs.Nonempty
have h₁ : p.support.Nonempty
Tactic: rw [← support_nonempty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty
have obtain : ∀ (n : ℕ) (hn : n ∈ p.support), p.coeffs.Nonempty
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ p.support
⊢ p.coeffs.Nonempty
have hn₁ : p.coeff n ≠ 0
Tactic: rw [mem_support_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ Eq (α := Finset R) (coeffs ((monomial n : (a : R) → R[X]) c)) {c}
have rw : Eq (α := Finset R) (image (fun (n_1 : ℕ) ↦ coeff ((monomial n : (a : R) → R[X]) c) n_1) {n}) {c}
Tactic: rw [coeffs, support_monomial n hc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
⊢ (-p).coeff n = -p.coeff n
have rcases : ∀ (toFinsupp : R[ℕ]), (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
have rw : { toFinsupp := -toFinsupp : R[X] }.coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
Tactic: rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
⊢ (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
have rw₁ : (-toFinsupp : (a : ℕ) → R) n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
Tactic: rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
rw₁ : (-toFinsupp : (a : ℕ) → R) n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
⊢ (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
have rw₂ : Eq (α := R) ((-toFinsupp : (a : ℕ) → R) n : R) (-(toFinsupp : (a : ℕ) → R) n : R)
Tactic: rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
rw₁ : (-toFinsupp : (a : ℕ) → R) n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
rw₂ : Eq (α := R) ((-toFinsupp : (a : ℕ) → R) n : R) (-(toFinsupp : (a : ℕ) → R) n : R)
⊢ (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
have rw₃ : Eq (α := R) (-(toFinsupp : (a : ℕ) → R) n : R) (-(toFinsupp : (a : ℕ) → R) n : R)
Tactic: rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n
have rcases : ∀ (toFinsupp : R[ℕ]),
  ({ toFinsupp := toFinsupp : R[X] } - q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n - q.coeff n
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
q : R[X]
n : ℕ
toFinsupp : R[ℕ]
⊢ ({ toFinsupp := toFinsupp : R[X] } - q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n - q.coeff n
have rcases : ∀ (toFinsupp_1 : R[ℕ]),
  ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
Tactic: rcases q with ⟨⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
⊢ ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have rw : { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
  { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
Tactic: rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
rw :
  { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
⊢ ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have rw₁ : (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
  { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
Tactic: rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
rw :
  { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₁ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
⊢ ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have rw₂ : (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
  HSub.hSub (α := R) ((toFinsupp : (a : ℕ) → R) n : R) ({ toFinsupp := toFinsupp_1 : R[X] }.coeff n)
Tactic: rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
rw :
  { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₁ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₂ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    HSub.hSub (α := R) ((toFinsupp : (a : ℕ) → R) n : R) ({ toFinsupp := toFinsupp_1 : R[X] }.coeff n)
⊢ ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have rw₃ : (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
  HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
Tactic: rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
rw :
  { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₁ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₂ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    HSub.hSub (α := R) ((toFinsupp : (a : ℕ) → R) n : R) ({ toFinsupp := toFinsupp_1 : R[X] }.coeff n)
rw₃ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
⊢ ({ toFinsupp := toFinsupp : R[X] } - { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have rw₄ : HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R) =
  HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
Tactic: rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
a : R
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) (-(monomial n : (a : R) → R[X]) a : R[X])
have rw : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) =
  0
Tactic: rw [eq_neg_iff_add_eq_zero, ← map_add, neg_add_cancel, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
a : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X])
      ((monomial n : (a : R) → R[X]) a : R[X]) =
    0
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) (-(monomial n : (a : R) → R[X]) a : R[X])
have rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a + a) : R[X]) (0 : R[X])
Tactic: rw [eq_neg_iff_add_eq_zero, ← map_add, neg_add_cancel, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
a : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X])
      ((monomial n : (a : R) → R[X]) a : R[X]) =
    0
rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a + a) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) (-(monomial n : (a : R) → R[X]) a : R[X])
have rw₂ : Eq.{u + 1} (α := R[X]) ((monomial n : (a : R) → R[X]) 0) 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← map_add, neg_add_cancel, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
a : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X])
      ((monomial n : (a : R) → R[X]) a : R[X]) =
    0
rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a + a) : R[X]) (0 : R[X])
rw₂ : Eq.{u + 1} (α := R[X]) ((monomial n : (a : R) → R[X]) 0) 0
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) (-(monomial n : (a : R) → R[X]) a : R[X])
have rw₃ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← map_add, neg_add_cancel, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
inst : Ring R
n : ℕ
⊢ (monomial n : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
have rw : (monomial n : (a : R) → R[X]) (a + -b) =
  HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
Tactic: rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
inst : Ring R
n : ℕ
rw :
  (monomial n : (a : R) → R[X]) (a + -b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
⊢ (monomial n : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
have rw₁ : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) (-b) : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
Tactic: rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
inst : Ring R
n : ℕ
rw :
  (monomial n : (a : R) → R[X]) (a + -b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
      ((monomial n : (a : R) → R[X]) (-b) : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
⊢ (monomial n : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
have rw₂ : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
Tactic: rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
inst : Ring R
n : ℕ
rw :
  (monomial n : (a : R) → R[X]) (a + -b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
      ((monomial n : (a : R) → R[X]) (-b) : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₂ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
⊢ (monomial n : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
have rw₃ : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X])
Tactic: rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).support = p.support
have rcases : ∀ (toFinsupp : R[ℕ]), (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
toFinsupp : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
have rw : { toFinsupp := -toFinsupp : R[X] }.support = { toFinsupp := toFinsupp : R[X] }.support
Tactic: rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.support = { toFinsupp := toFinsupp : R[X] }.support
⊢ (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
have rw₁ : (-toFinsupp).support = { toFinsupp := toFinsupp : R[X] }.support
Tactic: rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.support = { toFinsupp := toFinsupp : R[X] }.support
rw₁ : (-toFinsupp).support = { toFinsupp := toFinsupp : R[X] }.support
⊢ (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
have rw₂ : (-toFinsupp).support = toFinsupp.support
Tactic: rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.support = { toFinsupp := toFinsupp : R[X] }.support
rw₁ : (-toFinsupp).support = { toFinsupp := toFinsupp : R[X] }.support
rw₂ : (-toFinsupp).support = toFinsupp.support
⊢ (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
have rw₃ : toFinsupp.support = toFinsupp.support
Tactic: rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (hypothesis)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
⊢ Nontrivial.{u} R[X]
have h : Nontrivial.{u} R[ℕ]
Tactic: have h : Nontrivial R[ℕ] := by infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
⊢ Nontrivial.{u} R[X]
have rcases : ∀ (x y : R[ℕ]) (hxy : x ≠ y), Nontrivial.{u} R[X]
Tactic: rcases h.exists_pair_ne with ⟨x, y, hxy⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ Nontrivial.{u} R[X]
have refine : { toFinsupp := x : R[X] } ≠ { toFinsupp := y }
Tactic: refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = (C : (a : R) → R[X]) (↑q : R) * f
have rw : q • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) q 1) : R[X]) f
Tactic: rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionSemiring R
q : ℚ≥0
f : R[X]
rw : q • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) q 1) : R[X]) f
⊢ q • f = (C : (a : R) → R[X]) (↑q : R) * f
have rw₁ : q • f = HSMul.hSMul (β := R[X]) q ((C : (a : R) → R[X]) 1) * f
Tactic: rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionSemiring R
q : ℚ≥0
f : R[X]
rw : q • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) q 1) : R[X]) f
rw₁ : q • f = HSMul.hSMul (β := R[X]) q ((C : (a : R) → R[X]) 1) * f
⊢ q • f = (C : (a : R) → R[X]) (↑q : R) * f
have rw₂ : q • f = HSMul.hSMul (β := R[X]) q 1 * f
Tactic: rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionSemiring R
q : ℚ≥0
f : R[X]
rw : q • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) q 1) : R[X]) f
rw₁ : q • f = HSMul.hSMul (β := R[X]) q ((C : (a : R) → R[X]) 1) * f
rw₂ : q • f = HSMul.hSMul (β := R[X]) q 1 * f
⊢ q • f = (C : (a : R) → R[X]) (↑q : R) * f
have rw₃ : q • f = q • f
Tactic: rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = (C : (a : R) → R[X]) (↑a : R) * f
have rw : a • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X]) f
Tactic: rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionRing R
a : ℚ
f : R[X]
rw : a • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X]) f
⊢ a • f = (C : (a : R) → R[X]) (↑a : R) * f
have rw₁ : a • f = HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) 1) * f
Tactic: rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionRing R
a : ℚ
f : R[X]
rw : a • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X]) f
rw₁ : a • f = HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) 1) * f
⊢ a • f = (C : (a : R) → R[X]) (↑a : R) * f
have rw₂ : a • f = HSMul.hSMul (β := R[X]) a 1 * f
Tactic: rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : DivisionRing R
a : ℚ
f : R[X]
rw : a • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X]) f
rw₁ : a • f = HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) 1) * f
rw₂ : a • f = HSMul.hSMul (β := R[X]) a 1 * f
⊢ a • f = (C : (a : R) → R[X]) (↑a : R) * f
have rw₃ : a • f = a • f
Tactic: rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)
have h0 : natDegree.{u_1} (R := S) 0 ≤ 0
Tactic: apply List.sum_le_foldr_max natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
h0 : natDegree.{u_1} (R := S) 0 ≤ 0
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)
have hadd : ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree
Tactic: apply List.sum_le_foldr_max natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
have none : ∀ (hd : ∀ k ∈ s, (f k).degree = none), Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
Tactic: obtain _ | d := d
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
none :
  ∀ (hd : ∀ k ∈ s, (f k).degree = Option.none),
    Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
have some : ∀ (d : ℕ) (hd : ∀ k ∈ s, (f k).degree = some d),
  Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
Tactic: obtain _ | d := d
Cleared hypotheses: d, hd