awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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})
⊢ (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
have rw : Nonempty.{u_1 + 1}
  ((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) ↪r
    r)
Tactic: rw [← hs', hr', type_le_iff']
-- 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})
⊢ Nonempty.{u_1 + 1}
    ((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) ↪r
      r)
have refine_1 : ∀
  (x :
    (↑(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)),
  (↑x : α) ∈ s
Tactic: refine ⟨.ofMonotone (fun x ↦ ⟨x.1, ?_⟩) fun x y hxy ↦ ?_⟩
-- 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})
refine_1 :
  ∀
    (x :
      (↑(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)),
    (↑x : α) ∈ s
⊢ Nonempty.{u_1 + 1}
    ((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) ↪r
      r)
have refine_2 : ∀
  (x y :
    (↑(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))
  (hxy : x < y),
  r
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
      x)
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
      y)
Tactic: refine ⟨.ofMonotone (fun x ↦ ⟨x.1, ?_⟩) fun x y hxy ↦ ?_⟩
-- 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})
x y :
  (↑(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)
hxy : x < y
⊢ r
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
      x)
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
      y)
have refine_2 : ¬(Eq.{u_1 + 1} (α := (↑s : Type u_1))
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        x)
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        y) ∨
    r
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        y)
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        x))
Tactic: apply (trichotomous_of r _ _).resolve_right
-- 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})
x y :
  (↑(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)
hxy : x < y
hxy' :
  r
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
      y)
    ((fun
          (x :
            (↑(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)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
      x)
⊢ False
have refine_2 : ∀ (z : { x : α // x ∈ s })
  (hz : Membership.mem (γ := Set { x : α // x ∈ s }) {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a} z)
  (hxy :
    Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := Set α)
          (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})
          x)
        (↑z : α) sorry <
      y)
  (hxy' :
    r
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        y)
      ((fun
            (x :
              (↑(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)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := Set α)
            (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})
            x)
          (↑z : α) sorry))),
  False
Tactic: obtain ⟨x, z, hz, rfl⟩ := x
Cleared hypotheses: x, hxy, hxy'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ (Order.cof α).ord.cof = Order.cof α
have obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord),
  (Order.cof α).ord.cof = Order.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
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ (Order.cof α).ord.cof = Order.cof α
have rw : Order.cof (↑s : Type u_1) = Order.cof α
Tactic: rw [← hs', cof_type]
-- 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' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ Order.cof (↑s : Type u_1) = Order.cof α
have a : Order.cof (↑s : Type u_1) ≤ Order.cof α
Tactic: apply le_antisymm
-- 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' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
a : Order.cof (↑s : Type u_1) ≤ Order.cof α
⊢ Order.cof (↑s : Type u_1) = Order.cof α
have a₁ : Order.cof α ≤ Order.cof (↑s : Type u_1)
Tactic: apply le_antisymm
-- 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' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ Order.cof (↑s : Type u_1) ≤ Order.cof α
have a : Order.cof (↑s : Type u_1) ≤ #(↑s : Type u_1)
Tactic: rw [← card_ord (Order.cof α), ← hs', card_type]
-- 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' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ Order.cof α ≤ Order.cof (↑s : Type u_1)
have a : ∀ (s_1 : Set (↑s : Type u_1)), IsCofinal s_1 → Order.cof α ≤ #(↑s_1 : Type u_1)
Tactic: rw [le_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
have refine_2 : ∀
  (this :
    StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i)
        sorry),
  Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
Tactic: have : StrictMono (β := Iio (⨆ i, f i + 1)) (fun i ↦ ⟨f i, ?_⟩) := fun x y h ↦ hf h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
refine_2 :
  ∀
    (this :
      StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
        Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x)
          (f i) ⋯),
    Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
have refine_1 : ∀ (i : β), Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) (f i)
Tactic: have : StrictMono (β := Iio (⨆ i, f i + 1)) (fun i ↦ ⟨f i, ?_⟩) := fun x y h ↦ hf h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this :
  StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i) ⋯
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
have refine_2 : ∀
  (this :
    Cardinal.lift.{u + 1, v} (Order.cof β) =
      Cardinal.lift.{v, u + 1} (Order.cof (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))),
  Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
Tactic: have := lift_cof_congr_of_strictMono this ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this :
  StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i) ⋯
refine_2 :
  ∀
    (this :
      Cardinal.lift.{u + 1, v} (Order.cof β) =
        Cardinal.lift.{v, u + 1} (Order.cof (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))),
    Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
