awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this : Surjective h
x' : β
left : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left_1 : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'
have refine_1 : g y' = g y'
Tactic: rw [hxy]
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ
have rwa : y ∈ sᶜ
Tactic: rwa [hns]
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ False
have refine_2 : ∀ (y' : β) (hy' : y' ∈ (f '' s)ᶜ) (hy : g y' ∉ s) (hxy : f x = g' (g y')), False
Tactic: obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (hypothesis)
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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) 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
have hxy₁ : f x = y'
Tactic: rw [g'g _] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (hypothesis)
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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this : Surjective h
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have this₁ : Injective h
Tactic: 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⟩
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have inr : ∀ (a : α), R a (h a)
Tactic: refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
a : α
⊢ R a (h a)
have inr : R a (if a ∈ s then f a else invFun g a)
Tactic: simp only [h, Set.piecewise, g']
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
a : α
⊢ R a (if a ∈ s then f a else invFun g a)
have inr : a ∈ s → R a (f a)
Tactic: split
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
a : α
inr : a ∈ s → R a (f a)
⊢ R a (if a ∈ s then f a else invFun g a)
have inr₁ : a ∉ s → R a (invFun g a)
Tactic: split
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (hypothesis)
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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
a : α
h_1 : a ∉ s
⊢ g (invFun g a) = a
have this₁ : a ∈ g '' (f '' s)ᶜ
Tactic: have : a ∈ g '' (f '' s)ᶜ := by grind
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this_2 : Injective h
a : α
h_1 : a ∉ s
this : a ∈ g '' (f '' s)ᶜ
⊢ g (invFun g a) = a
have obtain : ∀ x ∈ (f '' s)ᶜ, ∀ (hx : g x = a), g (invFun g a) = a
Tactic: obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
-- 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
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) 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 (β := fun (a : α) ↦ β) f g'
this_1 : Surjective h
this : Injective h
a : α
h_1 : a ∉ s
⊢ R a (invFun g a)
have inr : ∀ (this : g (invFun g a) = a), R a (invFun g a)
Tactic: 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⟩
-- 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
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have inl : ∀ (hβ : IsEmpty β), ∃ (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
-- 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)
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have inr : ∀ (hβ : Nonempty β), ∃ (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
-- 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)
⊢ ∃ (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), ∃ (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
-- 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)
⊢ ∃ (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ᶜ), ∃ (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
-- 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)
⊢ ∃ (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), ∃ (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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∃ (h : α → β), Bijective h
have obtain : ∀ (f : α → β) (hf : Bijective f), (∀ (a : α), True) → ∃ (h : α → β), Bijective h
Tactic: obtain ⟨f, hf, _⟩ := schroeder_bernstein_of_rel hf hg (fun x y ↦ True) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
⊢ ∃ (s : Set ((i : ι) → β i)), Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
have refine : ∀ (c : Set (Set ((i : ι) → β i))) (hc : c ⊆ sets β) (hcc : IsChain (fun (x1 x2 : Set ((i : ι) → β i)) ↦ x1 ⊆ x2) c)
  (i : ι),
  ∀ x ∈ ⋃₀ c,
    ∀ y ∈ ⋃₀ c,
      ∀ (hi : Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y))
        (p : Set ((i : ι) → β i)) (hpc : p ∈ c) (hxp : x ∈ p) (q : Set ((i : ι) → β i)) (hqc : q ∈ c) (hyq : y ∈ q),
        x = y
Tactic: refine zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inl : ∀ (hx : x = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.SchroederBernstein (goal)
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s
h_1 : ¬∃ (i : ι), Surjective (β := β i) fun (x : (↑s : Type (max u v))) ↦ (↑x : (i : ι) → β i) i
h : ∀ (i : ι), ∃ (y : β i), ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
inl :
  ∀ (hx : x = f), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
⊢ Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
have inr : ∀ (hx : x ∈ s), Eq.{v + 1} (α := β i) ((fun (x : (i : ι) → β i) ↦ x i) x) ((fun (x : (i : ι) → β i) ↦ x i) y) → x = y
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx