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_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 :
  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) : ℤ)
⊢ ∃ (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 refine_1 : (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)
Tactic: refine ⟨_, _, _, _, ?_, ?_, ?_, ?_, 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_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 :
  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) : ℤ)
refine_1 : (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)
⊢ ∃ (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 refine_2 : (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)
Tactic: refine ⟨_, _, _, _, ?_, ?_, ?_, ?_, 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_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 :
  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) : ℤ)
refine_1 : (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)
refine_2 : (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)
⊢ ∃ (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 refine_3 : (↑m : ℤ) ∣ f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)
Tactic: refine ⟨_, _, _, _, ?_, ?_, ?_, ?_, 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_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 :
  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) : ℤ)
refine_1 : (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)
refine_2 : (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)
refine_3 : (↑m : ℤ) ∣ f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)
⊢ ∃ (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 refine_4 : (↑m : ℤ) ∣ f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)
Tactic: refine ⟨_, _, _, _, ?_, ?_, ?_, ?_, 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_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 :
  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) : ℤ)
⊢ (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)
have refine_2 : HPow.hPow (α := ZMod m) (β := ℕ) (↑a : ZMod m) 2 + HPow.hPow (α := ZMod m) (β := ℕ) (↑b : ZMod m) 2 +
      HPow.hPow (α := ZMod m) (β := ℕ) (↑c : ZMod m) 2 +
    HPow.hPow (α := ZMod m) (β := ℕ) (↑d : ZMod m) 2 =
  0
Tactic: suffices ((a : ZMod m) ^ 2 + (b : ZMod m) ^ 2 + (c : ZMod m) ^ 2 + (d : ZMod m) ^ 2) = 0 by
        simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, sq, add_comm, add_assoc,
          add_left_comm] using 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_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 :
  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) : ℤ)
⊢ HPow.hPow (α := ZMod m) (β := ℕ) (↑a : ZMod m) 2 + HPow.hPow (α := ZMod m) (β := ℕ) (↑b : ZMod m) 2 +
        HPow.hPow (α := ZMod m) (β := ℕ) (↑c : ZMod m) 2 +
      HPow.hPow (α := ZMod m) (β := ℕ) (↑d : ZMod m) 2 =
    0
have refine_2 : Eq (α := ZMod m)
  (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ZMod m) 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m n : ℕ
hm :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m
hn :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * n
have mul : ∀ (a b c d : ℕ),
  ∃ (a_1 : ℕ) (b_1 : ℕ) (c_1 : ℕ) (d_1 : ℕ),
    HPow.hPow (β := ℕ) a_1 2 + HPow.hPow (β := ℕ) b_1 2 + HPow.hPow (β := ℕ) c_1 2 + HPow.hPow (β := ℕ) d_1 2 =
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) * n
Tactic: rcases hm with ⟨a, b, c, d, rfl⟩
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
n : ℕ
hn :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
a b c d : ℕ
⊢ ∃ (a_1 : ℕ) (b_1 : ℕ) (c_1 : ℕ) (d_1 : ℕ),
    HPow.hPow (β := ℕ) a_1 2 + HPow.hPow (β := ℕ) b_1 2 + HPow.hPow (β := ℕ) c_1 2 + HPow.hPow (β := ℕ) d_1 2 =
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) * n
have mul : ∀ (w x y z : ℕ),
  ∃ (a_1 : ℕ) (b_1 : ℕ) (c_1 : ℕ) (d_1 : ℕ),
    HPow.hPow (β := ℕ) a_1 2 + HPow.hPow (β := ℕ) b_1 2 + HPow.hPow (β := ℕ) c_1 2 + HPow.hPow (β := ℕ) d_1 2 =
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
        (HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2)
Tactic: rcases hn with ⟨w, x, y, z, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
n : ℕ
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
have zero : ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0
Tactic: induction n using Nat.recOnMul with
  | zero => exact ⟨0, 0, 0, 0, rfl⟩
  | one => exact ⟨1, 0, 0, 0, rfl⟩
  | prime p hp => exact hp.sum_four_squares
  | mul m n hm hn =>
    rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
n : ℕ
zero :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
have one : ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1
Tactic: induction n using Nat.recOnMul with
  | zero => exact ⟨0, 0, 0, 0, rfl⟩
  | one => exact ⟨1, 0, 0, 0, rfl⟩
  | prime p hp => exact hp.sum_four_squares
  | mul m n hm hn =>
    rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
n : ℕ
zero :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0
one :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
have prime : ∀ (p : ℕ) (hp : Prime p),
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
Tactic: induction n using Nat.recOnMul with
  | zero => exact ⟨0, 0, 0, 0, rfl⟩
  | one => exact ⟨1, 0, 0, 0, rfl⟩
  | prime p hp => exact hp.sum_four_squares
  | mul m n hm hn =>
    rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
n : ℕ
zero :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0
one :
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1
prime :
  ∀ (p : ℕ) (hp : Prime p),
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n
have mul : ∀ (m n : ℕ)
  (hm :
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m)
  (hn :
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = n),
  ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * n
Tactic: induction n using Nat.recOnMul with
  | zero => exact ⟨0, 0, 0, 0, rfl⟩
  | one => exact ⟨1, 0, 0, 0, rfl⟩
  | prime p hp => exact hp.sum_four_squares
  | mul m n hm hn =>
    rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
N k : ℕ
⊢ (↑(N.roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑N : ℝ) (∑ p ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
have simp_rw : LE.le (α := ℝ) (↑(N.roughNumbersUpTo k).card : ℝ)
  (∑ x ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) (↑N : ℝ) (↑x : ℝ))
Tactic: simp_rw [Finset.mul_sum, mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
⊢ 1 / 2 ≤
    ∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
have hN₀ : let N₀ := 2 * HPow.hPow (β := ℕ) m 2;
N₀ = 2 * HPow.hPow (β := ℕ) m 2
Tactic: set N₀ : ℕ := 2 * m ^ 2 with hN₀
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this : 1 / 2 ≤ S
⊢ 1 / 2 ≤
    ∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
have h : HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1) = 2 * N₀
Tactic: convert! this using 5
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this : 1 / 2 ≤ S
⊢ HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1) = 2 * N₀
have h : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (k.primesBelow.card + 1)) 2 = 2 * N₀
Tactic: rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ 1 / 2 ≤
    ∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
have suffices : 1 / 2 ≤ S
Tactic: suffices 1 / 2 ≤ S by
    convert! this using 5
    rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
⊢ 1 / 2 ≤ S
have rwa : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
      HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this