a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * (n / a))))) ≤ φ a * (n / a + 1)
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n))) ≤ φ a * (n / a + 1)
conv_lhs => rw [← Nat.mod_add_div n a]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ φ a * (zero + 1)

case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * succ i)))) ≤ φ a * (succ i + 1)
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * (n / a))))) ≤ φ a * (n / a + 1)
induction' n / a with i ih
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * succ i)))) ≤ φ a * (succ i + 1)
simp only [mul_succ]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a
simp_rw [← add_assoc] at ih ⊢
no goals
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a
calc
  (filter a.coprime (Ico k (k + n % a + a * i + a))).card = (filter a.coprime
      (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card := by
    congr
    rw [Ico_union_Ico_eq_Ico]
    rw [add_assoc]
    exact le_self_add
    exact le_self_add
  _ ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + 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)
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ card (filter (coprime a) (Ico k (k + a))) * (zero + 1)
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ φ a * (zero + 1)
rw [← filter_coprime_Ico_eq_totient a k]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n % a))) ≤ card (filter (coprime a) (Ico k (k + a)))
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ card (filter (coprime a) (Ico k (k + a))) * (zero + 1)
simp only [add_zero, mul_one, MulZeroClass.mul_zero, le_of_lt (mod_lt n a_pos),
  Nat.zero_eq, zero_add]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ filter (coprime a) (Ico k (k + n % a)) ≤ filter (coprime a) (Ico k (k + a))
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n % a))) ≤ card (filter (coprime a) (Ico k (k + a)))
refine Finset.card_mono ?_
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ≤ Ico k (k + a)
case zero
a k n : ℕ
a_pos : 0 < a
⊢ filter (coprime a) (Ico k (k + n % a)) ≤ filter (coprime a) (Ico k (k + a))
refine' monotone_filter_left a.coprime _
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ⊆ Ico k (k + a)
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ≤ Ico k (k + a)
simp only [Finset.le_eq_subset]
no goals
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ⊆ Ico k (k + a)
exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k)
case e_s.e_s
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (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)
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) =
    card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)))
congr
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + n % a + a * i

case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
case e_s.e_s
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (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)
rw [Ico_union_Ico_eq_Ico]
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + (n % a + a * i)

case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + n % a + a * i

case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
rw [add_assoc]
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + (n % a + a * i)

case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
exact le_self_add
no goals
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
exact le_self_add
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card
      (filter (coprime a) (Ico k (k + n % a + a * i)) ∪
        filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) +
      card (filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) + φ a
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
no goals
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card
      (filter (coprime a) (Ico k (k + n % a + a * i)) ∪
        filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) +
      card (filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))
apply card_union_le