Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_card (IMOSLLean4/IMO2013/A5/FinChainFn.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card
Tactic:
have h0 := card_union_of_disjoint
  (h.iterRangeCompl_disjoint_exactIterRange n.le_refl)
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
h0 : (h.exactIterRange n ∪ h.iterRangeCompl n).card = (h.exactIterRange n).card + (h.iterRangeCompl n).card
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
h0 : (h.exactIterRange n ∪ h.iterRangeCompl n).card = (h.exactIterRange n).card + (h.iterRangeCompl n).card
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card
Tactic:
rw [h.iterRangeCompl_succ, h0, h.exactIterRange_card,
  iterRangeCompl_card n, Nat.succ_mul, add_comm]
State after:
no goals