-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem isUnitTrinomial_iff' :
    p.IsUnitTrinomial ↔
      (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) =
        3

Proof state:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

Tactic:
rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add,
  Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]

Result:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p.sum fun x x => x ^ 2) = 3

Proof state:
case refine_2
p : ℤ[X]
hp : ↑(#p.support) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Tactic:
exact Nat.cast_injective hp

Result:
no goals

Proof state:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p.sum fun x x => x ^ 2) = 3

Tactic:
refine ⟨?_, fun hp => ?_⟩

Result:
case refine_1
p : ℤ[X]
⊢ p.IsUnitTrinomial → (p.sum fun x x => x ^ 2) = 3

case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
⊢ p.IsUnitTrinomial

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ((trinomial k m n ↑u ↑v ↑w).sum fun x x => x ^ 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]

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3

Proof state:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Tactic:
rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_cast] at hp

Result:
case refine_2
p : ℤ[X]
hp : ↑(#p.support) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Proof state:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
⊢ p.IsUnitTrinomial

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)

Result:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ p.IsUnitTrinomial

Proof state:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ p.IsUnitTrinomial

Tactic:
refine isUnitTrinomial_iff.mpr ⟨?_, fun k hk => .of_pow_eq_one (key k hk) two_ne_zero⟩

Result:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x => x ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3

Tactic:
simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq, Units.val_one]

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ 1 + (1 + 1) = 3

Proof state:
case refine_1
p : ℤ[X]
⊢ p.IsUnitTrinomial → (p.sum fun x x => x ^ 2) = 3

Tactic:
rintro ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ((trinomial k m n ↑u ↑v ↑w).sum fun x x => x ^ 2) = 3

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ 1 + (1 + 1) = 3

Tactic:
decide

Result:
no goals