awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial
have hy₁ : IsUnit (x * 0 + y + z * 0)
Tactic: rw [if_neg hkm.ne', if_neg hmn.ne] at hy
Cleared hypotheses: hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial
have hz₁ : IsUnit (x * 0 + y * 0 + z)
Tactic: rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial
have hz₁ : IsUnit z
Tactic: simp_rw [mul_zero, zero_add, add_zero] at hx hy hz
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
hz₁ : IsUnit z
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial
have hx₁ : IsUnit x
Tactic: simp_rw [mul_zero, zero_add, add_zero] at hx hy hz
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
hz₁ : IsUnit z
hx₁ : IsUnit x
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial
have hy₁ : IsUnit y
Tactic: simp_rw [mul_zero, zero_add, add_zero] at hx hy hz
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3
have rw : p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
Tactic: rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add,
    Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
have refine_1 : p.IsUnitTrinomial → Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
Tactic: refine ⟨?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
refine_1 : p.IsUnitTrinomial → Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
⊢ p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
have refine_2 : ∀ (hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3), p.IsUnitTrinomial
Tactic: refine ⟨?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ Eq (α := ℤ) (sum (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
have refine_1 : HPow.hPow (β := ℕ) (↑u : ℤ) 2 + (HPow.hPow (β := ℕ) (↑v : ℤ) 2 + HPow.hPow (β := ℕ) (↑w : ℤ) 2) = 3
Tactic: rw [sum_def, trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,
      sum_insert (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
      sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn,
      trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ HPow.hPow (β := ℕ) (↑u : ℤ) 2 + (HPow.hPow (β := ℕ) (↑v : ℤ) 2 + HPow.hPow (β := ℕ) (↑w : ℤ) 2) = 3
have refine_1 : 1 + HAdd.hAdd (α := ℤ) 1 1 = 3
Tactic: simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq, Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
⊢ p.IsUnitTrinomial
have key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
Tactic: have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
      Int.sq_eq_one_of_sq_le_three
        ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ p.IsUnitTrinomial
have refine_2 : #p.support = 3
Tactic: refine isUnitTrinomial_iff.mpr ⟨?_, fun k hk => .of_pow_eq_one (key k hk) two_ne_zero⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ #p.support = 3
have hp₁ : Eq (α := ℤ) (↑(#p.support) : ℤ) 3
Tactic: rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_cast] at hp
Cleared hypotheses: hp, key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial
have rw : (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial
Tactic: rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
rw : (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial
have rw₁ : (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔
  (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
Tactic: rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
rw : (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial
rw₁ :
  (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial
have rw₂ : (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3 ↔
  (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
Tactic: rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]
-- 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 : ℤ)
⊢ n - m + k < n
have rwa : n - m < n - k
Tactic: rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }
have key : n - m + k < n
Tactic: have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
-- 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]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }
have rw : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
    (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
  {
    toFinsupp :=
      Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
        (HMul.hMul (α := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
            (trinomial k (n - m + k) n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ))).toFinsupp }
Tactic: rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]
-- 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]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    {
      toFinsupp :=
        Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
          (HMul.hMul (α := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
              (trinomial k (n - m + k) n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ))).toFinsupp }
have simp_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 (α := ℕ →₀ ℤ)
              (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 : ℤ)))) }
Tactic: simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial,
    toFinsupp_add, toFinsupp_monomial, AddMonoidAlgebra, Finsupp.filter_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.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 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) }
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) }
⊢ 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 + 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)
⊢ 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 + (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]