awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
⊢ Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
have refine : ∀ (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)))
  ⦃a₂ : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))⦄,
  Eq.{u + 2} (α := (↑(Iio a) : Type (u + 1)))
      ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
              (↑((f :
                      (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                        (↑s : Type (u + 1)))
                    x) :
                Ordinal.{u})
              sorry :
            { x : Ordinal.{u} // x ∈ Iio a }))
        x)
      ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
              (↑((f :
                      (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                        (↑s : Type (u + 1)))
                    x) :
                Ordinal.{u})
              sorry :
            { x : Ordinal.{u} // x ∈ Iio a }))
        a₂) →
    x = a₂
Tactic: refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' s) < a
have this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
Tactic: have : Small.{u} (Iio (typeLT s)) := by
    refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_
    simp [Subtype.val_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
have h : s =
  range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
    (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1))) i) :
      Ordinal.{u})
Tactic: convert! range_comp (· + 1) (fun i ↦ (f i).1)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ s =
    range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
have h : s = image (α := (↑s : Type (u + 1))) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ s)) Set.univ
Tactic: rw [range_comp', f.range_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' s) < a
have this₁ : Eq (α := Set Ordinal.{u})
  (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
    HAdd.hAdd (α := Ordinal.{u})
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
      1)
  ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
Tactic: have : range (fun i ↦ (f i).1 + 1) = (· + 1) '' s := by
    convert! range_comp (· + 1) (fun i ↦ (f i).1)
    rw [range_comp', f.range_eq]
    simp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' s) < a
have rw : ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
    HAdd.hAdd (α := Ordinal.{u})
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
      1 <
  a
Tactic: rw [← this, sSup_range]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
⊢ ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 <
    a
have a₁ : ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
    HAdd.hAdd (α := Ordinal.{u})
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
      1 ≤
  a
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
a₁ :
  ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 ≤
    a
⊢ ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 <
    a
have a₂ : ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
    HAdd.hAdd (α := Ordinal.{u})
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
      1 ≠
  a
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
s : Set Ordinal.{u}
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
ha :
  #(↑s : Type (u + 1)) <
    (lift.{u + 1, u}
        (⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
          HAdd.hAdd (α := Ordinal.{u})
            (↑((f :
                    (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                      (↑s : Type (u + 1)))
                  i) :
              Ordinal.{u})
            1)).cof
hs :
  ∀ i ∈ s,
    i <
      ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
        HAdd.hAdd (α := Ordinal.{u})
          (↑((f :
                  (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                    (↑s : Type (u + 1)))
                i) :
            Ordinal.{u})
          1
⊢ False
have ha₁ : #(↑s : Type (u + 1)) < Order.cof (↑s : Type (u + 1))
Tactic: rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
      Cardinal.lift_lift, Cardinal.lift_lt] at ha
Cleared hypotheses: ha, hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ ⨆ (i : β), f i + 1 < a
have rw : sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) < a
Tactic: rw [iSup, range_comp' (· + 1)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) < a
have apply : #(↑(range f) : Type (u + 1)) < (lift.{u + 1, u} a).cof
Tactic: apply sSup_add_one_lt_of_lt_cof _ (by simpa)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ #(↑(range f) : Type (u + 1)) < (lift.{u + 1, u} a).cof
have rw : Cardinal.lift.{v, u + 1} #(↑(range f) : Type (u + 1)) < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
Tactic: rw [← Cardinal.lift_lt.{_, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{v, u + 1} #(↑(range f) : Type (u + 1)) < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
have apply : Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
Tactic: apply mk_range_le_lift.trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
have ha₁ : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
Tactic: rw [← Cardinal.lift_lt.{_, u + 1}] at ha
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ (i : α), f i + 1 < a
have ha₁ : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
Tactic: rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ (i : α), f i < a
have ha₁ : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
Tactic: rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
inst : Small.{u, v} β
f : β → Ordinal.{u}
⊢ (lift.{v, u} (⨆ (i : β), f i + 1)).cof ≤ Cardinal.lift.{u, v} #β
have by_contra! : ∀ (hf : Cardinal.lift.{u, v} #β < (lift.{v, u} (⨆ (i : β), f i + 1)).cof), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #(↑s : Type (u + 1)) < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a
have rw : sSup (ord '' s) < a.ord
Tactic: rw [← ord_lt_ord, sSup_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #(↑s : Type (u + 1)) < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup (ord '' s) < a.ord
have ha₁ : #(↑(ord '' s) : Type (u + 1)) < (lift.{u + 1, u} a.ord).cof
Tactic: apply Ordinal.sSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #(↑s : Type (u + 1)) < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
ha₁ : #(↑(ord '' s) : Type (u + 1)) < (lift.{u + 1, u} a.ord).cof
⊢ sSup (ord '' s) < a.ord
have hs₁ : ∀ i ∈ ord '' s, i < a.ord
Tactic: apply Ordinal.sSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ⨆ (i : β), f i < a
have rw : ⨆ (i : β), (f i).ord < a.ord
Tactic: rw [← ord_lt_ord, iSup_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ⨆ (i : β), (f i).ord < a.ord
have ha₁ : Cardinal.lift.{u, v} #β < (lift.{v, u} a.ord).cof
Tactic: apply Ordinal.lift_iSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
ha₁ : Cardinal.lift.{u, v} #β < (lift.{v, u} a.ord).cof
⊢ ⨆ (i : β), (f i).ord < a.ord
have hf₁ : ∀ (i : β), (f i).ord < a.ord
Tactic: apply Ordinal.lift_iSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ (i : α), f i < a
have rw : ⨆ (i : α), (f i).ord < a.ord
Tactic: rw [← ord_lt_ord, iSup_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
ha₁ : #α < a.ord.cof
⊢ ⨆ (i : α), (f i).ord < a.ord
have hf₁ : ∀ (i : α), (f i).ord < a.ord
Tactic: apply Ordinal.iSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
have refine_1 : ∀ (b : Cardinal.{u}),
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
      b →
    o.cof ≤ b
Tactic: refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
refine_1 :
  ∀ (b : Cardinal.{u}),
    Membership.mem (γ := Set Cardinal.{u})
        {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a} b →
      o.cof ≤ b
⊢ o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
have refine_2 : Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
  o.cof
Tactic: refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ o.cof ≤ #ι
have refine_1 : (lsub f).cof ≤ #ι
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    o.cof
have refine_2 : ∀ (S : Set o.ToType) (hS : IsCofinal S) (hS' : #(↑S : Type u) = Order.cof o.ToType),
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    o.cof
Tactic: rcases Order.cof_eq (α := o.ToType) with ⟨S, hS, hS'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #(↑S : Type u) = Order.cof o.ToType
f : (↑S : Type u) → Ordinal.{u} :=
  fun (s : (↑S : Type u)) ↦
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      (↑s : o.ToType)
⊢ #(↑S : Type u) = o.cof
have rwa : ∀ (hS' : #(↑S : Type u) = o.cof), #(↑S : Type u) = o.cof
Tactic: rwa [cof_toType] at hS'
Cleared hypotheses: hS', f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #(↑S : Type u) = Order.cof o.ToType
f : (↑S : Type u) → Ordinal.{u} :=
  fun (s : (↑S : Type u)) ↦
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      (↑s : o.ToType)
⊢ Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    o.cof
have refine_2 : ∀ (a : Ordinal.{u}) (ha : a < o), a < lsub f
Tactic: refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [cof_toType] at hS'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #(↑S : Type u) = Order.cof o.ToType
f : (↑S : Type u) → Ordinal.{u} :=
  fun (s : (↑S : Type u)) ↦
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      (↑s : o.ToType)
a : Ordinal.{u}
ha : a < o
⊢ a < lsub f
have ha₁ : a < type fun (x1 x2 : o.ToType) ↦ x1 < x2
Tactic: rw [← type_toType o] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #(↑S : Type u) = Order.cof o.ToType
f : (↑S : Type u) → Ordinal.{u} :=
  fun (s : (↑S : Type u)) ↦
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      (↑s : o.ToType)
a : Ordinal.{u}
ha : a < type fun (x1 x2 : o.ToType) ↦ x1 < x2
⊢ a < lsub f
have refine_2 : ∀ (b : o.ToType) (hb : b ∈ S)
  (hb' :
    (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u + 1))) → o.ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) a ha) ≤
      b),
  a < lsub f
Tactic: rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #(↑S : Type u) = Order.cof o.ToType
f : (↑S : Type u) → Ordinal.{u} :=
  fun (s : (↑S : Type u)) ↦
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      (↑s : o.ToType)
a : Ordinal.{u}
ha : a < type fun (x1 x2 : o.ToType) ↦ x1 < x2
b : o.ToType
hb : b ∈ S
hb' :
  (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u + 1))) → o.ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) a ha) ≤
    b
⊢ a < lsub f
have hb'₁ : a ≤
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
      (a : o.ToType) → Ordinal.{u})
    b
Tactic: rw [← not_lt, ← typein_le_typein, typein_enum] at hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = o.cof
have rw : ∃ (ι : Type u) (f : ι → Ordinal.{u}),
  lsub f = o ∧ #ι = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
Tactic: rw [cof_eq_sInf_lsub]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lsub.{u, v} f).cof ≤ Cardinal.lift.{v, u} #ι
have rw : (lift.{u, max u v} (lsub.{u, v} f)).cof ≤ Cardinal.lift.{max u v, u} #ι
Tactic: rw [← lift_id'.{u} (lsub f), ← Cardinal.lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
have rw : a ≤ sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a} ↔
  ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
Tactic: rw [cof_eq_sInf_lsub]