Theorem: IMOSL.IMO2009C1.Iic_filter_dvd_card (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
k n : ℕ
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1
Tactic:
let h := (k + (n + 1)).card_multiples (n + 1)
State after:
k n : ℕ
h : (filter (fun e => n + 1 ∣ e + 1) (range (k + (n + 1)))).card = (k + (n + 1)) / (n + 1) :=
  Nat.card_multiples (k + (n + 1)) (n + 1)
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1

State before:
k n : ℕ
h : (filter (fun e => n + 1 ∣ e + 1) (range (k + (n + 1)))).card = (k + (n + 1)) / (n + 1) :=
  Nat.card_multiples (k + (n + 1)) (n + 1)
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1
Tactic:
rwa [range_eq_Ico, ← Ico_union_Ico_eq_Ico k.zero_le le_self_add, filter_union,
  card_union_of_disjoint (disjoint_filter_filter <| Ico_disjoint_Ico_consecutive 0 k _),
  ← range_eq_Ico, Nat.card_multiples, k.add_div_right n.succ_pos,
  Nat.succ_eq_add_one, add_right_inj] at h
State after:
no goals