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
⊢ 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]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
have rw : HAdd.hAdd (α := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X])) =
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
Tactic: rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
-- 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 :
  HAdd.hAdd (α := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X])) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
⊢ 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]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
have rw₁ : HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑w : ℤ)) : ℤ[X]) =
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
Tactic: rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
-- 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 :
  HAdd.hAdd (α := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X])) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₁ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑w : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
⊢ 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]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
have rw₂ : HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X]) =
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
Tactic: rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
-- 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 :
  HAdd.hAdd (α := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X])) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₁ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑w : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₂ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
⊢ 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]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
have rw₃ : HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X]) =
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
    ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
Tactic: rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
-- 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
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
have h : k + n < n + (n - m + k)
Tactic: refine ⟨?_, by gcongr⟩
-- 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
⊢ k + n < n + (n - m + k)
have h : n + k < n + (n - m + k)
Tactic: rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
-- 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
h : n + k < n + (n - m + k)
⊢ k + n < n + (n - m + k)
have h₁ : k < n - m + k
Tactic: rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
-- 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
h : n + k < n + (n - m + k)
h₁ : k < n - m + k
⊢ k + n < n + (n - m + k)
have h₂ : 0 < n - m
Tactic: rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
-- 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
⊢ m + n ∈ Set.Ioo (k + n) (n + n)
have h : k + n < m + n
Tactic: constructor
-- 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
h : k + n < m + n
⊢ m + n ∈ Set.Ioo (k + n) (n + n)
have h₁ : m + n < n + n
Tactic: constructor
-- 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
⊢ m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
have h : n + k ∉ Set.Ioo (n + k) (n + n)
Tactic: rw [← add_assoc, add_tsub_cancel_of_le hmn.le, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
h : p * p.mirror = q * q.mirror
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
⊢ q = p ∨ q = p.mirror
have h₁ : f (p * p.mirror) = f (q * q.mirror)
Tactic: replace h := congr_arg f h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : f (p * p.mirror) = f (q * q.mirror)
⊢ q = p ∨ q = p.mirror
have h₁ : 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))) =
  f (q * q.mirror)
Tactic: replace h := (irreducible_aux1 hkm hmn u v w hp).trans h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  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))) =
    f (q * q.mirror)
⊢ q = p ∨ q = p.mirror
have h₁ : 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))) =
  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)))
Tactic: replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  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))) =
    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)))
⊢ q = p ∨ q = p.mirror
have h₁ : 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)) =
  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))
Tactic: rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  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)) =
    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))
