-- 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
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'
⊢ ∃ ξ ∈ Set.Ioc 1 2, (C + C') * (ξ - 1) < (↑q.totient)⁻¹

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

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

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)⁻¹

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
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)
⊢ 2 - 1 = 1

Tactic:
norm_num

Result:
no goals

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

Tactic:
simp only [Nat.cast_zero, Real.zero_rpow (zero_lt_one.trans hx).ne', div_zero, le_refl]

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
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'
⊢ 1 < (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₀

Result:
no goals

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
⊢ Summable fun n => residueClass a n / ↑n

Tactic:
convert (summable_residueClass_non_primes_div a).add H using 2 with n

Result:
case h.e'_5.h
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
n : ℕ
⊢ residueClass a n / ↑n =
    (if Nat.Prime n then 0 else residueClass a n) / ↑n + (if Nat.Prime n then residueClass a n else 0) / ↑n

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

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

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 ^ 1 ≤ ↑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
this : 0 < C + C'
⊢ False

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

Result:
no goals

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
H₁ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
⊢ False

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

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

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
⊢ ¬Summable fun n => (if Nat.Prime n then residueClass a n else 0) / ↑n

Tactic:
intro H

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

Proof state:
case h.e'_5.h
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
n : ℕ
⊢ residueClass a n / ↑n =
    (if Nat.Prime n then 0 else residueClass a n) / ↑n + (if Nat.Prime n then residueClass a n else 0) / ↑n

Tactic:
simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]

Result:
no goals