awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₅ : m + k ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
h₅ : m + k ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₆ : k + n ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
h₅ : m + k ∉ Set.Ioo (k + n) (n + n)
h₆ : k + n ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₇ : k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
h : n + n ∉ Set.Ioo (k + n) (n + n)
h₁ : n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
h₂ : n + k ∉ Set.Ioo (k + n) (n + n)
h₃ : m + n ∈ Set.Ioo (k + n) (n + n)
h₄ : m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
h₅ : m + k ∉ Set.Ioo (k + n) (n + n)
h₆ : k + n ∉ Set.Ioo (k + n) (n + n)
h₇ : k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
have h₈ : k + k ∉ Set.Ioo (k + n) (n + n)
Tactic: rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
    Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }
have simp : HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
  {
    toFinsupp :=
      HAdd.hAdd (α := ℕ →₀ ℤ) (Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))
        (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) }
Tactic: simp only [add_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) (Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))
          (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) }
have rw : HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
  HAdd.hAdd (α := ℤ[X]) { toFinsupp := Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)) }
    { toFinsupp := Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)) }
Tactic: rw [ofFinsupp_add]