awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inl₃ : ∀ (this : ¬ℵ₀ ≤ c), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₆ inr₇ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₈ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
inr₉ inr₁₀ : ∀ (this : c.IsSingular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₁₁ : ∀ (this : c.IsSingular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have inl : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) ↔
  IsSuccLimit.{u_1 + 1} (α := Ordinal.{u_1}) 0 ∧ Ordinal.cof 0 < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0
Tactic: obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
inl :
  IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) ↔
    IsSuccLimit.{u_1 + 1} (α := Ordinal.{u_1}) 0 ∧ Ordinal.cof 0 < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have inr : ∀ (a : Ordinal.{u_1}),
  IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)) ↔
    IsSuccLimit (succ a) ∧ (succ a).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)
Tactic: obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
inl :
  IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) ↔
    IsSuccLimit.{u_1 + 1} (α := Ordinal.{u_1}) 0 ∧ Ordinal.cof 0 < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0
inr :
  ∀ (a : Ordinal.{u_1}),
    IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)) ↔
      IsSuccLimit (succ a) ∧ (succ a).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have inr₁ : ∀ (ho : IsSuccLimit o),
  IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have inr : ℵ₀ ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ∧
    (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔
  IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [isSingular_iff, ← (cof_ord_le _).lt_iff_ne]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω ≤ c
have obtain : ∀ (o : Ordinal.{u_1}) (hc : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)),
  LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
Tactic: obtain ⟨o, rfl⟩ := mem_range_aleph_iff.2 hc.aleph0_le
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
o : Ordinal.{u_1}
hc : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
⊢ LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
have hc₁ : IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [isSingular_aleph_iff] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
have rw : ω ≤ o
Tactic: rw [aleph_le_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preBeth c.ord = c
have apply : (preBeth ∘ ord) c ≤ c
Tactic: apply (preBeth_strictMono.comp ord_strictMono).le_apply.antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (preBeth ∘ ord) c ≤ c
have apply : ∀ a' < c.ord, preBeth a' ≤ c
Tactic: apply (isNormal_preBeth.le_iff_forall_le (isSuccLimit_ord hc.aleph0_lt.le)).2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ∀ a' < c.ord, preBeth a' ≤ c
have refine : ∀ (a : Ordinal.{u_1}) (ha : a < c.ord), preBeth a < c
Tactic: refine fun a ha ↦ le_of_lt ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
ha : a < c.ord
⊢ preBeth a < c
have ind : ∀ (a : Ordinal.{u_1}) (IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c) (ha : a < c.ord), preBeth a < c
Tactic: induction a using WellFoundedLT.induction with | ind a IH
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
⊢ preBeth a < c
have ind : ⨆ (a_1 : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a_1 : Ordinal.{u_1})) < c
Tactic: rw [preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
⊢ ⨆ (a_1 : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a_1 : Ordinal.{u_1})) < c
have apply : lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
Tactic: apply lift_iSup_lt_of_lt_cof_ord _ _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
apply : lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
⊢ ⨆ (a_1 : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a_1 : Ordinal.{u_1})) < c
have apply₁ : ∀ (i : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1})) < c
Tactic: apply lift_iSup_lt_of_lt_cof_ord _ _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
⊢ lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
have rwa : lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof
Tactic: rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
rwa : lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof
⊢ lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
have rwa₁ : lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof
Tactic: rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
rwa : lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof
rwa₁ : lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof
⊢ lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
have rwa₂ : lift.{u_1 + 1, u_1} a.card < lift.{u_1 + 1, u_1} c
Tactic: rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
rwa : lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof
rwa₁ : lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof
rwa₂ : lift.{u_1 + 1, u_1} a.card < lift.{u_1 + 1, u_1} c
⊢ lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
have rwa₃ : a.card < c
Tactic: rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℶ_ c.ord = c
have rw : HPow.hPow (β := ℕ) ω 2 < c.ord
Tactic: rw [← preBeth_of_omega0_sq_le (le_of_lt _), hc.preBeth_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ HPow.hPow (β := ℕ) ω 2 < c.ord
have rw : ℵ₀ < c
Tactic: rw [lt_ord, pow_two, card_mul, card_omega0, aleph0_mul_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord
have rw : ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
Tactic: rw [← ord_preAleph, hc.preAleph_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord
have rw₁ : c.ord = c.ord
Tactic: rw [← ord_preAleph, hc.preAleph_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord
have rw : ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
Tactic: rw [← ord_aleph, hc.aleph_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord
have rw₁ : c.ord = c.ord
Tactic: rw [← ord_aleph, hc.aleph_ord]
-- 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: rcases isEmpty_or_nonempty β with hβ | hβ
-- 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: rcases isEmpty_or_nonempty β with hβ | hβ
-- 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β : IsEmpty β
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have this : IsEmpty α
Tactic: have : IsEmpty α := Function.isEmpty f
-- 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
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have hs : (g '' (f '' s)ᶜ)ᶜ = s
Tactic: have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
-- 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
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have hns : g '' (f '' s)ᶜ = sᶜ
Tactic: have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
-- 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
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have g'g : LeftInverse g' g
Tactic: have g'g : LeftInverse g' g := leftInverse_invFun hg
-- 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
⊢ g' '' sᶜ = (f '' s)ᶜ
have rw : g' '' g '' (f '' s)ᶜ = (f '' s)ᶜ
Tactic: rw [← hns, g'g.image_image]
-- 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
rw : g' '' g '' (f '' s)ᶜ = (f '' s)ᶜ
⊢ g' '' sᶜ = (f '' s)ᶜ
have rw₁ : (f '' s)ᶜ = (f '' s)ᶜ
Tactic: rw [← hns, g'g.image_image]
-- 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
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have hg'ns : g' '' sᶜ = (f '' s)ᶜ
Tactic: have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
-- 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'
⊢ Surjective h
have rw : range h = univ
Tactic: rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- 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'
rw : range h = univ
⊢ Surjective h
have rw₁ : f '' s ∪ g' '' sᶜ = univ
Tactic: rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- 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'
rw : range h = univ
rw₁ : f '' s ∪ g' '' sᶜ = univ
⊢ Surjective h
have rw₂ : f '' s ∪ (f '' s)ᶜ = univ
Tactic: rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- 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'
rw : range h = univ
rw₁ : f '' s ∪ g' '' sᶜ = univ
rw₂ : f '' s ∪ (f '' s)ᶜ = univ
⊢ Surjective h
have rw₃ : Eq.{v + 1} (α := Set β) univ univ
Tactic: rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- 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'
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
have this : Surjective h
Tactic: have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
-- 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
⊢ Injective h
have refine_1 : InjOn g' sᶜ
Tactic: refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
-- 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
refine_1 : InjOn g' sᶜ
⊢ Injective h
have refine_2 : ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y
Tactic: refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
-- 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 : g' x = g' y
⊢ x = y
have refine_1 : ∀ x' ∈ (f '' s)ᶜ, ∀ (hx : g x' ∈ sᶜ) (hxy : g' (g x') = g' y), g x' = y
Tactic: obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
Cleared hypotheses: 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 : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ g x' = y
have refine_1 : ∀ y' ∈ (f '' s)ᶜ, ∀ (hy : g y' ∈ sᶜ) (hxy : g' (g x') = g' (g y')), g x' = g y'
Tactic: obtain ⟨y', _, 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' : β
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')
⊢ g x' = g y'
have hxy₁ : x' = y'
Tactic: rw [g'g _, g'g _] at hxy
Cleared hypotheses: hxy