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

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ h.iterRangeCompl (n + 1) = image (fun k => f^[k] a) (range (n + 1))
Tactic:
rw [h.iterRangeCompl_succ, exactIterRange, h0, image_singleton,
iter_range_of_rangeCompl_singleton h0 n, range_succ, image_insert]
State after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ {f^[n] a} ∪ image (fun k => f^[k] a) (range n) = insert (f^[n] a) (image (fun k => f^[k] a) (range n))

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ {f^[n] a} ∪ image (fun k => f^[k] a) (range n) = insert (f^[n] a) (image (fun k => f^[k] a) (range n))
Tactic:
rfl
State after:
no goals