awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
inr : q.mirror = p ∨ q.mirror = p.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
rw [← mirror_inj, or_comm, ← mirror_eq_iff]

Premises used: Polynomial.mirror_eq_iff, or_comm, 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.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
⊢ q.mirror = p ∨ q.mirror = p.mirror

Tactic:
irreducible_aux2 hkm hmn (lt_add_of_pos_left k (tsub_pos_of_lt hmn'))
        (lt_tsub_iff_right.mp ((tsub_lt_tsub_iff_left_of_le hmn'.le).mpr hkm')) u v w hp hq h

Premises used: Iff.mpr, lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le, LT.lt.le, Iff.mp, lt_add_of_pos_left, Polynomial.IsUnitTrinomial.irreducible_aux2, tsub_pos_of_lt
-- 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.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
hmul : (↑w : ℤ) * (↑u : ℤ) = (↑u : ℤ) * (↑w : ℤ)
⊢ q.mirror = p ∨ q.mirror = p.mirror

Tactic:
exact
      irreducible_aux2 hkm hmn (lt_add_of_pos_left k (tsub_pos_of_lt hmn'))
        (lt_tsub_iff_right.mp ((tsub_lt_tsub_iff_left_of_le hmn'.le).mpr hkm')) u v w hp hq h

Premises used: Iff.mpr, lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le, LT.lt.le, Iff.mp, lt_add_of_pos_left, Polynomial.IsUnitTrinomial.irreducible_aux2, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
⊢ Irreducible p

Tactic:
irreducible_of_mirror hp.not_isUnit (fun q hpq => ?_) h

Premises used: Polynomial.irreducible_of_mirror, Polynomial.IsUnitTrinomial.not_isUnit
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
refine : ∀ (q : ℤ[X]) (hpq : p * p.mirror = q * q.mirror), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ Irreducible p

Tactic:
refine irreducible_of_mirror hp.not_isUnit (fun q hpq => ?_) h

Premises used: Polynomial.irreducible_of_mirror, Polynomial.IsUnitTrinomial.not_isUnit
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
⊢ q.IsUnitTrinomial

Tactic:
have hq : IsUnitTrinomial q := (isUnitTrinomial_iff'' hpq).mp hp
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
hq : q.IsUnitTrinomial
obtain :
  ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ) (hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)),
    q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
hq : q.IsUnitTrinomial
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
obtain :
  ∀ (k' m' n' : ℕ) (hkm' : k' < m') (hmn' : m' < n') (x y z : ℤˣ)
    (hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
obtain ⟨k', m', n', hkm', hmn', x, y, z, hq⟩ := hq
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
rw : 2 * k = 2 * k'
rw₁ : 2 * natTrailingDegree (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) = 2 * k'
rw₂ rw₃ : ℤ
rw₄ : 2 * p.natTrailingDegree = 2 * k'
rw₅ : (p * p.mirror).natTrailingDegree = 2 * k'
rw₆ : (q * q.mirror).natTrailingDegree = 2 * k'
rw₇ : 2 * q.natTrailingDegree = 2 * k'
rw₈ : 2 * natTrailingDegree (trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)) = 2 * k'
rw₉ rw₁₀ : 2 * k' = 2 * k'
⊢ k = k'

Tactic:
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]

Premises used: Polynomial.trinomial_natTrailingDegree, Polynomial.natTrailingDegree_mul_mirror, Units.ne_zero, two_ne_zero, mul_right_inj'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
⊢ k = k'

Tactic:
have hk : k = k' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hk : k = k'
rw : 2 * n = 2 * n'
rw₁ : 2 * natDegree (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) = 2 * n'
rw₂ rw₃ : ℤ
rw₄ : 2 * p.natDegree = 2 * n'
rw₅ : (p * p.mirror).natDegree = 2 * n'
rw₆ : (q * q.mirror).natDegree = 2 * n'
rw₇ : 2 * q.natDegree = 2 * n'
rw₈ : 2 * natDegree (trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)) = 2 * n'
rw₉ rw₁₀ : 2 * n' = 2 * n'
⊢ n = n'

Tactic:
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ←
      hp, ← natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq,
      trinomial_natDegree hkm' hmn' z.ne_zero]

Premises used: Polynomial.natDegree_mul_mirror, Polynomial.trinomial_natDegree, Units.ne_zero, two_ne_zero, mul_right_inj'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hk : k = k'
⊢ n = n'

Tactic:
have hn : n = n' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ←
      hp, ← natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq,
      trinomial_natDegree hkm' hmn' z.ne_zero]
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hk : k = k'
hn : n = n'
⊢ k < m'

Tactic:
subst hk
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hk : k = k'
hn : n = n'
hkm'₁ : k < m'
⊢ q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)

Tactic:
subst hk
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
⊢ m' < n

Tactic:
subst hn
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hmn'₁ : m' < n
⊢ q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)

