-- Mathlib/NumberTheory/Dioph.lean
theorem sumsq_eq_zero (x) : ∀ l, sumsq l x = 0 ↔ l.Forall fun a : Poly α => a x = 0
  | [] => eq_self_iff_true _
  | p::ps => by
    rw [List.forall_cons, ← sumsq_eq_zero _ ps]; rw [sumsq]
    exact
      ⟨fun h : p x * p x + sumsq ps x = 0 =>
        have : p x = 0 :=
          eq_zero_of_mul_self_eq_zero <|
            le_antisymm
              (by
                rw [← h]
                have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)
                rwa [add_zero] at t)
              (mul_self_nonneg _)
        ⟨this, by simpa [this] using h⟩,
      fun ⟨h1, h2⟩ => by rw [add_apply, mul_apply, h1, h2]; rfl⟩

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ (sumsq (p :: ps)) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0

Tactic:
rw [sumsq]

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ (p * p + sumsq ps) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ (sumsq (p :: ps)) x = 0 ↔ List.Forall (fun a => a x = 0) (p :: ps)

Tactic:
rw [List.forall_cons, ← sumsq_eq_zero _ ps]

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ (sumsq (p :: ps)) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
⊢ p x * p x ≤ 0

Tactic:
rw [← h]

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
⊢ p x * p x ≤ p x * p x + (sumsq ps) x

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
⊢ p x * p x ≤ p x * p x + (sumsq ps) x

Tactic:
have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
t : p x * p x + 0 ≤ p x * p x + (sumsq ps) x
⊢ p x * p x ≤ p x * p x + (sumsq ps) x

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ (p * p + sumsq ps) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0

Tactic:
exact
  ⟨fun h : p x * p x + sumsq ps x = 0 =>
    have : p x = 0 :=
      eq_zero_of_mul_self_eq_zero <|
        le_antisymm
          (by
            rw [← h]
            have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)
            rwa [add_zero] at t)
          (mul_self_nonneg _)
    ⟨this, by simpa [this] using h⟩,
  fun ⟨h1, h2⟩ => by rw [add_apply, mul_apply, h1, h2]; rfl⟩

Result:
no goals

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
this : p x = 0
⊢ (sumsq ps) x = 0

Tactic:
simpa [this] using h

Result:
no goals

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
x✝ : p x = 0 ∧ (sumsq ps) x = 0
h1 : p x = 0
h2 : (sumsq ps) x = 0
⊢ 0 * 0 + 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : p x * p x + (sumsq ps) x = 0
t : p x * p x + 0 ≤ p x * p x + (sumsq ps) x
⊢ p x * p x ≤ p x * p x + (sumsq ps) x

Tactic:
rwa [add_zero] at t

Result:
no goals

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
x✝ : p x = 0 ∧ (sumsq ps) x = 0
h1 : p x = 0
h2 : (sumsq ps) x = 0
⊢ (p * p + sumsq ps) x = 0

Tactic:
rw [add_apply, mul_apply, h1, h2]

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
x✝ : p x = 0 ∧ (sumsq ps) x = 0
h1 : p x = 0
h2 : (sumsq ps) x = 0
⊢ 0 * 0 + 0 = 0