-- Mathlib/SetTheory/Cardinal/SchroederBernstein.lean
theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Function.Injective f)
    (hg : Function.Injective g) : ∃ h : α → β, Bijective h

Proof state:
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
⊢ ∃ h, Bijective h

Tactic:
have : IsEmpty α := Function.isEmpty f

Result:
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
this : IsEmpty α
⊢ ∃ h, Bijective h

Proof state:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ ∃ h, Bijective h

Tactic:
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])

Result:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
⊢ ∃ h, Bijective h

Proof state:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
⊢ ∃ h, Bijective h

Tactic:
have g'g : LeftInverse g' g := leftInverse_invFun hg

Result:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ ∃ h, Bijective h

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ (g '' (f '' s)ᶜ)ᶜ = sᶜᶜ

Tactic:
simp [hs]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : g' (g x') = g' (g y')
⊢ g x' = g y'

Tactic:
rw [g'g _, g'g _] at hxy

Result:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'

Tactic:
rw [hxy]

Result:
no goals

Proof state:
case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ False

Tactic:
obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]

Result:
case refine_2.intro.intro
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ s
y' : β
hy' : y' ∈ (f '' s)ᶜ
hy : g y' ∉ s
hxy : f x = g' (g y')
⊢ False

Proof state:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
⊢ ∃ h, Bijective h

Tactic:
exact ⟨h, ‹Injective h›, ‹Surjective h›⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
⊢ Surjective h

Tactic:
rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]

Result:
no goals

Proof state:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
⊢ ∃ h, Bijective h

Tactic:
set s : Set α := F.lfp

Result:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
⊢ ∃ h, Bijective h

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∃ h, Bijective h

Tactic:
rcases isEmpty_or_nonempty β with hβ | hβ

Result:
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
⊢ ∃ h, Bijective h

case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
⊢ ∃ h, Bijective h

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]

Result:
no goals