[GOAL]
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∃ h, Bijective h
[PROOFSTEP]
cases' isEmpty_or_nonempty β with hβ hβ
[GOAL]
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
⊢ ∃ h, Bijective h
[PROOFSTEP]
have : IsEmpty α := Function.isEmpty f
[GOAL]
case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : IsEmpty β
this : IsEmpty α
⊢ ∃ h, Bijective h
[PROOFSTEP]
exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective⟩
[GOAL]
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
hβ : Nonempty β
⊢ ∃ h, Bijective h
[PROOFSTEP]
set F : Set α →o Set α :=
  { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
    monotone' := fun s t hst =>
      compl_subset_compl.mpr <| image_subset _ <| compl_subset_compl.mpr <| image_subset _ hst }
    -- Porting note: dot notation `F.lfp` doesn't work here
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
⊢ ∃ h, Bijective h
[PROOFSTEP]
set s : Set α := OrderHom.lfp F
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
⊢ ∃ h, Bijective h
[PROOFSTEP]
have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ ∃ h, Bijective h
[PROOFSTEP]
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ (g '' (f '' s)ᶜ)ᶜ = sᶜᶜ
[PROOFSTEP]
simp [hs]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
⊢ ∃ h, Bijective h
[PROOFSTEP]
set g' := invFun g
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
⊢ ∃ h, Bijective h
[PROOFSTEP]
have g'g : LeftInverse g' g := leftInverse_invFun hg
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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
[PROOFSTEP]
have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
s : Set α := ↑OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ g' '' sᶜ = (f '' s)ᶜ
[PROOFSTEP]
rw [← hns, g'g.image_image]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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, Bijective h
[PROOFSTEP]
set h : α → β := s.piecewise f g'
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
⊢ ∃ h, Bijective h
[PROOFSTEP]
have : Surjective h := by rw [← range_iff_surjective, range_piecewise, hg'ns, union_compl_self]
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
⊢ Surjective h
[PROOFSTEP]
rw [← range_iff_surjective, range_piecewise, hg'ns, union_compl_self]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
⊢ ∃ h, Bijective h
[PROOFSTEP]
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⟩
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
⊢ Injective h
[PROOFSTEP]
refine' (injective_piecewise_iff _).2 ⟨hf.injOn _, _, _⟩
[GOAL]
case refine'_1
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
⊢ InjOn g' sᶜ
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case refine'_1
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x = y
[PROOFSTEP]
obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
case refine'_1.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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ g x' = y
[PROOFSTEP]
obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s 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'
[PROOFSTEP]
rw [g'g _, g'g _] at hxy 
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s 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'
[PROOFSTEP]
rw [hxy]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g' y
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : ¬y ∈ s
hxy : f x = g' y
⊢ False
[PROOFSTEP]
obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
[GOAL]
α : 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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : ¬y ∈ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ
[PROOFSTEP]
rwa [hns]
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s 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
[PROOFSTEP]
rw [g'g _] at hxy 
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this : Surjective h
x : α
hx : x ∈ s
y' : β
hy' : y' ∈ (f '' s)ᶜ
hy : ¬g y' ∈ s
hxy : f x = y'
⊢ False
[PROOFSTEP]
exact hy' ⟨x, hx, hxy⟩
[GOAL]
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 t : Set α), s ≤ t → (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ) }
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 : α → β := piecewise s f g'
this✝ : Surjective h
this : Injective h
⊢ ∃ h, Bijective h
[PROOFSTEP]
exact ⟨h, ‹Injective h›, ‹Surjective h›⟩
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
⊢ ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
[PROOFSTEP]
simpa only [ne_eq, not_exists, not_forall, not_and] using h
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hy with hy hy
[GOAL]
case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
cases' hy with hy hy
[GOAL]
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
subst x
[GOAL]
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
y : (i : ι) → β i
hy : y ∈ s
⊢ ∀ (i : ι), f i = y i → f = y
[PROOFSTEP]
exact fun i e => (hf i y hy e.symm).elim
[GOAL]
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
subst y
[GOAL]
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ s
⊢ ∀ (i : ι), x i = f i → x = f
[PROOFSTEP]
exact fun i e => (hf i x hx e).elim
[GOAL]
case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
[PROOFSTEP]
exact hs x hx y hy
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
⊢ a = b
[PROOFSTEP]
let ⟨sa, ea⟩ := hf a
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
⊢ a = b
[PROOFSTEP]
let ⟨sb, eb⟩ := hf b
[GOAL]
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
sb : f b ∈ s
eb : f b i = b
⊢ a = b
[PROOFSTEP]
rw [← ea, ← eb, hs _ sa _ sb _ e']
