-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n)
    (u v w : Units ℤ) (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) : q = p ∨ q = p.mirror

Proof state:
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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:
refine Or.inr ?_

Result:
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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

Proof state:
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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

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

Result:
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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

Proof state:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = C ↑v * (C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n))
⊢ q = p ∨ q = p.mirror

Tactic:
rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h

Result:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n) = C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n)
⊢ q = p ∨ q = p.mirror

Proof state:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ m = m'

Tactic:
omega

Result:
no goals

Proof state:
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 => { 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

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

Result:
case inl.intro
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 => { 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

case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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

case inr.inr.intro.intro
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 => { 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

Proof state:
case inr.inr.intro.intro
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 => { 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:
obtain rfl : m = m' := by omega

Result:
case inr.inr.intro.intro
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
hm : m = n - m + k
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n ↑u ↑v ↑w
hm' : m = n - m + k
⊢ q = p ∨ q = p.mirror

Proof state:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = f (q * q.mirror)
⊢ q = p ∨ q = p.mirror

Tactic:
replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm

Result:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h :
  C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = C ↑v * (C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n))
⊢ q = p ∨ q = p.mirror

Proof state:
case inr.inl.intro.intro
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] := fun p => { 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

Result:
no goals

Proof state:
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 => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }
h : C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n) = C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n)
⊢ q = p ∨ q = p.mirror

Tactic:
rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h

Result:
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 => { 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