have refine_2₁ : IsCofinal.{u + 1} (α := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
  (range fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i)
      sorry)
Tactic: have := lift_cof_congr_of_strictMono this ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this_1 :
  StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i) ⋯
this :
  Cardinal.lift.{u + 1, v} (Order.cof β) =
    Cardinal.lift.{v, u + 1} (Order.cof (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
have refine_2 : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1))) =
  Cardinal.lift.{v, u + 1} (Order.cof (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
Tactic: rw [← Cardinal.lift_inj.{_, max (u + 1) v}, Cardinal.lift_lift.{_, _, v},
        Cardinal.lift_umax.{_, u + 1}, Cardinal.lift_umax.{_, u + 1}, this]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this :
  StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i) ⋯
b : Ordinal.{u}
hb : Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) b
⊢ ∃ (y : (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))),
    Membership.mem (γ := Set (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
        (range fun (i : β) ↦
          Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x)
            (f i) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
          hb ≤
        y
have hb₁ : ∃ (i : β), b ≤ f i
Tactic: rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this :
  StrictMono.{v, u + 1} (β := (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))) fun (i : β) ↦
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) (f i) ⋯
b : Ordinal.{u}
hb_1 : Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) b
hb : ∃ (i : β), b ≤ f i
⊢ ∃ (y : (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))),
    Membership.mem (γ := Set (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
        (range fun (i : β) ↦
          Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x)
            (f i) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
          hb_1 ≤
        y
have refine_2 : ∀ (i : β) (hi : b ≤ f i),
  ∃ (y : (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1))),
    Membership.mem (γ := Set (↑(Iio (⨆ (i : β), f i + 1)) : Type (u + 1)))
        (range fun (i : β) ↦
          Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x)
            (f i) sorry)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
          hb_1 ≤
        y
Tactic: obtain ⟨i, hi⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) (f i)
have refine_1 : f i < ⨆ (i : β), f i + 1
Tactic: rw [mem_Iio]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
inst_2 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i)) = Cardinal.lift.{u, v} (Order.cof β)
have rw : Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
Tactic: rw [← iSup_add_one hf, lift_cof_iSup_add_one hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
inst_2 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
rw : Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i)) = Cardinal.lift.{u, v} (Order.cof β)
have rw₁ : Cardinal.lift.{u, v} (Order.cof β) = Cardinal.lift.{u, v} (Order.cof β)
Tactic: rw [← iSup_add_one hf, lift_cof_iSup_add_one hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i) = a.cof
have rw : cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i + 1) = a.cof
Tactic: rw [← iSup_Iio_add_one hf ha, cof_iSup_Iio_add_one hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
rw : cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i + 1) = a.cof
⊢ cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i) = a.cof
have rw₁ : a.cof = a.cof
Tactic: rw [← iSup_Iio_add_one hf ha, cof_iSup_Iio_add_one hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ (f a).cof = a.cof
have rw : StrictMono (β := Ordinal.{u_1}) fun (b : (↑(Iio a) : Type (u_1 + 1))) ↦ f (↑b : Ordinal.{u_1})
Tactic: rw [hf.apply_of_isSuccLimit ha, cof_iSup_Iio _ ha.isSuccPrelimit]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
h : ∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof
⊢ (a + 1).cof ≤ (f (a + 1)).cof
have add_one : f (a + 1) ≠ 0
Tactic: rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
h : ∀ o' < a, ∀ (h : a = o'), a.cof ≤ (f a).cof
⊢ a.cof ≤ (f a).cof
have limit : a.cof ≤ a.cof
Tactic: rw [cof_map_of_isNormal hf ha]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof
have zero : cof 0 ≤ (f 0).cof
Tactic: cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
zero : cof 0 ≤ (f 0).cof
⊢ a.cof ≤ (f a).cof
have add_one : ∀ (a : Ordinal.{u_1}), (∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof) → (a + 1).cof ≤ (f (a + 1)).cof
Tactic: cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
zero : cof 0 ≤ (f 0).cof
add_one : ∀ (a : Ordinal.{u_1}), (∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof) → (a + 1).cof ≤ (f (a + 1)).cof
⊢ a.cof ≤ (f a).cof
have limit : ∀ (ha : IsSuccLimit a), (∀ o' < a, ∀ (h : a = o'), a.cof ≤ (f a).cof) → a.cof ≤ (f a).cof
Tactic: cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]