⊢ q = p ∨ q = p.mirror
have h₁ : m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
  (↑u : ℤ) = (↑w : ℤ) ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
    (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
Tactic: rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
    (↑u : ℤ) = (↑w : ℤ) ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
      (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
⊢ q = p ∨ q = p.mirror
have h₁ : m = m' ∧ n - m = n - m' ∨
  u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m = n - m + k ∧ m' = n - m' + k
Tactic: simp only [add_left_inj, Units.val_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m = m' ∧ n - m = n - m' ∨
    u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m = n - m + k ∧ m' = n - m' + k
⊢ q = p ∨ q = p.mirror
have inl : ∀ (hkm' : k < m) (hmn' : m < n) (hq : q = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)), q = p ∨ q = p.mirror
Tactic: rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
Cleared hypotheses: m', hkm', hmn', hq, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m = m' ∧ n - m = n - m' ∨
    u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m = n - m + k ∧ m' = n - m' + k
inl : ∀ (hkm' : k < m) (hmn' : m < n) (hq : q = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)), q = p ∨ q = p.mirror
⊢ q = p ∨ q = p.mirror
have inr : ∀ (hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)) (hkm : k < n - m' + k) (hmn : n - m' + k < n)
  (hp : p = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)) (h : n - (n - m' + k) + k = m'), q = p ∨ q = p.mirror
Tactic: rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
Cleared hypotheses: m, hkm, hmn, w, hp, hq, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  m = m' ∧ n - m = n - m' ∨
    u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ (↑u : ℤ) + (↑w : ℤ) = 0 ∧ m = n - m + k ∧ m' = n - m' + k
inl : ∀ (hkm' : k < m) (hmn' : m < n) (hq : q = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)), q = p ∨ q = p.mirror
inr :
  ∀ (hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)) (hkm : k < n - m' + k) (hmn : n - m' + k < n)
    (hp : p = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)) (h : n - (n - m' + k) + k = m'),
    q = p ∨ q = p.mirror
⊢ q = p ∨ q = p.mirror
have inr₁ : ∀ (hm : m = n - m + k) (hm' : m' = n - m' + k), q = p ∨ q = p.mirror
Tactic: rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)
h : n - (n - m' + k) + k = m'
⊢ q = p ∨ q = p.mirror
have inr : q = p.mirror
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] :=
  fun (p : ℤ[X]) ↦ { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ)
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror
have hp₁ : trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ) = p.mirror
Tactic: rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
⊢ q = p ∨ q = p.mirror
have hmul : (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff
Tactic: have hmul := congr_arg leadingCoeff h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
hmul : (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff
⊢ q = p ∨ q = p.mirror
have hmul₁ : (↑w : ℤ) * (↑u : ℤ) = (↑z : ℤ) * (↑x : ℤ)
Tactic: rw [leadingCoeff_mul, leadingCoeff_mul, mirror_leadingCoeff, mirror_leadingCoeff, hp, hq,
    trinomial_leadingCoeff hkm hmn w.ne_zero, trinomial_leadingCoeff hkm' hmn' z.ne_zero,
    trinomial_trailingCoeff hkm hmn u.ne_zero, trinomial_trailingCoeff hkm' hmn' x.ne_zero]
    at hmul
Cleared hypotheses: hmul
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑z : ℤ) * (↑x : ℤ)
⊢ q = p ∨ q = p.mirror
have hadd : eval 1 (p * p.mirror) = eval 1 (q * q.mirror)
Tactic: have hadd := congr_arg (eval 1) h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑z : ℤ) * (↑x : ℤ)
hadd : eval 1 (p * p.mirror) = eval 1 (q * q.mirror)
⊢ q = p ∨ q = p.mirror
have hadd₁ : HPow.hPow (β := ℕ) (eval 1 (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) 2 =
  HPow.hPow (β := ℕ) (eval 1 (trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ))) 2
Tactic: rw [eval_mul, eval_mul, mirror_eval_one, mirror_eval_one, ← sq, ← sq, hp, hq] at hadd
Cleared hypotheses: hadd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑z : ℤ) * (↑x : ℤ)
hadd :
  HPow.hPow (β := ℕ) (eval 1 (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) 2 =
    HPow.hPow (β := ℕ) (eval 1 (trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ))) 2
⊢ q = p ∨ q = p.mirror
have hadd₁ : HPow.hPow (β := ℕ) ((↑u : ℤ) + (↑v : ℤ) + (↑w : ℤ)) 2 = HPow.hPow (β := ℕ) ((↑x : ℤ) + (↑v : ℤ) + (↑z : ℤ)) 2
Tactic: simp only [eval_add, eval_C_mul, eval_X_pow, one_pow, mul_one, trinomial_def] at hadd
Cleared hypotheses: hadd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h : p * p.mirror = q * q.mirror
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑z : ℤ) * (↑x : ℤ)
hadd : HPow.hPow (β := ℕ) ((↑u : ℤ) + (↑v : ℤ) + (↑w : ℤ)) 2 = HPow.hPow (β := ℕ) ((↑x : ℤ) + (↑v : ℤ) + (↑z : ℤ)) 2
⊢ q = p ∨ q = p.mirror
have hadd₁ : HPow.hPow (β := ℕ) ((↑v : ℤ) + ((↑w : ℤ) + (↑u : ℤ))) 2 = HPow.hPow (β := ℕ) ((↑v : ℤ) + ((↑z : ℤ) + (↑x : ℤ))) 2
Tactic: rw [add_assoc, add_assoc, add_comm (u : ℤ), add_comm (x : ℤ), add_assoc, add_assoc] at hadd
Cleared hypotheses: hadd