awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
⊢ False
have neg : ∀ (w x y z : ℤ) (hw : (↑m : ℤ) ∣ w) (hx : (↑m : ℤ) ∣ x) (hy : (↑m : ℤ) ∣ y) (hz : (↑m : ℤ) ∣ z)
  (h :
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
      HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)),
  False
Tactic: rsuffices ⟨w, x, y, z, hw, hx, hy, hz, h⟩ : ∃ w x y z : ℤ, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧
      w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
neg :
  ∀ (w x y z : ℤ) (hw : (↑m : ℤ) ∣ w) (hx : (↑m : ℤ) ∣ x) (hy : (↑m : ℤ) ∣ y) (hz : (↑m : ℤ) ∣ z)
    (h :
      HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
        HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)),
    False
⊢ False
have rsuffices : ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
  (↑m : ℤ) ∣ w ∧
    (↑m : ℤ) ∣ x ∧
      (↑m : ℤ) ∣ y ∧
        (↑m : ℤ) ∣ z ∧
          HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
            HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
Tactic: rsuffices ⟨w, x, y, z, hw, hx, hy, hz, h⟩ : ∃ w x y z : ℤ, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧
      w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
⊢ HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2 =
    (↑(r * p) : ℤ)
have refine : HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 *
    (HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2) =
  HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 * (↑(r * p) : ℤ)
Tactic: refine mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
| HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 * (↑(r * p) : ℤ)
have rw : HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2
Tactic: rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 *
      (HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
        HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 * (↑(r * p) : ℤ)
have conv_rhs : HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 *
    (HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2) =
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2
Tactic: conv_rhs => rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
⊢ False
have this₁ : HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
    HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2 =
  (↑(r * p) : ℤ)
Tactic: have : (w / m) ^ 2 + (x / m) ^ 2 + (y / m) ^ 2 + (z / m) ^ 2 = ↑(r * p) := by
        refine mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_
        conv_rhs => rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]
        simp only [mul_add, ← mul_pow, Int.mul_ediv_cancel', *]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
this :
  HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2 =
    (↑(r * p) : ℤ)
⊢ False
have this₁ : HPow.hPow (β := ℕ) (w / (↑m : ℤ)).natAbs 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)).natAbs 2 +
      HPow.hPow (β := ℕ) (y / (↑m : ℤ)).natAbs 2 +
    HPow.hPow (β := ℕ) (z / (↑m : ℤ)).natAbs 2 =
  r * p
Tactic: rw [← natAbs_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
⊢ HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
have rw : HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f d).natAbs 2 +
    HPow.hPow (β := ℕ) (f c).natAbs 2 =
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
    HPow.hPow (β := ℕ) (f d).natAbs 2
Tactic: rw [← natAbs_iff, natAbs_neg, ← hr]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    (↑m : ℤ) ∣ w ∧
      (↑m : ℤ) ∣ x ∧
        (↑m : ℤ) ∣ y ∧
          (↑m : ℤ) ∣ z ∧
            HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
              HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
have hr₁ : HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
  (↑(m * r) : ℤ)
Tactic: replace hr : (f b) ^ 2 + (f a) ^ 2 + (f d) ^ 2 + (-f c) ^ 2 = ↑(m * r) := by
      rw [← natAbs_iff, natAbs_neg, ← hr]
      ac_rfl
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    (↑m : ℤ) ∣ w ∧
      (↑m : ℤ) ∣ x ∧
        (↑m : ℤ) ∣ y ∧
          (↑m : ℤ) ∣ z ∧
            HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
              HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
have this₁ : Eq (α := ℤ)
  ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ))
    (HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2)
    (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2))
  ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ)) (↑(m * r) : ℤ) (m * p))
Tactic: have := congr_arg₂ (· * Nat.cast ·) hr habcd
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  Eq (α := ℤ)
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ))
      (HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 +
        HPow.hPow (β := ℕ) (-f c) 2)
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2))
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ)) (↑(m * r) : ℤ) (m * p))
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    (↑m : ℤ) ∣ w ∧
      (↑m : ℤ) ∣ x ∧
        (↑m : ℤ) ∣ y ∧
          (↑m : ℤ) ∣ z ∧
            HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
              HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
have this₁ : HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
    HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
  HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
Tactic: simp only [← _root_.euler_four_squares, Nat.cast_add, Nat.cast_pow] at this
Cleared hypotheses: this