awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s : Set α // Bounded r s } = 0
have this : IsEmpty α
Tactic: haveI := mk_eq_zero_iff.1 ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ #{ s : Set α // Bounded r s } = 0
have inl : IsEmpty.{u_1 + 1} { s : Set α // Bounded r s }
Tactic: rw [mk_eq_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty.{u_1 + 1} { s : Set α // Bounded r s }
have inl : ∀ (a : { s : Set α // Bounded r s }), False
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s : Set α // Bounded r s } = #α
have h' : IsStrongLimit.{u_1} #α
Tactic: have h' : IsStrongLimit #α := ⟨ha, @h⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
⊢ #{ s : Set α // Bounded r s } = #α
have ha₁ : ℵ₀ ≤ #α
Tactic: have ha := h'.aleph0_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
⊢ #{ s : Set α // Bounded r s } = #α
have inr : #{ s : Set α // Bounded r s } ≤ #α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
inr : #{ s : Set α // Bounded r s } ≤ #α
⊢ #{ s : Set α // Bounded r s } = #α
have inr₁ : #α ≤ #{ s : Set α // Bounded r s }
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
⊢ #{ s : Set α // Bounded r s } ≤ #α
have this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
Tactic: have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := setOf_exists _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
⊢ #{ s : Set α // Bounded r s } ≤ #α
have inr : #(↑(⋃ (i : α), 𝒫 {j : α | r j i}) : Type u_1) ≤ #α
Tactic: rw [← coe_setOf, this]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
⊢ #(↑(⋃ (i : α), 𝒫 {j : α | r j i}) : Type u_1) ≤ #α
have inr : max (#α) (⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1)) ≤ #α
Tactic: refine mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
⊢ max (#α) (⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1)) ≤ #α
have inr : ⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
Tactic: rw [max_eq_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
⊢ ⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
have apply : ∀ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
Tactic: apply ciSup_le' _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
i : α
⊢ #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
have rw : HPow.hPow (α := Cardinal.{u_1}) 2 #(↑{j : α | r j i} : Type u_1) ≤ #α
Tactic: rw [mk_powerset]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s : Set α // Bounded r s }
have inr : ∀ (x : α), Bounded r {x}
Tactic: refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
inr : ∀ (x : α), Bounded r {x}
⊢ #α ≤ #{ s : Set α // Bounded r s }
have inr₁ : Injective (β := { s : Set α // Bounded r s }) fun (x : α) ↦ Subtype.mk (p := fun (s : Set α) ↦ Bounded r s) {x} sorry
Tactic: refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
x : α
⊢ Bounded r {x}
have inr : IsSuccLimit (type r)
Tactic: apply bounded_singleton
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (type r)
have inr : IsSuccLimit (#α).ord
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inl : ∀ (ha : #α = 0), #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
Tactic: rcases eq_or_ne #α 0 with (ha | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
inl : ∀ (ha : #α = 0), #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr : ∀ (ha : #α ≠ 0), #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
Tactic: rcases eq_or_ne #α 0 with (ha | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have h' : IsStrongLimit.{u_1} #α
Tactic: have h' : IsStrongLimit #α := ⟨ha, @h⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr : ∀ (r : α → α → Prop) (wo : IsWellOrder α r) (hr : (#α).ord = type r),
  #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
Tactic: rcases exists_ord_eq α with ⟨r, wo, hr⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr₁ : #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
| #α
have rw : #{ s : Set α // Bounded r s }
Tactic: rw [← mk_bounded_subset h hr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
have inr : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #{ s : Set α // Bounded r s }
Tactic: conv_rhs => rw [← mk_bounded_subset h hr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #{ s : Set α // Bounded r s }
have inr : ∀ ⦃x : Set α⦄, #(↑x : Type u_1) < (#α).ord.cof → Bounded r x
Tactic: apply mk_subtype_le_of_subset
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #(↑s : Type u_1) < (#α).ord.cof
⊢ Bounded r s
have hs₁ : #(↑s : Type u_1) < (type r).cof
Tactic: rw [hr] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #(↑s : Type u_1) < (type r).cof
⊢ Bounded r s
have inr : ∀ (hs : ¬Bounded r s), (type r).cof ≤ #(↑s : Type u_1)
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : ¬Bounded r s
⊢ (type r).cof ≤ #(↑s : Type u_1)
have hs₁ : Unbounded r s
Tactic: rw [not_bounded_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #(↑s : Type u_1)
have inr : IsCofinal s
Tactic: apply cof_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ IsCofinal s
have inr : ∀ (x : α), ∃ y ∈ s, ¬y < x
Tactic: simp_rw [IsCofinal, ← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
have inr : ∀ (x : α), #(↑{x} : Type u_1) < (#α).ord.cof
Tactic: refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : ∀ (x : α), #(↑{x} : Type u_1) < (#α).ord.cof
⊢ #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
have inr₁ : Injective (β := { s : Set α // #(↑s : Type u_1) < (#α).ord.cof }) fun (x : α) ↦
  Subtype.mk (p := fun (s : Set α) ↦ #(↑s : Type u_1) < (#α).ord.cof) {x} sorry
Tactic: refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ #(↑{x} : Type u_1) < (#α).ord.cof
have inr : IsSuccLimit (#α).ord
Tactic: rw [mk_singleton, one_lt_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
inr inr₁ inr₂ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr₃ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
Tactic: classical
  letI := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
inr inr₁ inr₂ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
inr₃ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
have inr₄ : #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
Tactic: classical
  letI := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c < c ^ c.ord.cof
have mk : ∀ (α : Type u_1) (hc : ℵ₀ ≤ #α), #α < #α ^ (#α).ord.cof
Tactic: induction c using Cardinal.inductionOn with | mk α
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof
have mk : ∀ (w : LinearOrder α) (w_1 : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2), #α < #α ^ (#α).ord.cof
Tactic: obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ NoMaxOrder α
have rw : IsSuccPrelimit (#α).ord
Tactic: rw [← isSuccPrelimit_type_lt_iff, ← hα]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ #α < #α ^ (#α).ord.cof
have this : NoMaxOrder α
Tactic: have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
⊢ #α < #α ^ (#α).ord.cof
have mk : ∀ (s : Set α) (hs : IsCofinal s) (hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord),
  #α < #α ^ (#α).ord.cof
Tactic: obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ #α < #α ^ (#α).ord.cof
have mk : #α < prod fun (x : (↑s : Type u_1)) ↦ #α
Tactic: rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ #α < prod fun (x : (↑s : Type u_1)) ↦ #α
have mk : #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
Tactic: refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
have mk : #(↑Set.univ : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
Tactic: rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
mk : #(↑Set.univ : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
⊢ #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
have mk₁ : #(↑(⋃ i ∈ s, Iio i) : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
Tactic: rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
mk : #(↑Set.univ : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
mk₁ : #(↑(⋃ i ∈ s, Iio i) : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
⊢ #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
have mk₂ : #(↑(⋃ i ∈ s, Iio i) : Type u_1) ≤ #(↑(⋃ i ∈ s, Iio i) : Type u_1)
Tactic: rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ a < (b ^ a).ord.cof
have apply : (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof
Tactic: apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a hb.ne_bot)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof
have rw : b ^ a < (b ^ a) ^ (b ^ a).ord.cof
Tactic: rw [← power_mul, mul_eq_self ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
⊢ lift.{v, u_1} 𝔠 = 𝔠
have rw : lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀) = 𝔠
Tactic: rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
rw : lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀) = 𝔠
⊢ lift.{v, u_1} 𝔠 = 𝔠
have rw₁ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 (lift.{v, u_1} ℵ₀) = 𝔠
Tactic: rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
rw : lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀) = 𝔠
rw₁ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 (lift.{v, u_1} ℵ₀) = 𝔠
⊢ lift.{v, u_1} 𝔠 = 𝔠
have rw₂ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 ℵ₀ = 𝔠
Tactic: rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
rw : lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀) = 𝔠
rw₁ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 (lift.{v, u_1} ℵ₀) = 𝔠
rw₂ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 ℵ₀ = 𝔠
⊢ lift.{v, u_1} 𝔠 = 𝔠
have rw₃ : 𝔠 = 𝔠
Tactic: rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
have rw : lift.{v, u} 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
Tactic: rw [← lift_continuum.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
rw : lift.{v, u} 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
have rw₁ : 𝔠 ≤ c ↔ 𝔠 ≤ c
Tactic: rw [← lift_continuum.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠
have rw : lift.{v, u} c ≤ lift.{v, u} 𝔠 ↔ c ≤ 𝔠
Tactic: rw [← lift_continuum.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
rw : lift.{v, u} c ≤ lift.{v, u} 𝔠 ↔ c ≤ 𝔠
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠
have rw₁ : c ≤ 𝔠 ↔ c ≤ 𝔠
Tactic: rw [← lift_continuum.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c
have rw : lift.{v, u} 𝔠 < lift.{v, u} c ↔ 𝔠 < c
Tactic: rw [← lift_continuum.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
rw : lift.{v, u} 𝔠 < lift.{v, u} c ↔ 𝔠 < c
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c
have rw₁ : 𝔠 < c ↔ 𝔠 < c
Tactic: rw [← lift_continuum.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠
have rw : lift.{v, u} c < lift.{v, u} 𝔠 ↔ c < 𝔠
Tactic: rw [← lift_continuum.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Continuum (goal)
Goal:
c : Cardinal.{u}
rw : lift.{v, u} c < lift.{v, u} 𝔠 ↔ c < 𝔠
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠
have rw₁ : c < 𝔠 ↔ c < 𝔠
Tactic: rw [← lift_continuum.{v, u}, lift_lt]