-- Mathlib/NumberTheory/PrimeCounting.lean
theorem primeCounting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
    π' (k + n) ≤ π' k + Nat.totient a * (n / a + 1) :=
  calc
    π' (k + n) ≤ #{p ∈ range k | p.Prime} + #{p ∈ Ico k (k + n) | p.Prime}

Proof state:
case left
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ k ≤ p ∧ p < k + n

Tactic:
exact ⟨succ_k_le_p, p_lt_n⟩

Result:
no goals

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ ∀ ⦃x : ℕ⦄, k ≤ x → x < k + n → Prime x → (k ≤ x ∧ x < k + n) ∧ a.Coprime x

Tactic:
intro p succ_k_le_p p_lt_n p_prime

Result:
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ (k ≤ p ∧ p < k + n) ∧ a.Coprime p

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ #(filter (fun b => a.Coprime b) (Ico k (k + n))) ≤ φ a * (n / a + 1)

Tactic:
exact Ico_filter_coprime_le k n h0

Result:
no goals

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' (k + n) ≤ #(filter (fun p => Prime p) (range k)) + #(filter (fun p => Prime p) (Ico k (k + n)))

Tactic:
rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, ←
  Ico_union_Ico_eq_Ico (zero_le k) le_self_add, filter_union]

Result:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ #(filter (fun x => Prime x) (Ico 0 k) ∪ filter (fun x => Prime x) (Ico k (k + n))) ≤
    #(filter (fun p => Prime p) (Ico 0 k)) + #(filter (fun p => Prime p) (Ico k (k + n)))

Proof state:
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ a.Coprime p

Tactic:
rw [coprime_comm]

Result:
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ p.Coprime a

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ #(filter (fun p => Prime p) (range k)) + #(filter (fun p => Prime p) (Ico k (k + n))) ≤
    π' k + #(filter (fun p => Prime p) (Ico k (k + n)))

Tactic:
rw [primeCounting', count_eq_card_filter_range]

Result:
no goals

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ #(filter (fun x => Prime x) (Ico 0 k) ∪ filter (fun x => Prime x) (Ico k (k + n))) ≤
    #(filter (fun p => Prime p) (Ico 0 k)) + #(filter (fun p => Prime p) (Ico k (k + n)))

Tactic:
apply card_union_le

Result:
no goals

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + #(filter (fun b => a.Coprime b) (Ico k (k + n))) ≤ π' k + φ a * (n / a + 1)

Tactic:
rw [add_le_add_iff_left]

Result:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ #(filter (fun b => a.Coprime b) (Ico k (k + n))) ≤ φ a * (n / a + 1)

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ filter (fun p => Prime p) (Ico k (k + n)) ⊆ filter (fun b => a.Coprime b) (Ico k (k + n))

Tactic:
simp only [subset_iff, and_imp, mem_filter, mem_Ico]

Result:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ ∀ ⦃x : ℕ⦄, k ≤ x → x < k + n → Prime x → (k ≤ x ∧ x < k + n) ∧ a.Coprime x

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ (k ≤ p ∧ p < k + n) ∧ a.Coprime p

Tactic:
constructor

Result:
case left
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ k ≤ p ∧ p < k + n

case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ a.Coprime p

Proof state:
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ p.Coprime a

Tactic:
exact coprime_of_lt_prime h0 (gt_of_ge_of_gt succ_k_le_p h1) p_prime

Result:
no goals

Proof state:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + #(filter (fun p => Prime p) (Ico k (k + n))) ≤ π' k + #(filter (fun b => a.Coprime b) (Ico k (k + n)))

Tactic:
refine add_le_add_left (card_le_card ?_) k.primeCounting'

Result:
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ filter (fun p => Prime p) (Ico k (k + n)) ⊆ filter (fun b => a.Coprime b) (Ico k (k + n))