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

State before:
α : Type u_1
f : α → α
h : FinChainFn f
⊢ Surjective f ↔ h.rangeCompl = ∅
Tactic:
rw [← Set.range_iff_surjective, ← compl_inj_iff,
  ← h.rangeCompl_spec, Set.compl_univ, coe_eq_empty]
State after:
no goals