awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 - m + k) ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) key

Premises used: asymm, Iff.mp, add_lt_add_iff_left
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)

Premises used: asymm, And.left, Iff.mp, LT.lt.trans, Not, add_lt_add_iff_left
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)

Premises used: asymm, Iff.mp, LT.lt.trans, add_lt_add_iff_left
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 }
⊢ f (p * p.mirror) = f (q * q.mirror)

Tactic:
replace h := congr_arg f h
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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)
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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)
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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)))
⊢ 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

Premises used: Iff.mpr, Polynomial.isUnit_C, IsUnit.mul_right_inj, Units.isUnit
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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))
⊢ 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

Premises used: Units.ne_zero, Polynomial.binomial_eq_binomial
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
⊢ 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

Premises used: add_left_inj, Units.val_inj
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
inr₁ : ∀ (hm : m = n - m + k) (hm' : m' = n - m' + k), q = p ∨ q = p.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = 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 }
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ q = p ∨ q = p.mirror

Tactic:
Or.inl (hq.trans hp.symm)

Premises used: Or.inl, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = 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 }
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ q = p ∨ q = p.mirror

Tactic:
exact Or.inl (hq.trans hp.symm)

Premises used: Or.inl, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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'
inr : q = p.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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'
⊢ 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

Premises used: Units.ne_zero, Polynomial.mirror_eq_iff, eq_comm, Polynomial.trinomial_mirror
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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'
hp₁ : trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ) = p.mirror
⊢ n - (n - m' + k) + k = m'

Tactic:
rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp

Premises used: Units.ne_zero, Polynomial.mirror_eq_iff, eq_comm, Polynomial.trinomial_mirror
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ) = p.mirror
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror

Tactic:
hq.trans hp

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑u : ℤ) = p.mirror
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror

Tactic:
exact hq.trans hp

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ q = p ∨ q = p.mirror

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
⊢ (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff

Tactic:
have hmul := congr_arg leadingCoeff h
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
⊢ (↑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

Premises used: Polynomial.leadingCoeff_mul, Units.ne_zero, Polynomial.trinomial_trailingCoeff, Polynomial.mirror_leadingCoeff, Polynomial.trinomial_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
⊢ eval 1 (p * p.mirror) = eval 1 (q * q.mirror)

Tactic:
have hadd := congr_arg (eval 1) h
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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)
⊢ 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

Premises used: Polynomial.eval_mul, sq, Polynomial.mirror_eval_one
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
⊢ 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

Premises used: one_pow, Polynomial.eval_X_pow, Polynomial.eval_add, Polynomial.trinomial_def, mul_one, Polynomial.eval_C_mul
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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
⊢ 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

Premises used: Units.val, add_assoc, add_comm
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 (β := ℕ) ((↑v : ℤ) + ((↑w : ℤ) + (↑u : ℤ))) 2 = HPow.hPow (β := ℕ) ((↑v : ℤ) + ((↑z : ℤ) + (↑x : ℤ))) 2
⊢ 2 * (↑w : ℤ) * (↑u : ℤ) + 2 * (↑v : ℤ) * ((↑w : ℤ) + (↑u : ℤ)) =
    2 * (↑z : ℤ) * (↑x : ℤ) + 2 * (↑v : ℤ) * ((↑z : ℤ) + (↑x : ℤ))

Tactic:
simp only [add_sq', add_assoc, add_right_inj, ← Units.val_pow_eq_pow_val, Int.units_sq] at hadd

Premises used: add_assoc, Int.units_sq, Units.val_pow_eq_pow_val, add_right_inj, add_sq'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 :
  2 * (↑w : ℤ) * (↑u : ℤ) + 2 * (↑v : ℤ) * ((↑w : ℤ) + (↑u : ℤ)) =
    2 * (↑z : ℤ) * (↑x : ℤ) + 2 * (↑v : ℤ) * ((↑z : ℤ) + (↑x : ℤ))
⊢ (↑w : ℤ) + (↑u : ℤ) = (↑z : ℤ) + (↑x : ℤ)

Tactic:
rw [mul_assoc, hmul, ← mul_assoc, add_right_inj,
    mul_right_inj' (show 2 * (v : ℤ) ≠ 0 from mul_ne_zero two_ne_zero v.ne_zero)] at hadd

Premises used: mul_assoc, Units.ne_zero, two_ne_zero, mul_right_inj', mul_ne_zero, add_right_inj
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : (↑w : ℤ) + (↑u : ℤ) = (↑z : ℤ) + (↑x : ℤ)
⊢ (↑w : ℤ) = (↑z : ℤ) ∧ (↑u : ℤ) = (↑x : ℤ) ∨ (↑w : ℤ) = (↑x : ℤ) ∧ (↑u : ℤ) = (↑z : ℤ)

Tactic:
replace hadd :=
    (Int.isUnit_add_isUnit_eq_isUnit_add_isUnit w.isUnit u.isUnit z.isUnit x.isUnit).mp hadd
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : (↑w : ℤ) = (↑z : ℤ) ∧ (↑u : ℤ) = (↑x : ℤ) ∨ (↑w : ℤ) = (↑x : ℤ) ∧ (↑u : ℤ) = (↑z : ℤ)
⊢ w = z ∧ u = x ∨ w = x ∧ u = z

Tactic:
simp only [Units.val_inj] at hadd

Premises used: Units.val_inj
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : w = z ∧ u = x ∨ w = x ∧ u = z
inl :
  ∀ (hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) (hmul : (↑w : ℤ) * (↑u : ℤ) = (↑w : ℤ) * (↑u : ℤ)),
    q = p ∨ q = p.mirror
inr :
  ∀ (hq : q = trinomial k m' n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ)) (hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)),
    q = p ∨ q = p.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
rcases hadd with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑w : ℤ) * (↑u : ℤ)
⊢ q = p ∨ q = p.mirror

Tactic:
irreducible_aux2 hkm hmn hkm' hmn' u v w hp hq h

Premises used: Polynomial.IsUnitTrinomial.irreducible_aux2
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑w : ℤ) * (↑u : ℤ)
⊢ q = p ∨ q = p.mirror

Tactic:
exact irreducible_aux2 hkm hmn hkm' hmn' u v w hp hq h

Premises used: Polynomial.IsUnitTrinomial.irreducible_aux2
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
⊢ q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)

Tactic:
rw [← mirror_inj, trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero] at hq

Premises used: Units.ne_zero, Polynomial.trinomial_mirror, Polynomial.mirror_inj
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
hq₁ : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)

Tactic:
rw [← mirror_inj, trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero] at hq

Premises used: Units.ne_zero, Polynomial.trinomial_mirror, Polynomial.mirror_inj
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
⊢ p * p.mirror = q.mirror * q.mirror.mirror

Tactic:
rw [mul_comm q, ← q.mirror_mirror, q.mirror.mirror_mirror] at h

Premises used: Polynomial.mirror, mul_comm, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
h₁ : p * p.mirror = q.mirror * q.mirror.mirror
⊢ q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)

Tactic:
rw [mul_comm q, ← q.mirror_mirror, q.mirror.mirror_mirror] at h

Premises used: Polynomial.mirror, mul_comm, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
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 : ℤ)
h : p * p.mirror = q * q.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
h₁ : p * p.mirror = q.mirror * q.mirror.mirror
hq₁ : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)

Tactic:
rw [mul_comm q, ← q.mirror_mirror, q.mirror.mirror_mirror] at h

Premises used: Polynomial.mirror, mul_comm, Polynomial.mirror_mirror