-- 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:
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 / ↑n ^ x ≤ C

Tactic:
refine tsum_le_tsum (fun n ↦ ?_) ?_ key

Result:
case refine_1
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 / ↑n ^ x ≤ residueClass a n / ↑n

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

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
⊢ False

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)

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)
⊢ 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
⊢ False

Tactic:
have key : Summable fun n : ℕ ↦ residueClass a n / n := by
  convert (summable_residueClass_non_primes_div a).add H using 2 with n
  simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]

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
⊢ False

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
this : 0 < (C + C') * (2 - 1)
⊢ False

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

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'
⊢ False

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
⊢ ↑n ^ 1 ≤ ↑n ^ x

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

Result:
no goals

Proof state:
case intro.inr.intro.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)⁻¹
h₀ : 0 < C + C'
ξ : ℝ
hξ₁ : ξ ∈ Set.Ioc 1 2
hξ₂ : (C + C') * (ξ - 1) < (↑q.totient)⁻¹
⊢ False

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

Result:
no goals

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'
⊢ (↑q.totient)⁻¹ / (C + C') / 2 ⊓ (2 - 1) < (↑q.totient)⁻¹ / (C + C')

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

Result:
no goals

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

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Result:
case refine_1.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
x : ℝ
hx : 1 < x
⊢ residueClass a 0 / ↑0 ^ x ≤ residueClass a 0 / ↑0

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