awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
calc :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) =
    HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
have calc₁ : HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
Tactic: calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast
-- 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 : ℝ)
calc :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) =
    HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
calc₁ :
  HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
have calc₂ : HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
Tactic: calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ False
have obtain : ∀ (k : ℕ)
  (hk :
    ∀ t ⊆ {n : ℕ | k ≤ n},
      ∑' (n : (↑t : Type)), indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
        Iio (1 / 2)),
  False
Tactic: obtain ⟨k, hk⟩ := h.nat_tsum_vanishing (Iio_mem_nhds one_half_pos : Iio (1 / 2 : ℝ) ∈ 𝓝 0)
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∀ t ⊆ {n : ℕ | k ≤ n},
    ∑' (n : (↑t : Type)), indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
      Iio (1 / 2)
⊢ False
have hk₁ : ∑' (n : (↑({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) : Type)),
    indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
  Iio (1 / 2)
Tactic: specialize hk ({p | Nat.Prime p} ∩ {p | k ≤ p}) inter_subset_right
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (n : (↑({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) : Type)),
      indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
    Iio (1 / 2)
⊢ False
have hk₁ : ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x < 1 / 2
Tactic: rw [tsum_subtype, indicator_indicator, inter_eq_left.mpr fun n hn ↦ hn.1, mem_Iio] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
⊢ Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have h₁ : Eq (α := ℕ → ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
  (indicator {n : ℕ | k ≤ n} (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
Tactic: convert! h.indicator {n : ℕ | k ≤ n} using 1
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
⊢ False
have h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: have h' : Summable (indicator ({p | Nat.Prime p} ∩ {p | k ≤ p}) fun n ↦ (1 : ℝ) / n) := by
    convert! h.indicator {n : ℕ | k ≤ n} using 1
    simp only [indicator_indicator, inter_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ False
have refine : LE.le (α := ℝ)
  (∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
    HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
  (∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x)
Tactic: refine ((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ LE.le (α := ℝ)
    (∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
    (∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x)
have h₁ : ∀ (p : ℕ) (hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow),
  HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
Tactic: convert!
    Summable.sum_le_tsum (primesBelow ((4 ^ (k.primesBelow.card + 1)).succ) \ primesBelow k)
      (fun n _ ↦ indicator_nonneg (fun p _ ↦ by positivity) _) h' using
    2 with p hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
have hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
Tactic: obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
have hp₂ : p ∉ k.primesBelow
Tactic: obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (hypothesis)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
have hpp : Nat.Prime p
Tactic: have hpp := prime_of_mem_primesBelow hp₁
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
have h₁ : Membership.mem (γ := Set ℕ) ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) p
Tactic: refine (indicator_of_mem ?_ fun n : ℕ ↦ (1 / n : ℝ)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
have pos : ∀ (h : r < -1), (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
Tactic: by_cases h : r < -1
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
pos : ∀ (h : r < -1), (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
have neg : ∀ (h : ¬r < -1), (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
Tactic: by_cases h : r < -1
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
h : r < -1
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
have pos : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
Tactic: simp only [h, iff_true]
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
h : ¬r < -1
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
have neg : ¬Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
Tactic: simp only [h, iff_false]
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
h : ¬r < -1
⊢ ¬Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
have neg : ∀ (H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) (b : Primes),
  HDiv.hDiv (α := ℝ) 1 (↑(↑b : ℕ) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(↑b : ℕ) : ℝ) r
Tactic: refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
r : ℝ
h : ¬r < -1
H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
p : Primes
⊢ HDiv.hDiv (α := ℝ) 1 (↑(↑p : ℕ) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
have neg : HPow.hPow (α := ℝ) (β := ℝ) (↑(↑p : ℕ) : ℝ) (-1) ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
Tactic: rw [one_div, ← Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p
have apply : ¬Irreducible (M := GaussianInt) (↑p : GaussianInt)
Tactic: apply sq_add_sq_of_nat_prime_of_not_irreducible p
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible (M := GaussianInt) (↑p : GaussianInt)
have rwa : ¬_root_.Prime (M := GaussianInt) (↑p : GaussianInt)
Tactic: rwa [_root_.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
hp : p % 4 ≠ 3
rwa : ¬_root_.Prime (M := GaussianInt) (↑p : GaussianInt)
⊢ ¬Irreducible (M := GaussianInt) (↑p : GaussianInt)
have rwa₁ : ¬p % 4 = 3
Tactic: rwa [_root_.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
R : Type u_1
inst : CommRing R
a b x y u v : R
ha : a = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hb : b = HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2
⊢ a * b = HPow.hPow (β := ℕ) (x * u - y * v) 2 + HPow.hPow (β := ℕ) (x * v + y * u) 2
have rw : (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) * (HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2) =
  HPow.hPow (β := ℕ) (x * u - y * v) 2 + HPow.hPow (β := ℕ) (x * v + y * u) 2
Tactic: rw [ha, hb]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
a b x y u v : ℕ
ha : a = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hb : b = HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2
⊢ ∃ (r : ℕ) (s : ℕ), a * b = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
have zify : ∀ (ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2)
  (hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2),
  ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
Tactic: zify at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
⊢ ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
have obtain : ∀ (r s : ℤ) (h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2),
  ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
Tactic: obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
r s : ℤ
h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
⊢ ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
have refine : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
  HPow.hPow (α := ℤ) (β := ℕ) (↑r.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s.natAbs : ℤ) 2
Tactic: refine ⟨r.natAbs, s.natAbs, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
m n : ℕ
hd : m ∣ n
hs : IsSquare (α := ZMod n) (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (α := ZMod m) (-1)
have rw : IsSquare (α := ZMod m) ((f : (a : ZMod n) → ZMod m) (-1))
Tactic: rw [← map_one f, ← map_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1)
have rw : IsSquare (α := ZMod m × ZMod n) (-1, -1)
Tactic: rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)
have obtain : ∀ (x : ZMod m) (hx : -1 = x * x), IsSquare (α := ZMod m × ZMod n) (-1, -1)
Tactic: obtain ⟨x, hx⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
m n : ℕ
hc : m.Coprime n
hn : IsSquare (α := ZMod n) (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)
have obtain : ∀ (y : ZMod n) (hy : -1 = y * y), IsSquare (α := ZMod m × ZMod n) (-1, -1)
Tactic: obtain ⟨y, hy⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)
have rw : IsSquare (x * x, y * y)
Tactic: rw [hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
⊢ IsSquare (α := ZMod (m * n)) (-1)
have this : IsSquare (α := ZMod m × ZMod n) (-1)
Tactic: have : IsSquare (-1 : ZMod m × ZMod n) := by
    rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
    obtain ⟨x, hx⟩ := hm
    obtain ⟨y, hy⟩ := hn
    rw [hx, hy]
    exact ⟨(x, y), rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
⊢ p % 4 ≠ 3
have obtain : ∀ (y : ZMod p) (h : -1 = y * y), p % 4 ≠ 3
Tactic: obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd (Nat.dvd_of_mem_primeFactors hp) hs
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3
have h₁ : HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2
Tactic: rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2
⊢ p % 4 ≠ 3
have this : Fact (Prime p)
Tactic: have : Fact p.Prime := ⟨Nat.prime_of_mem_primeFactors hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3
have refine : ∀ (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
Tactic: refine ⟨fun H q hq ↦ Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one hq H,
    fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hpp : Nat.Prime p
ih : ∀ (hn : Squarefree n) (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
hn : Squarefree (p * n)
H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3
⊢ IsSquare (α := ZMod (p * n)) (-1)
have this : Fact (Nat.Prime p)
Tactic: have : Fact p.Prime := ⟨hpp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p n : ℕ
hpp : Nat.Prime p
ih : ∀ (hn : Squarefree n) (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
hn : Squarefree (p * n)
H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ p.Coprime n
have by_contra : ∀ (hc : ¬p.Coprime n), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hpp : Nat.Prime p
ih : ∀ (hn : Squarefree n) (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
hn : Squarefree (p * n)
H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ IsSquare (α := ZMod (p * n)) (-1)
have hcp : p.Coprime n
Tactic: have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hpp : Nat.Prime p
ih : ∀ (hn : Squarefree n) (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
hn : Squarefree (p * n)
H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : p.Coprime n
⊢ IsSquare (α := ZMod (p * n)) (-1)
have hp₁ : IsSquare (α := ZMod p) (-1)
Tactic: have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ IsSquare (α := ZMod n) (-1)
have zero : ∀ (hn : Squarefree (R := ℕ) 0) (H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3), IsSquare (α := ZMod 0) (-1)
Tactic: induction n using induction_on_primes with
  | zero => exact False.elim (hn.ne_zero rfl)
  | one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩
Cleared hypotheses: n, hn, H