p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ (sum p fun n x => x ^ 2) = 3
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ coeff (p * mirror p) ((natDegree (p * mirror p) + natTrailingDegree (p * mirror p)) / 2) = 3
rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add,
  Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]
case refine'_1
p q : ℤ[X]
⊢ IsUnitTrinomial p → (sum p fun n x => x ^ 2) = 3

case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
⊢ IsUnitTrinomial p
p q : ℤ[X]
⊢ IsUnitTrinomial p ↔ (sum p fun n x => x ^ 2) = 3
refine' ⟨_, fun hp => _⟩
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (sum (trinomial k m n ↑u ↑v ↑w) fun n x => x ^ 2) = 3
case refine'_1
p q : ℤ[X]
⊢ IsUnitTrinomial p → (sum p fun n x => x ^ 2) = 3
rintro ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (sum (trinomial k m n ↑u ↑v ↑w) fun n x => x ^ 2) = 3
rw [sum_def, trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,
  sum_insert (mt mem_insert.mp (not_or_of_not 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]
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3
simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq]
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ IsUnitTrinomial p
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
⊢ IsUnitTrinomial p
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)
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ IsUnitTrinomial p
refine' isUnitTrinomial_iff.mpr ⟨_, fun k hk => isUnit_ofPowEqOne (key k hk) two_ne_zero⟩
case refine'_2
p q : ℤ[X]
hp : ↑(card (support p)) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
case refine'_2
p q : ℤ[X]
hp : (sum p fun n x => x ^ 2) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_coe] at hp
no goals
case refine'_2
p q : ℤ[X]
hp : ↑(card (support p)) = 3
key : ∀ (k : ℕ), k ∈ support p → coeff p k ^ 2 = 1
⊢ card (support p) = 3
exact Nat.cast_injective hp