-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
inl : ∀ (hβ : IsEmpty β), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
inr inr₁ inr₂ inr₃ : ∀ (hβ : Nonempty β), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
inr₄ :
  ∀ (hβ : Nonempty β),
    let F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ };
    let s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F;
    ∀ (hs : (g '' (f '' s)ᶜ)ᶜ = s), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
inr₅ inr₆ :
  ∀ (hβ : Nonempty β),
    let F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ };
    let s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F;
    ∀ (hs : (g '' (f '' s)ᶜ)ᶜ = s) (hns : g '' (f '' s)ᶜ = sᶜ), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
inr₇ :
  ∀ (hβ : Nonempty β),
    let F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ };
    let s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F;
    ∀ (hs : (g '' (f '' s)ᶜ)ᶜ = s) (hns : g '' (f '' s)ᶜ = sᶜ),
      let g' := invFun g;
      ∀ (g'g : LeftInverse g' g), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have inr₈ : ∀ (hβ : Nonempty β),
  let F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := sorry };
  let s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F;
  ∀ (hs : (g '' (f '' s)ᶜ)ᶜ = s) (hns : g '' (f '' s)ᶜ = sᶜ),
    let g' := invFun g;
    ∀ (g'g : LeftInverse g' g) (hg'ns : g' '' sᶜ = (f '' s)ᶜ), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
Tactic: classical
  rcases isEmpty_or_nonempty β with hβ | hβ
  · have : IsEmpty α := Function.isEmpty f
    exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩
  set F : Set α →o Set α :=
    { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
      monotone' := fun s t hst => by dsimp at hst ⊢; gcongr }
  set s : Set α := F.lfp
  have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
  have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
  set g' := invFun g
  have g'g : LeftInverse g' g := leftInverse_invFun hg
  have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
  set h : α → β := s.piecewise f g'
  have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
  have : Injective h := by
    refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
    · intro x hx y hy hxy
      obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
      obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _, g'g _] at hxy
      rw [hxy]
    · intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩
  refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
  simp only [h, Set.piecewise, g']
  split
  · exact hp₁ a
  · have : g (invFun g a) = a := by
      have : a ∈ g '' (f '' s)ᶜ := by grind
      obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
      exact Function.invFun_eq ⟨x, hx⟩
    grind