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

State before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
a : α
⊢ a ∈ ↑(h.exactIterRange n) ↔ a ∈ Set.range f^[n] \ Set.range f^[n + 1]
Tactic:
rw [exactIterRange, coe_image, h.rangeCompl_spec, iterate_succ,
  Set.range_comp _ f, Set.range_diff_image (h.injective.iterate n)]
State after:
no goals