Tactic:
subst hn
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
inl : ∀ (h1 : (↑y : ℤ) = (↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
inr : ∀ (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)

Premises used: Units.val, eq_or_eq_neg_of_sq_eq_sq, Int.isUnit_sq, Units.isUnit, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
⊢ q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)

Tactic:
rw [h1] at hq
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
hq₁ : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
⊢ (↑y : ℤ) = (↑v : ℤ)

Tactic:
rw [h1] at hq
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
inl : ∀ (h2 : q = p), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
inl₁ : ∀ (h2 : q = p.mirror), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)

Premises used: Polynomial.IsUnitTrinomial.irreducible_aux3
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
h2 : q = p
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
Or.inl h2

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
h2 : q = p
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
exact Or.inl h2

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
h2 : q = p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
Or.inr (Or.inr (Or.inl h2))

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
h2 : q = p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
exact Or.inr (Or.inr (Or.inl h2))

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)

Tactic:
rw [h1] at hq
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
hq₁ : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
⊢ (↑y : ℤ) = -(↑v : ℤ)

Tactic:
rw [h1] at hq
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
inr :
  ∀
    (hp :
      p =
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
            HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
    (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
    (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [trinomial_def] at hp

Premises used: Polynomial.trinomial_def
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
inr :
  ∀
    (hp :
      -p =
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
            HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
    (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
    (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp

Premises used: neg_add, neg_inj, neg_mul, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
inr :
  ∀ (hpq : -p * (-p).mirror = q * q.mirror) (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ)
    (hp :
      -p =
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
            HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
    (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
    (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [← neg_mul_neg, ← mirror_neg] at hpq

Premises used: Polynomial.mirror_neg, neg_mul_neg
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : -p * (-p).mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
inr :
  ∀ (hpq : -p * (-p).mirror = -p * (-p).mirror) (hq : -p = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)),
    -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror
inr₁ :
  ∀ (hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror)
    (hq : (-p).mirror = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)),
    (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)

Premises used: Polynomial.IsUnitTrinomial.irreducible_aux3, Neg.neg, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : (↑y : ℤ) = -(↑v : ℤ)
hpq : -p * (-p).mirror = -p * (-p).mirror
hq : -p = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
⊢ -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror

Tactic:
Or.inr (Or.inl rfl)

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : (↑y : ℤ) = -(↑v : ℤ)
hpq : -p * (-p).mirror = -p * (-p).mirror
hq : -p = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
⊢ -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror

Tactic:
exact Or.inr (Or.inl rfl)

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : (↑y : ℤ) = -(↑v : ℤ)
hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror
hq : (-p).mirror = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
⊢ (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror

Tactic:
Or.inr (Or.inr (Or.inr p.mirror_neg))

Premises used: Polynomial.mirror_neg, Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : (↑y : ℤ) = -(↑v : ℤ)
hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror
hq : (-p).mirror = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
⊢ (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror

Tactic:
exact Or.inr (Or.inr (Or.inr p.mirror_neg))

Premises used: Polynomial.mirror_neg, Or.inr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsCoprime p p.mirror
⊢ Irreducible p

Tactic:
irreducible_of_coprime hp fun _ => h.isUnit_of_dvd'

Premises used: Polynomial.IsUnitTrinomial.irreducible_of_coprime, IsCoprime.isUnit_of_dvd'
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α₁ : Type u_2
rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop
δ : P₁ → Prop
q : P₁
h : ∀ (a : FreeMonoid α₁), δ ((mk rels₁ : (a : FreeMonoid α₁) → P₁) a)
⊢ δ q

Tactic:
Quotient.ind h q

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop
rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop
δ : P₁ → P₂ → Prop
q₁ : P₁
q₂ : P₂
h :
  ∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂),
    δ ((mk rels₁ : (a : FreeMonoid α₁) → P₁) a) ((mk rels₂ : (a : FreeMonoid α₂) → P₂) b)
⊢ δ q₁ q₂

Tactic:
Quotient.inductionOn₂ q₁ q₂ h

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α₁ : Type u_2
α₂ : Type u_3
α₃ : Type u_4
rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop
rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop
rels₃ : FreeMonoid α₃ → FreeMonoid α₃ → Prop
δ : P₁ → P₂ → P₃ → Prop
q₁ : P₁
q₂ : P₂
q₃ : P₃
h :
  ∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂) (c : FreeMonoid α₃),
    δ ((mk rels₁ : (a : FreeMonoid α₁) → P₁) a) ((mk rels₂ : (a : FreeMonoid α₂) → P₂) b)
      ((mk rels₃ : (a : FreeMonoid α₃) → P₃) c)
⊢ δ q₁ q₂ q₃

Tactic:
Quotient.inductionOn₃ q₁ q₂ q₃ h

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
⊢ Eq (α := PresentedMonoid rels) ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) x : PresentedMonoid rels)
      ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) y : PresentedMonoid rels) ↔
    (conGen rels : (a : FreeMonoid α) → FreeMonoid α → Prop) x y

Tactic:
Quotient.eq

Premises used: PresentedMonoid, Con.Quotient, Quotient.eq