awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
have refine_1 : residueClass a 0 / HPow.hPow (α := ℝ) (↑0 : ℝ) x ≤ residueClass a 0 / (↑0 : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
refine_1 : residueClass a 0 / HPow.hPow (α := ℝ) (↑0 : ℝ) x ≤ residueClass a 0 / (↑0 : ℝ)
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
have refine_1₁ : ∀ (hn : n > 0), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
have refine_1 : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
| (↑n : ℝ)
have rw : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
Tactic: rw [← Real.rpow_one n]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x
have refine_1 : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: conv_lhs => rw [← Real.rpow_one n]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)
have norm_cast : 1 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
⊢ False
have H₁ : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
Tactic: have H₁ {x : ℝ} (hx : 1 < x) : ∑' n, residueClass a n / (n : ℝ) ^ x ≤ C := by
    refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key
    · rcases n.eq_zero_or_pos with rfl | hn
      · simp
      · refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
        conv_lhs => rw [← Real.rpow_one n]
        exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le
    · exact summable_real_of_abscissaOfAbsConv_lt <|
        (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| mod_cast hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁ : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
⊢ False
have obtain : ∀ (C' : ℝ)
  (hC' :
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x),
  False
Tactic: obtain ⟨C', hC'⟩ := LSeries_residueClass_lower_bound ha
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁ : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ False
have H₂ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
Tactic: have H₁ {x} (hx : x ∈ Set.Ioc 1 2) : (q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1) :=
    (div_le_iff₀ <| sub_pos.mpr hx.1).mp <|
      sub_le_iff_le_add.mp <| (hC' hx).trans (H₁ hx.1)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
⊢ False
have hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
Tactic: have hq : 0 < (q.totient : ℝ)⁻¹ := inv_pos.mpr (mod_cast q.totient.pos_of_neZero)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
⊢ False
have inl : ∀ (h₀ : C + C' ≤ 0), False
Tactic: rcases le_or_gt (C + C') 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
inl : ∀ (h₀ : C + C' ≤ 0), False
⊢ False
have inr : ∀ (h₀ : 0 < C + C'), False
Tactic: rcases le_or_gt (C + C') 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : C + C' ≤ 0
⊢ False
have this : 0 < (C + C') * HSub.hSub (α := ℝ) 2 1
Tactic: have := hq.trans_le (H₁ (Set.right_mem_Ioc.mpr one_lt_two))
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : C + C' ≤ 0
this : 0 < (C + C') * HSub.hSub (α := ℝ) 2 1
⊢ False
have this₁ : 0 < C + C'
Tactic: rw [show (2 : ℝ) - 1 = 1 by norm_num, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : 0 < C + C'
⊢ ∃ (ξ : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ ∧ (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹
have refine_1 : 1 < min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2
Tactic: refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : 0 < C + C'
refine_1 : 1 < min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2
⊢ ∃ (ξ : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ ∧ (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹
have refine_2 : (C + C') * (min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2 - 1) < (↑q.totient : ℝ)⁻¹
Tactic: refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : 0 < C + C'
⊢ (C + C') * (min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2 - 1) < (↑q.totient : ℝ)⁻¹
have refine_2 : min ((↑q.totient : ℝ)⁻¹ / (C + C') / 2) (HSub.hSub (α := ℝ) 2 1) < (↑q.totient : ℝ)⁻¹ / (C + C')
Tactic: rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
H₁_1 : ∀ {x : ℝ} (hx : 1 < x), ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
C' : ℝ
hC' :
  ∀ {x : ℝ},
    Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
      (↑q.totient : ℝ)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
H₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x), (↑q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1)
hq : LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹
h₀ : 0 < C + C'
⊢ False
have inr : ∀ (ξ : ℝ) (hξ₁ : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ) (hξ₂ : (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹), False
Tactic: obtain ⟨ξ, hξ₁, hξ₂⟩ : ∃ ξ ∈ Set.Ioc 1 2, (C + C') * (ξ - 1) < (q.totient : ℝ)⁻¹ := by
      refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
      · simpa only [lt_inf_iff, lt_add_iff_pos_right, Nat.ofNat_pos, div_pos_iff_of_pos_right,
          Nat.one_lt_ofNat, and_true] using div_pos hq h₀
      · rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]
        exact (min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
⊢ Set.Infinite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}
have by_contra! : ∀ (H : Set.Finite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
n : ℕ
⊢ ∃ p > n, Prime p ∧ (↑p : ZMod q) = a
have obtain : ∀ (p : ℕ) (hp₁ : Membership.mem (γ := Set ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a} p) (hp₂ : n < p),
  ∃ p > n, Prime p ∧ (↑p : ZMod q) = a
Tactic: obtain ⟨p, hp₁, hp₂⟩ := Set.infinite_iff_exists_gt.mp (infinite_setOf_prime_and_eq_mod ha) n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
have this : NeZero q
Tactic: have : NeZero q := ⟨hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this : NeZero q
⊢ IsUnit (M := ZMod q) (↑a : ZMod q)
have rwa : IsCoprime (↑q : ℤ) a
Tactic: rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this : NeZero q
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
have this₁ : IsUnit (M := ZMod q) (↑a : ZMod q)
Tactic: have : IsUnit (a : ZMod q) := by
    rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
have obtain : ∀ (p : ℕ) (hpn : p > n) (hpp : Prime p) (heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)),
  ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
Tactic: obtain ⟨p, hpn, hpp, heq⟩ := forall_exists_prime_gt_and_eq_mod this n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
p : ℕ
hpn : p > n
hpp : Prime p
heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
have refine : (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
Tactic: refine ⟨p, hpn, hpp, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]
have rw : ∀ (a_1 : ℕ), ∃ b ≥ a_1, Prime b ∧ b ≡ a [MOD q]
Tactic: rw [frequently_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n : ℕ
⊢ ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]
have obtain : ∀ (p : ℕ) (hn : p > n) (hp : Prime p) (ha : p ≡ a [MOD q]), ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]
Tactic: obtain ⟨p, hn, hp, ha⟩ := forall_exists_prime_gt_and_modEq n hq h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ completedCosZeta 0 s = completedRiemannZeta s
have rw : completedCosZeta 0 s = completedHurwitzZetaEven 0 s
Tactic: rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta 0 s = completedHurwitzZetaEven 0 s
⊢ completedCosZeta 0 s = completedRiemannZeta s
have rw₁ : completedCosZeta 0 s = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
Tactic: rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta 0 s = completedHurwitzZetaEven 0 s
rw₁ : completedCosZeta 0 s = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
⊢ completedCosZeta 0 s = completedRiemannZeta s
have rw₂ : (hurwitzEvenFEPair 0).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
Tactic: rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta 0 s = completedHurwitzZetaEven 0 s
rw₁ : completedCosZeta 0 s = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair 0).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
⊢ completedCosZeta 0 s = completedRiemannZeta s
have rw₃ : (hurwitzEvenFEPair 0).Λ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
Tactic: rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s
have rw : completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
Tactic: rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
    hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s
have rw₁ : completedCosZeta₀ 0 s = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
Tactic: rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
    hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
rw₁ : completedCosZeta₀ 0 s = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s
have rw₂ : (hurwitzEvenFEPair 0).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
Tactic: rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
    hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
rw₁ : completedCosZeta₀ 0 s = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair 0).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s
have rw₃ : (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
Tactic: rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
    hurwitzEvenFEPair_zero_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
have simp_rw : completedHurwitzZetaEven 0 s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
Tactic: simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
simp_rw : completedHurwitzZetaEven 0 s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
⊢ completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
have simp_rw₁ : completedHurwitzZetaEven 0 s = completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
Tactic: simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
simp_rw : completedHurwitzZetaEven 0 s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
simp_rw₁ : completedHurwitzZetaEven 0 s = completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
⊢ completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
have simp_rw₂ : completedHurwitzZetaEven₀ 0 s - (if True then 1 else 0) / s - 1 / (1 - s) =
  completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
Tactic: simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s
have rw : completedHurwitzZetaEven₀ 0 (1 - s) = completedRiemannZeta₀ s
Tactic: rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedHurwitzZetaEven₀ 0 (1 - s) = completedRiemannZeta₀ s
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s
have rw₁ : completedHurwitzZetaEven₀ 0 (1 - s) = completedCosZeta₀ 0 s
Tactic: rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedHurwitzZetaEven₀ 0 (1 - s) = completedRiemannZeta₀ s
rw₁ : completedHurwitzZetaEven₀ 0 (1 - s) = completedCosZeta₀ 0 s
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s
have rw₂ : completedCosZeta₀ 0 s = completedCosZeta₀ 0 s
Tactic: rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ completedRiemannZeta (1 - s) = completedRiemannZeta s
have rw : completedHurwitzZetaEven 0 (1 - s) = completedRiemannZeta s
Tactic: rw [← completedHurwitzZetaEven_zero, ← completedCosZeta_zero, completedHurwitzZetaEven_one_sub]