awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
refine_1 : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
conv_lhs => rw [← Real.rpow_one n]

Premises used: Nat.cast, Real.rpow_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le

Premises used: LT.lt.le, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
summable_real_of_abscissaOfAbsConv_lt <|
        (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| mod_cast hx

Premises used: congrArg, LSeries.summable_real_of_abscissaOfAbsConv_lt, ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, cast, EReal.coe_lt_coe_iff._simp_1, LT.lt, congrFun', Eq.symm, LE.le.trans_lt, Nat.cast_one, Eq.trans, Real.toEReal
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
exact summable_real_of_abscissaOfAbsConv_lt <|
        (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| mod_cast hx

Premises used: LSeries.summable_real_of_abscissaOfAbsConv_lt, ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 ≤ 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
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
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
⊢ False

Tactic:
obtain ⟨C', hC'⟩ := LSeries_residueClass_lower_bound ha

Premises used: ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ ∀ {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)
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
⊢ LT.lt (α := ℝ) 0 (↑q.totient : ℝ)⁻¹

Tactic:
have hq : 0 < (q.totient : ℝ)⁻¹ := inv_pos.mpr (mod_cast q.totient.pos_of_neZero)
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
inr : ∀ (h₀ : 0 < C + C'), False
⊢ False

Tactic:
rcases le_or_gt (C + C') 0 with h₀ | h₀

Premises used: le_or_gt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ 0 < (C + C') * HSub.hSub (α := ℝ) 2 1

Tactic:
have := hq.trans_le (H₁ (Set.right_mem_Ioc.mpr one_lt_two))
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ HSub.hSub (α := ℝ) 2 1 = 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ 0 < C + C'

Tactic:
rw [show (2 : ℝ) - 1 = 1 by norm_num, mul_one] at this

Premises used: mul_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
⊢ False

Tactic:
(this.trans_le h₀).false

Premises used: LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
⊢ False

Tactic:
exact (this.trans_le h₀).false

Premises used: LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)⁻¹

Tactic:
⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩

Premises used: HDiv.hDiv, Nat.totient, Nat.cast, Inv.inv, HAdd.hAdd, And.intro, min_le_right, Exists.intro, OfNat.ofNat, Min.min
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
refine_2 : (C + C') * (min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2 - 1) < (↑q.totient : ℝ)⁻¹
⊢ ∃ (ξ : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ ∧ (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹

Tactic:
refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
⊢ 1 < min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2

Tactic:
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₀

Premises used: lt_add_iff_pos_right, and_true, lt_inf_iff, div_pos_iff_of_pos_right, Nat.ofNat_pos, Nat.one_lt_ofNat, div_pos
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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_2 : min ((↑q.totient : ℝ)⁻¹ / (C + C') / 2) (HSub.hSub (α := ℝ) 2 1) < (↑q.totient : ℝ)⁻¹ / (C + C')
⊢ (C + C') * (min (1 + (↑q.totient : ℝ)⁻¹ / (C + C') / 2) 2 - 1) < (↑q.totient : ℝ)⁻¹

Tactic:
rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]

Premises used: lt_div_iff₀', add_sub_cancel_left, min_sub_sub_right
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
⊢ min ((↑q.totient : ℝ)⁻¹ / (C + C') / 2) (HSub.hSub (α := ℝ) 2 1) < (↑q.totient : ℝ)⁻¹ / (C + C')

Tactic:
(min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two

Premises used: div_lt_self, min_le_left, one_lt_two, div_pos, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
⊢ min ((↑q.totient : ℝ)⁻¹ / (C + C') / 2) (HSub.hSub (α := ℝ) 2 1) < (↑q.totient : ℝ)⁻¹ / (C + C')

Tactic:
exact (min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two

Premises used: div_lt_self, min_le_left, one_lt_two, div_pos, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
inr :
  ∀ (ξ : ℝ) (hξ₁ : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ) (hξ₂ : (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹), False
⊢ 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

Premises used: Set.Ioc, Nat.totient, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
ξ : ℝ
hξ₁ : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ
hξ₂ : (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹
⊢ False

Tactic:
((H₁ hξ₁).trans_lt hξ₂).false

Premises used: LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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'
ξ : ℝ
hξ₁ : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) ξ
hξ₂ : (C + C') * (ξ - 1) < (↑q.totient : ℝ)⁻¹
⊢ False

Tactic:
exact ((H₁ hξ₁).trans_lt hξ₂).false

Premises used: LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
by_contra! : ∀ (H : Set.Finite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}), False
⊢ Set.Infinite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Set.Finite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}
⊢ False

Tactic:
not_summable_residueClass_prime_div ha <|
    summable_of_hasFiniteSupport <| show Set.Finite _ from support_residueClass_prime_div a ▸ H

Premises used: ArithmeticFunction.vonMangoldt.support_residueClass_prime_div, Eq.rec, ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div, summable_of_hasFiniteSupport, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Set.Finite (α := ℕ) {p : ℕ | Prime p ∧ (↑p : ZMod q) = a}
⊢ False

Tactic:
exact not_summable_residueClass_prime_div ha <|
    summable_of_hasFiniteSupport <| show Set.Finite _ from support_residueClass_prime_div a ▸ H

Premises used: ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div, summable_of_hasFiniteSupport
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
n : ℕ
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
⊢ ∃ 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

Premises used: Set.infinite_iff_exists_gt, Iff.mp, Nat.infinite_setOf_prime_and_eq_mod
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
n 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:
⟨p, hp₂.gt, Set.mem_setOf.mp hp₁⟩

Premises used: Set.mem_setOf, And.intro, Exists.intro, Iff.mp, LT.lt.gt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
n 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:
exact ⟨p, hp₂.gt, Set.mem_setOf.mp hp₁⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
⊢ NeZero q

Tactic:
have : NeZero q := ⟨hq⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this : NeZero q
rwa : IsCoprime (↑q : ℤ) a
rwa₁ rwa₂ rwa₃ rwa₄ : IsCoprime a (↑q : ℤ)
⊢ IsUnit (M := ZMod q) (↑a : ZMod q)

Tactic:
rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]

Premises used: isCoprime_comm, ZMod.coe_int_isUnit_iff_isCoprime