awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : Nonempty α
val : Unique α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
have inr : ∀ (this : BoundedOrder α), (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
Tactic: have := BoundedOrder.ofUnique α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
⊢ (type fun (x1 x2 : Ordinal.{u_2}) ↦ x1 < x2) ≤ (cof Ordinal.{u_2}).ord
have rw : ∀ (s : Set Ordinal.{u_2}), IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #(↑s : Type (u_2 + 1))
Tactic: rw [type_lt_ordinal, ← ord_univ, ord_le_ord, le_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : IsCofinal s
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ #(↑s : Type (u_2 + 1))
have contrapose! : ∀ (hs : #(↑s : Type (u_2 + 1)) < Cardinal.univ.{u_2, u_2 + 1}), ¬IsCofinal s
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (hypothesis)
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : #(↑s : Type (u_2 + 1)) < Cardinal.univ.{u_2, u_2 + 1}
⊢ ¬IsCofinal s
have hs₁ : Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))
Tactic: rw [← Cardinal.lift_id (#s), ← small_iff_lift_mk_lt_univ] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))
⊢ ¬IsCofinal s
have rw : BddAbove s
Tactic: rw [not_isCofinal_iff_bddAbove]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ (cof α).ord = type fun (x1 x2 : α) ↦ x1 < x2
have apply : (cof α).ord ≤ type fun (x1 x2 : α) ↦ x1 < x2
Tactic: apply IsRegularCardinalOrder.type_lt_le_ord_cof.antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ (cof α).ord ≤ type fun (x1 x2 : α) ↦ x1 < x2
have rw : cof α ≤ #α
Tactic: rw [ord_le, card_type]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ cof α = #α
have rw : cof α = (type (α := α) LT.lt).card
Tactic: rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : cof α = (type (α := α) LT.lt).card
⊢ cof α = #α
have rw₁ : cof α = (cof α).ord.card
Tactic: rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : cof α = (type (α := α) LT.lt).card
rw₁ : cof α = (cof α).ord.card
⊢ cof α = #α
have rw₂ : cof α = cof α
Tactic: rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
have rw : (#α).ord = (cof α).ord
Tactic: rw [← ord_cof_eq_type_lt, cof_eq_cardinalMk]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : (#α).ord = (cof α).ord
⊢ (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
have rw₁ : (#α).ord = (#α).ord
Tactic: rw [← ord_cof_eq_type_lt, cof_eq_cardinalMk]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = type fun (x1 x2 : α) ↦ x1 < x2
have apply : (type fun (x1 x2 : α) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2
Tactic: apply (RelEmbedding.ofMonotone Subtype.val (by simp)).ordinal_type_le.antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2
have rw : cof α ≤ #{ x : α // x ∈ s }
Tactic: rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
a o : α
s : Set α
hs : IsCofinal s
ho : o ∈ s
H : ∀ b < a, (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α) < o
⊢ (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) ≤ o
have rw : a ≤ ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)
Tactic: rw [← Subtype.coe_mk o ho, Subtype.coe_le_coe, ← OrderIso.le_symm_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
a o : α
s : Set α
hs : IsCofinal s
ho : o ∈ s
H : ∀ b < a, (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α) < o
⊢ a ≤ ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)
have H₁ : ∀ c < a, c < ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)
Tactic: apply le_of_forall_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
inst_3 : SuccOrder α
a o : α
s : Set α
hs : IsCofinal s
ha : o ∈ s
H : (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) < o
⊢ (↑((enum s hs : (a : α) → (↑s : Type u_1)) (succ a)) : α) ≤ o
have refine : ∀ (b : α) (hb : b < succ a),
  LE.le.{u_1} (α := α) (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α)
    (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α)
Tactic: refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
x : α
⊢ (enum Set.univ ⋯ : (a : α) → (↑Set.univ : Type u_1)) x =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) Set.univ x) x ⋯
have rw : (OrderIso.symm OrderIso.Set.univ : (a : α) → (↑Set.univ : Type u_1)) x =
  Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) Set.univ x) x sorry
Tactic: rw [← Subsingleton.allEq OrderIso.Set.univ.symm (enum univ .univ)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
| o.cof
have rw : Order.cof o.ToType
Tactic: rw [← type_toType o, cof_type]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ Order.cof o.ToType = o.cof
have conv_rhs : Order.cof o.ToType = o.cof
Tactic: conv_rhs => rw [← type_toType o, cof_type]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
conv_rhs : Order.cof o.ToType = o.cof
⊢ Order.cof o.ToType = o.cof
have conv_rhs₁ : Order.cof o.ToType = Order.cof o.ToType
Tactic: conv_rhs => rw [← type_toType o, cof_type]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof
have type : ∀ (α : Type u) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  Cardinal.lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2).cof = (lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2)).cof
Tactic: cases o using inductionOnWellOrder with | type α
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2).cof = (lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2)).cof
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type₂ : Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
type₂ : Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type₃ : Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
type₂ : Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)
type₃ : Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type₄ : Cardinal.lift.{max u v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
type₂ : Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)
type₃ : Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
type₄ : Cardinal.lift.{max u v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
have type₅ : Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α)) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
Tactic: rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ Order.cof (↑(Iio o) : Type (u + 1)) = (lift.{u + 1, u} o).cof
have rw : cof
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦
          x1 < x2) (typein fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o) =
  (lift.{u + 1, u} o).cof
