case zero
p : ℕ
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 zero)) = zero / p

case succ
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 (succ n))) = succ n / p
n p : ℕ
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
induction' n with n IH
no goals
case succ
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
h1 : Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 (succ n))) = succ n / p
simp [Nat.succ_div, add_ite, add_zero, h1, filter_insert, apply_ite card, card_insert_eq_ite, IH,
  Finset.mem_filter, mem_Ioc, not_le.2 (lt_add_one n), Nat.succ_eq_add_one]
no goals
case zero
p : ℕ
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 zero)) = zero / p
simp
case inl
p : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p
⊢ Ioc 0 (succ 0) = insert (succ 0) (Ioc 0 0)

case inr
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
hn : n > 0
⊢ Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
rcases n.eq_zero_or_pos with (rfl | hn)
no goals
case inr
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
hn : n > 0
⊢ Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
simp_rw [← Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right]
no goals
case inl
p : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p
⊢ Ioc 0 (succ 0) = insert (succ 0) (Ioc 0 0)
simp