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_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_2 :
  Eq (α := ZMod m)
    (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ZMod m) 0
⊢ 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:
norm_cast
-- 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₀ : 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) : ℤ)
⊢ Eq (α := ZMod m)
    (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ZMod m) 0

Tactic:
simp [habcd]
-- 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₀ : 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 * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, mul_comm
-- 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₀ : 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 * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, mul_comm
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0

Tactic:
⟨0, 0, 0, 0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 0

Tactic:
exact ⟨0, 0, 0, 0, rfl⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1

Tactic:
⟨1, 0, 0, 0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1

Tactic:
exact ⟨1, 0, 0, 0, rfl⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
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:
hp.sum_four_squares

Premises used: Nat.Prime.sum_four_squares
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
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:
exact hp.sum_four_squares

Premises used: Nat.Prime.sum_four_squares
-- Module: Mathlib.NumberTheory.SumFourSquares
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
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
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * n

Tactic:
rcases hm with ⟨a, b, c, d, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
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 : ℕ
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)
⊢ ∃ (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 hn with ⟨w, x, y, z, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d 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:
⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩

Premises used: Nat.euler_four_squares, Exists.intro
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d 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:
exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
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
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
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 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 _ _ _ _ _ _ _ _⟩

Premises used: Nat.zero, rfl
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
N k : ℕ
simp_rw :
  LE.le (α := ℝ) (↑(N.roughNumbersUpTo k).card : ℝ)
    (∑ x ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) (↑N : ℝ) (↑x : ℝ))
⊢ (↑(N.roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑N : ℝ) (∑ p ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
simp_rw [Finset.mul_sum, mul_one_div]

Premises used: Finset.mul_sum, mul_one_div
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
N k : ℕ
⊢ LE.le (α := ℝ) (↑(N.roughNumbersUpTo k).card : ℝ)
    (∑ x ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) (↑N : ℝ) (↑x : ℝ))

Tactic:
(Nat.cast_le.mpr <| roughNumbersUpTo_card_le N k).trans <|
    cast_sum (R := ℝ) .. ▸ Finset.sum_le_sum fun n _ ↦ cast_div_le

Premises used: Iff.mpr, Nat.roughNumbersUpTo_card_le, Eq.rec, Nat.cast_sum, Nat.cast_div_le, Finset.sum_le_sum, Nat.cast_le, LE.le.trans, Eq.symm
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
N k : ℕ
⊢ LE.le (α := ℝ) (↑(N.roughNumbersUpTo k).card : ℝ)
    (∑ x ∈ N.succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) (↑N : ℝ) (↑x : ℝ))

Tactic:
exact (Nat.cast_le.mpr <| roughNumbersUpTo_card_le N k).trans <|
    cast_sum (R := ℝ) .. ▸ Finset.sum_le_sum fun n _ ↦ cast_div_le

Premises used: Iff.mpr, Nat.roughNumbersUpTo_card_le, Nat.cast_le, LE.le.trans
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
⊢ let N₀ := 2 * HPow.hPow (β := ℕ) m 2;
  N₀ = 2 * HPow.hPow (β := ℕ) m 2

Tactic:
set N₀ : ℕ := 2 * m ^ 2 with hN₀
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 ≤ S

Tactic:
this
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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
h : HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1) = 2 * N₀
⊢ 1 / 2 ≤
    ∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)

Tactic:
convert! this using 5
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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
⊢ 4 = HPow.hPow (α := ℕ) (β := ℕ) 2 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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
h : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (k.primesBelow.card + 1)) 2 = 2 * N₀
⊢ HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1) = 2 * N₀

Tactic:
rw [show 4 = 2 ^ 2 by simp, pow_right_comm]

Premises used: pow_right_comm
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 (β := ℕ) (HPow.hPow (α := ℕ) 2 (k.primesBelow.card + 1)) 2 = 2 * N₀

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
suffices : 1 / 2 ≤ S
⊢ 1 / 2 ≤
    ∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)

Tactic:
suffices 1 / 2 ≤ S by
    convert! this using 5
    rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
    ring
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 :
  2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) - (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑m : ℝ) ≤
    2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * S
⊢ 2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) - (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑m : ℝ) =
    2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * (1 / 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : 2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * (1 / 2) ≤ 2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * S
⊢ 0 < 2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
suffices :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
⊢ 1 / 2 ≤ S

Tactic:
suffices 2 * N₀ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S by
    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
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) =
    HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)

Tactic:
exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm

Premises used: HMul.hMul, Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_card, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)

Tactic:
exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _

Premises used: HMul.hMul, Nat.add_le_add_right, Nat.smoothNumbersUpTo_card_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
grw :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) +
      HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
        (∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
⊢ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S

Tactic:
grw [roughNumbersUpTo_card_le']

Premises used: Nat.roughNumbersUpTo_card_le'
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
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 : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (↑(m * (2 * N₀).sqrt) : ℝ) +
      HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
        (∑ x ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) ≤
    (↑(m * (2 * N₀).sqrt) : ℝ) +
      HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
        (∑ x ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑x : ℝ))
⊢ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) +
      HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
        (∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S

Tactic:
norm_cast