Tactic: rw [Order.cof_Iio, typein_ordinal]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
rw :
  cof
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦
            x1 < x2) (typein fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o) =
    (lift.{u + 1, u} o).cof
⊢ Order.cof (↑(Iio o) : Type (u + 1)) = (lift.{u + 1, u} o).cof
have rw₁ : (lift.{u + 1, u} o).cof = (lift.{u + 1, u} o).cof
Tactic: rw [Order.cof_Iio, typein_ordinal]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ o.cof = 0 ↔ o = 0
have rw : Order.cof o.ToType = 0 ↔ o = 0
Tactic: rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : Order.cof o.ToType = 0 ↔ o = 0
⊢ o.cof = 0 ↔ o = 0
have rw₁ : IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
Tactic: rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : Order.cof o.ToType = 0 ↔ o = 0
rw₁ : IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
⊢ o.cof = 0 ↔ o = 0
have rw₂ : o = 0 ↔ o = 0
Tactic: rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₅ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ ¬IsSuccPrelimit o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
rw₅ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ ¬IsSuccPrelimit o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₆ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
rw₅ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ ¬IsSuccPrelimit o
rw₆ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₇ : o = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
rw₅ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ ¬IsSuccPrelimit o
rw₆ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
rw₇ : o = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
⊢ 1 < o.cof ↔ IsSuccLimit o
have rw₈ : o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o ↔
  o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
Tactic: rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o
have rw : 1 < o.cof ↔ IsSuccLimit o
Tactic: rw [aleph0_le_cof_iff, one_lt_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
rw : 1 < o.cof ↔ IsSuccLimit o
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o
have rw₁ : IsSuccLimit o ↔ IsSuccLimit o
Tactic: rw [aleph0_le_cof_iff, one_lt_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
⊢ o.cof = ℵ₀
have apply : ℵ₀ ≤ o.cof
Tactic: apply ((cof_le_card _).trans _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
apply : ℵ₀ ≤ o.cof
⊢ o.cof = ℵ₀
have apply₁ : o.card ≤ ℵ₀
Tactic: apply ((cof_le_card _).trans _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
⊢ ℵ₀ ≤ o.cof
have rwa : 1 < o.cof
Tactic: rwa [aleph0_le_cof_iff, one_lt_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
⊢ o.card ≤ ℵ₀
have rwa : o < (succ ℵ₀).ord
Tactic: rwa [card_le_iff, succ_aleph0, ord_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
rwa : o < (succ ℵ₀).ord
⊢ o.card ≤ ℵ₀
have rwa₁ : o < ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
Tactic: rwa [card_le_iff, succ_aleph0, ord_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
have obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u_1) = Order.cof α),
  ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
Tactic: obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u_1) = Order.cof α
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
have obtain : ∀ (r : (↑s : Type u_1) → (↑s : Type u_1) → Prop) (hr : IsWellOrder (↑s : Type u_1) r)
  (hr' : (#(↑s : Type u_1)).ord = type r),
  ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
Tactic: obtain ⟨r, hr, hr'⟩ := exists_ord_eq s
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u_1) = Order.cof α
r : (↑s : Type u_1) → (↑s : Type u_1) → Prop
hr : IsWellOrder (↑s : Type u_1) r
hr' : (#(↑s : Type u_1)).ord = type r
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
have ht : IsCofinal.{u_1} (α := α)
  (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a})
Tactic: have ht := hs.trans (isCofinal_setOf_imp_lt r)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u_1) = Order.cof α
r : (↑s : Type u_1) → (↑s : Type u_1) → Prop
hr : IsWellOrder (↑s : Type u_1) r
hr' : (#(↑s : Type u_1)).ord = type r
ht :
  IsCofinal.{u_1} (α := α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a})
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
have refine : (type
    fun
      (x1 x2 :
        (↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
              {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a}) :
          Type u_1)) ↦
    x1 < x2) ≤
  (Order.cof α).ord
Tactic: refine ⟨_, ht, (ord_le.2 (cof_le ht)).antisymm' ?_⟩