case zero
p : ℕ
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range zero)) = zero / p

case succ
p n : ℕ
hn : card (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range (succ n))) = succ n / p
n p : ℕ
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
induction' n with n hn
no goals
case succ
p n : ℕ
hn : card (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range (succ n))) = succ n / p
simp [Nat.succ_div, add_ite, add_zero, Finset.range_succ, filter_insert, apply_ite card,
  card_insert_of_not_mem, hn]
no goals
case zero
p : ℕ
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range zero)) = zero / p
simp