awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
⊢ g' '' sᶜ = (f '' s)ᶜ

Tactic:
have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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'
rw : range h = univ
rw₁ : f '' s ∪ g' '' sᶜ = univ
rw₂ : f '' s ∪ (f '' s)ᶜ = univ
rw₃ rw₄ : Eq.{v + 1} (α := Set β) univ univ
⊢ Surjective h

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

Premises used: Set.range_eq_univ, Set.union_compl_self, Set.range_piecewise
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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'
⊢ Surjective h

Tactic:
have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
⊢ Injective h

Tactic:
(injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩

Premises used: Iff.mpr, Function.Injective.injOn, Set.injective_piecewise_iff, And.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
refine_1 : InjOn g' sᶜ
refine_2 : ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y
⊢ Injective h

Tactic:
refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩

Premises used: Iff.mpr, Function.Injective.injOn, Set.injective_piecewise_iff, And.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 : g' x = g' y
rwa rwa₁ rwa₂ rwa₃ : x ∈ sᶜ
⊢ x ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 : g' x = g' y
refine_1 : ∀ x' ∈ (f '' s)ᶜ, ∀ (hx : g x' ∈ sᶜ) (hxy : g' (g x') = g' y), g x' = y
⊢ x = y

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

Premises used: Set.image, rfl
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
y : α
hy : y ∈ sᶜ
x' : β
left : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
rwa rwa₁ rwa₂ rwa₃ : y ∈ sᶜ
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
y : α
hy : y ∈ sᶜ
x' : β
left : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
refine_1 : ∀ y' ∈ (f '' s)ᶜ, ∀ (hy : g y' ∈ sᶜ) (hxy : g' (g x') = g' (g y')), g x' = g y'
⊢ g x' = y

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

Premises used: Set.image, rfl
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 : g' (g x') = g' (g y')
⊢ x' = y'

Tactic:
rw [g'g _, g'g _] at hxy
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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'
refine_1 refine_1₁ : g y' = g y'
⊢ g x' = g y'

Tactic:
rw [hxy]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
rwa rwa₁ rwa₂ rwa₃ : y ∈ sᶜ
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
refine_2 : ∀ (y' : β) (hy' : y' ∈ (f '' s)ᶜ) (hy : g y' ∉ s) (hxy : f x = g' (g y')), False
⊢ False

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

Premises used: Set.image, rfl
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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')
⊢ f x = y'

Tactic:
rw [g'g _] at hxy
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 = y'
⊢ False

Tactic:
hy' ⟨x, hx, hxy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 = y'
⊢ False

Tactic:
exact hy' ⟨x, hx, hxy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
⊢ 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⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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)

Tactic:
⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
inr : ∀ (a : α), R a (h a)
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 : R a (if a ∈ s then f a else invFun g a)
⊢ R a (h a)

Tactic:
simp only [h, Set.piecewise, g']

Premises used: Set.piecewise
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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)
inr₁ : a ∉ s → R a (invFun g a)
⊢ R a (if a ∈ s then f a else invFun g a)

Tactic:
split
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 (f a)

Tactic:
hp₁ a
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 (f a)

Tactic:
exact hp₁ a
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
⊢ a ∈ g '' (f '' s)ᶜ

Tactic:
grind
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
⊢ a ∈ g '' (f '' s)ᶜ

Tactic:
have : a ∈ g '' (f '' s)ᶜ := by grind
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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)ᶜ
obtain : ∀ x ∈ (f '' s)ᶜ, ∀ (hx : g x = a), g (invFun g a) = a
⊢ g (invFun g a) = a

Tactic:
obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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)ᶜ
x : β
left : x ∈ (f '' s)ᶜ
hx : g x = a
⊢ g (invFun g a) = a

Tactic:
Function.invFun_eq ⟨x, hx⟩

Premises used: Exists.intro, Function.invFun_eq
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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)ᶜ
x : β
left : x ∈ (f '' s)ᶜ
hx : g x = a
⊢ g (invFun g a) = a

Tactic:
exact Function.invFun_eq ⟨x, hx⟩

Premises used: Exists.intro, Function.invFun_eq
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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
inr : ∀ (this : g (invFun g a) = a), R a (invFun g 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⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
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 : g (invFun g a) = a
⊢ R a (invFun g a)

Tactic:
grind
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∀ (a : α), (fun (x : α) (y : β) ↦ True) a (f a)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∀ (b : β), (fun (x : α) (y : β) ↦ True) (g b) b

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
obtain : ∀ (f : α → β) (hf : Bijective f), (∀ (a : α), True) → ∃ (h : α → β), Bijective h
⊢ ∃ (h : α → β), Bijective h

Tactic:
obtain ⟨f, hf, _⟩ := schroeder_bernstein_of_rel hf hg (fun x y ↦ True) (by simp) (by simp)

Premises used: True, Function.Embedding.schroeder_bernstein_of_rel
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f_1 : α → β
g : β → α
hf_1 : Injective f_1
hg : Injective g
f : α → β
hf : Bijective f
right : ∀ (a : α), True
⊢ ∃ (h : α → β), Bijective h

Tactic:
⟨f, hf⟩

Premises used: Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f_1 : α → β
g : β → α
hf_1 : Injective f_1
hg : Injective g
f : α → β
hf : Bijective f
right : ∀ (a : α), True
⊢ ∃ (h : α → β), Bijective h

Tactic:
exact ⟨f, hf⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
ι : Type u
β : ι → Type v
I : Nonempty ι
⊢ ∃ (s : Set ((i : ι) → β i)), Maximal (fun (x : Set ((i : ι) → β i)) ↦ x ∈ sets β) s

Tactic:
zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩

Premises used: _private.0.Function.Embedding.min_injective.match_5, Set.sUnion, zorn_subset, And.intro, Exists.intro, Set.subset_sUnion_of_mem, Eq