awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational (x / (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
m : ℤ
x : ℝ
rw : Irrational (x / (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x
have rw₂ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Tactic: rw [← cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
⊢ Irrational (x / (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw : Irrational (x / (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_div_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational (x / (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_div_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.Irrational (goal)
Goal:
n : ℕ
x : ℝ
rw : Irrational (x / (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x
have rw₂ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Tactic: rw [← cast_natCast, irrational_div_ratCast_iff, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∈ s.prodPrimes.divisors
⊢ Squarefree d
have hd₁ : d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0
Tactic: simp only [Nat.mem_divisors] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ Eq (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
have rw : Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) (∏ a ∈ d.primeFactors, a) : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
Tactic: rw [← s.nu_mult.map_prod_of_subset_primeFactors _ _ subset_rfl,
    Nat.prod_primeFactors_of_squarefree <| Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
rw : Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) (∏ a ∈ d.primeFactors, a) : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
⊢ Eq (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
have rw₁ : Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
Tactic: rw [← s.nu_mult.map_prod_of_subset_primeFactors _ _ subset_rfl,
    Nat.prod_primeFactors_of_squarefree <| Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) 0 (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p)
have h0 : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
Tactic: apply prod_pos
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)
have hp_prime : Nat.Prime p
Tactic: have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : Nat.Prime p
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)
have hp_dvd : p ∣ s.prodPrimes
Tactic: have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
have p : LT.lt (α := ℝ) 0 (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p)
Tactic: calc
    0 < ∏ p ∈ d.primeFactors, s.nu p := by
      apply prod_pos
      intro p hpd
      have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
      have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
      exact s.nu_pos_of_prime p hp_prime hp_dvd
    _ = s.nu d := prod_primeFactors_nu hd
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ Ne (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (0 : ℝ)
have h : LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
Tactic: apply _root_.ne_of_gt
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (1 : ℝ)
have hd_sq : Squarefree d
Tactic: have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (1 : ℝ)
have this : d ≠ 0
Tactic: have := hd_sq.ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
have hf : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
Tactic: apply prod_lt_prod_of_nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
hf : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
⊢ LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
have hfg : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ) (1 : ℝ)
Tactic: apply prod_lt_prod_of_nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
hf : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
hfg : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
have h_ne : d.primeFactors.Nonempty
Tactic: apply prod_lt_prod_of_nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hp : p ∈ d.primeFactors
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)
have hp₁ : Nat.Prime p ∧ p ∣ d ∧ d ≠ 0
Tactic: simp only [mem_primeFactors] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : p ∈ d.primeFactors
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ) (1 : ℝ)
have hpd₁ : Nat.Prime p ∧ p ∣ d
Tactic: rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
Cleared hypotheses: hpd
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (1 : ℝ)
have d₁ : LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
Tactic: calc
    s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
    _ < ∏ p ∈ d.primeFactors, 1 := by
      apply prod_lt_prod_of_nonempty
      · intro p hp
        simp only [mem_primeFactors] at hp
        apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
      · intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
      · simp only [nonempty_primeFactors, show 1 < d by lia]
    _ = 1 := by
      simp
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
d₁ : LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (1 : ℝ)
have d₂ : Eq (α := ℝ) (∏ p ∈ d.primeFactors, 1) 1
Tactic: calc
    s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
    _ < ∏ p ∈ d.primeFactors, 1 := by
      apply prod_lt_prod_of_nonempty
      · intro p hp
        simp only [mem_primeFactors] at hp
        apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
      · intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
      · simp only [nonempty_primeFactors, show 1 < d by lia]
    _ = 1 := by
      simp
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
⊢ Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
have simp_rw : Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
  (∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x * 1 else s.weights x * 0)
Tactic: simp_rw [mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
simp_rw :
  Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x * 1 else s.weights x * 0)
⊢ Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
have simp_rw₁ : Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
  (∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x else s.weights x * 0)
Tactic: simp_rw [mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (hypothesis)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ siftedSum (s := s) ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d
have hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
Tactic: have hμ : ∀ n, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d := h
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ siftedSum (s := s) ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d
have calc : siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
Tactic: calc siftedSum ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
    _ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes,
        if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
    _ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
calc : siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
⊢ siftedSum (s := s) ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d
have calc₁ : Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
  (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
Tactic: calc siftedSum ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
    _ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes,
        if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
    _ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
calc : siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
calc₁ :
  Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
⊢ siftedSum (s := s) ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d
have calc₂ : Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
  (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
Tactic: calc siftedSum ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
    _ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes,
        if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
    _ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
have rw : LE.le (α := ℝ) (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
  (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
Tactic: rw [siftedSum_eq_sum_support_mul_ite]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ LE.le (α := ℝ) (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
    (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
have h₁ : ∀ n ∈ s.support,
  LE.le (α := ℝ) (if s.prodPrimes.gcd n = 1 then 1 else 0) (∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
Tactic: gcongr with n
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
have simp_rw : Eq (α := ℝ) (∑ x ∈ s.support, ∑ i ∈ (s.prodPrimes.gcd x).divisors, s.weights x * muPlus i)
  (∑ x ∈ s.support, ∑ a ∈ s.prodPrimes.divisors with a ∣ x, s.weights x * muPlus a)
Tactic: simp_rw [mul_sum, ← sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ x ∈ s.support, ∑ i ∈ (s.prodPrimes.gcd x).divisors, s.weights x * muPlus i)
    (∑ x ∈ s.support, ∑ a ∈ s.prodPrimes.divisors with a ∣ x, s.weights x * muPlus a)
have e_f : ∀ (n : ℕ),
  Eq (α := ℝ) (∑ i ∈ (s.prodPrimes.gcd n).divisors, s.weights n * muPlus i)
    (∑ a ∈ s.prodPrimes.divisors with a ∣ n, s.weights n * muPlus a)
Tactic: congr with n
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
⊢ Eq (α := ℝ) (∑ i ∈ (s.prodPrimes.gcd n).divisors, s.weights n * muPlus i)
    (∑ a ∈ s.prodPrimes.divisors with a ∣ n, s.weights n * muPlus a)
have e_f : (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
⊢ (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}
have e_f : {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}
Tactic: rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
⊢ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}
have e_f : ∀ (x : ℕ), x ∈ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} ↔ x ∈ {a ∈ s.prodPrimes.divisors | a ∣ n}
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
have rw : Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
  (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
Tactic: rw [sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
have simp_rw : Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
  (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ n ∈ s.support, if x ∣ n then s.weights n else 0)
Tactic: simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
simp_rw :
  Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ n ∈ s.support, if x ∣ n then s.weights n else 0)
⊢ Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
have simp_rw₁ : Eq (α := ℝ) (∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x)
  (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ a ∈ s.support with x ∣ a, s.weights a)
Tactic: simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
simp_rw :
  Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ n ∈ s.support, if x ∣ n then s.weights n else 0)
simp_rw₁ :
  Eq (α := ℝ) (∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x)
    (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ a ∈ s.support with x ∣ a, s.weights a)
⊢ Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
have simp_rw₂ : Eq (α := ℝ) (∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x)
  (∑ x ∈ s.prodPrimes.divisors, ∑ i ∈ s.support with x ∣ i, muPlus x * s.weights i)
Tactic: simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
have case : Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
  (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
Tactic: case caseC =>
    rw [sum_comm]
    simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d =
    s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d
have rw : Eq (α := ℝ) (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
  (∑ x ∈ s.prodPrimes.divisors,
    (s.totalMass * HMul.hMul (β := ℝ) (muPlus x) ((s.nu : (a : ℕ) → ℝ) x : ℝ) + muPlus x * rem (s := s) x))
Tactic: rw [mainSum, mul_sum, ← sum_add_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ Eq (α := ℝ) (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
    (∑ x ∈ s.prodPrimes.divisors,
      (s.totalMass * HMul.hMul (β := ℝ) (muPlus x) ((s.nu : (a : ℕ) → ℝ) x : ℝ) + muPlus x * rem (s := s) x))
have e_f : ∀ (d : ℕ),
  muPlus d * multSum (s := s) d =
    s.totalMass * HMul.hMul (β := ℝ) (muPlus d) ((s.nu : (a : ℕ) → ℝ) d : ℝ) + muPlus d * rem (s := s) d
Tactic: congr with d
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d ≤
    s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, |muPlus d| * |rem (s := s) d|
have bc : ∀ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d ≤ |muPlus d| * |rem (s := s) d|
Tactic: gcongr _ + ∑ d ∈ _, ?_ with d
-- Lean 4 proof step from Mathlib.NumberTheory.SelbergSieve (goal)
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
h_1 : d ∈ s.prodPrimes.divisors
⊢ muPlus d * rem (s := s) d ≤ |muPlus d| * |rem (s := s) d|
have bc : muPlus d * rem (s := s) d ≤ |muPlus d * rem (s := s) d|
Tactic: rw [← abs_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : Membership.mem (γ := Finset (β → ℤ)) T v
⊢ Membership.mem (γ := Finset (α → ℤ)) S (A *ᵥ v)
have rw : ∀ (hv : 0 ≤ v ∧ v ≤ B'), N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
Tactic: rw [mem_Icc] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
have mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
Tactic: have mulVec_def : A.mulVec v =
      fun i ↦ Finset.sum univ fun j : β ↦ A i j * v j := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
have rw : (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
  LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P
Tactic: rw [mulVec_def]