awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumFourSquares
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 =
    r * m
hr₀ : 0 < r
⊢ 2 * (f a).natAbs < m

Tactic:
apply hf_lt
-- Module: Mathlib.NumberTheory.SumFourSquares
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 =
    r * m
hr₀ : 0 < r
⊢ 2 * (f b).natAbs < m

Tactic:
apply hf_lt
-- Module: Mathlib.NumberTheory.SumFourSquares
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 =
    r * m
hr₀ : 0 < r
⊢ 2 * (f c).natAbs < m

Tactic:
apply hf_lt
-- Module: Mathlib.NumberTheory.SumFourSquares
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 =
    r * m
hr₀ : 0 < r
⊢ 2 * (f d).natAbs < m

Tactic:
apply hf_lt
-- Module: Mathlib.NumberTheory.SumFourSquares
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
⊢ r < m

Tactic:
have hrm : r < m := by
      rw [mul_comm] at hr
      apply lt_of_sum_four_squares_eq_mul hr <;> apply hf_lt
-- Module: Mathlib.NumberTheory.SumFourSquares
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
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) : ℤ)
⊢ 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)

Premises used: HMul.hMul
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)

Tactic:
mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_

Premises used: Iff.mpr, pow_ne_zero, mul_left_cancel₀, LT.lt.ne', OfNat.ofNat, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)
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) : ℤ)
⊢ HPow.hPow (β := ℕ) (w / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)) 2 + HPow.hPow (β := ℕ) (y / (↑m : ℤ)) 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)) 2 =
    (↑(r * p) : ℤ)

Tactic:
refine mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_

Premises used: pow_ne_zero, mul_left_cancel₀, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)
rw : HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2
| HPow.hPow (α := ℤ) (β := ℕ) (↑m : ℤ) 2 * (↑(r * p) : ℤ)

Tactic:
rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]

Premises used: mul_mul_mul_comm, sq, Nat.cast_mul, Nat.cast_pow
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)
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
⊢ 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:
conv_rhs => rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]

Premises used: mul_mul_mul_comm, sq, Nat.cast_mul, Nat.cast_pow
-- Module: Mathlib.NumberTheory.SumFourSquares
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 (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2

Tactic:
simp only [mul_add, ← mul_pow, Int.mul_ediv_cancel', *]

Premises used: Int.mul_ediv_cancel', mul_add, mul_pow
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)

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', *]
-- Module: Mathlib.NumberTheory.SumFourSquares
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) : ℤ)
⊢ 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