Lean4
theorem mem_iff (a : α) (b : β a) : b ∈ Part.fix f a ↔ ∃ i, b ∈ approx f i a := by
classical
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
· simp only [Part.fix_def f h₀]
constructor <;> intro hh
· exact ⟨_, hh⟩
have h₁ := Nat.find_spec h₀
rw [dom_iff_mem] at h₁
obtain ⟨y, h₁⟩ := h₁
replace h₁ := approx_mono' f _ _ h₁
suffices y = b by
subst this
exact h₁
obtain ⟨i, hh⟩ := hh
revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
wlog case : i ≤ j
· rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
replace hh := approx_mono f case _ _ hh
apply Part.mem_unique h₁ hh
· simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
simp only [dom_iff_mem, not_exists] at h₀
intro; apply h₀
