-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The function `n ↦ Λ n / n` restricted to primes in an invertible residue class
is not summable. This then implies that there must be infinitely many such primes. -/
lemma not_summable_residueClass_prime_div (ha : IsUnit a) :
    ¬ Summable fun n : ℕ ↦ (if n.Prime then residueClass a n else 0) / n

Proof state:
case intro
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
⊢ False

Tactic:
have hq : 0 < (q.totient : ℝ)⁻¹ := inv_pos.mpr (mod_cast q.totient.pos_of_neZero)

Result:
case intro
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
⊢ False

Proof state:
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
⊢ False

Tactic:
let C := ∑' n, residueClass a n / n

Result:
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

Proof state:
case refine_2
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ (C + C') * ((1 + (↑q.totient)⁻¹ / (C + C') / 2) ⊓ 2 - 1) < (↑q.totient)⁻¹

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

Result:
case refine_2
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ (↑q.totient)⁻¹ / (C + C') / 2 ⊓ (2 - 1) < (↑q.totient)⁻¹ / (C + C')

Proof state:
case refine_1.inr
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 / ↑n ^ x ≤ residueClass a n / ↑n

Tactic:
refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_

Result:
case refine_1.inr
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 ≤ ↑n ^ x

Proof state:
case intro.inl
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
⊢ False

Tactic:
have := hq.trans_le (H₁ (Set.right_mem_Ioc.mpr one_lt_two))

Result:
case intro.inl
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
this : 0 < (C + C') * (2 - 1)
⊢ False

Proof state:
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
⊢ 1 ≤ ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
⊢ False

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

Result:
case intro.inl
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
⊢ False

case intro.inr
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 : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ False

Proof state:
case refine_2
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 / ↑n ^ x

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

Result:
no goals