-- Mathlib/Data/Nat/Totient.lean
theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
    #{x ∈ Ico k (k + n) | a.Coprime x} ≤ totient a * (n / a + 1)

Proof state:
case zero.a.h.h.bc
a k n : ℕ
a_pos : 0 < a
⊢ n % a ≤ a

Tactic:
exact le_of_lt (mod_lt n a_pos)

Result:
no goals

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

Tactic:
conv_lhs => rw [← Nat.mod_add_div n a]

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

Proof state:
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * (i + 1))))) ≤ φ a * (i + 1 + 1)

Tactic:
simp only [mul_succ]

Result:
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a

Proof state:
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a

Tactic:
calc
  #{x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}
    ≤ #{x ∈ Ico k (k + n % a + a * i) ∪
      Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x} := by
    gcongr
    apply Ico_subset_Ico_union_Ico
  _ ≤ #{x ∈ Ico k (k + n % a + a * i) | a.Coprime x} + a.totient := by
    rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
    apply card_union_le
  _ ≤ a.totient * i + a.totient + a.totient := add_le_add_right ih (totient a)

Result:
no goals

Proof state:
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i)) ∪
        filter (fun x => a.Coprime x) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) +
      #(filter (fun x => a.Coprime x) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))

Tactic:
apply card_union_le

Result:
no goals

Proof state:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * 0)))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + a))) * (0 + 1)

Tactic:
simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos), zero_add]

Result:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a))) ≤ #(filter (fun x => a.Coprime x) (Ico k (k + a)))

Proof state:
case a.h
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) ⊆ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)

Tactic:
apply Ico_subset_Ico_union_Ico

Result:
no goals

Proof state:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * 0)))) ≤ φ a * (0 + 1)

Tactic:
rw [← filter_coprime_Ico_eq_totient a k]

Result:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * 0)))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + a))) * (0 + 1)

Proof state:
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i + a))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)))

Tactic:
gcongr

Result:
case a.h
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) ⊆ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)

Proof state:
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a

Tactic:
simp_rw [← add_assoc] at ih ⊢

Result:
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a

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

Tactic:
induction' n / a with i ih

Result:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * 0)))) ≤ φ a * (0 + 1)

case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + (n % a + a * (i + 1))))) ≤ φ a * (i + 1 + 1)

Proof state:
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) + φ a

Tactic:
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]

Result:
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i)) ∪
        filter (fun x => a.Coprime x) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    #(filter (fun x => a.Coprime x) (Ico k (k + n % a + a * i))) +
      #(filter (fun x => a.Coprime x) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))

Proof state:
case zero
a k n : ℕ
a_pos : 0 < a
⊢ #(filter (fun x => a.Coprime x) (Ico k (k + n % a))) ≤ #(filter (fun x => a.Coprime x) (Ico k (k + a)))

Tactic:
gcongr

Result:
case zero.a.h.h.bc
a k n : ℕ
a_pos : 0 < a
⊢ n % a ≤ a