awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)) < Order.cof (↑s : Type (u + 1))
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

Tactic:
ha.not_ge (cof_le_cardinalMk _)

Premises used: LT.lt.not_ge, Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)) < Order.cof (↑s : Type (u + 1))
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

Tactic:
exact ha.not_ge (cof_le_cardinalMk _)

Premises used: LT.lt.not_ge, Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
(sSup_le_sSup_add_one s).trans_lt (sSup_add_one_lt_of_lt_cof ha hs)

Premises used: Ordinal.sSup_add_one_lt_of_lt_cof, Ordinal.sSup_le_sSup_add_one, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
rw : sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) < a
⊢ ⨆ (i : β), f i + 1 < a

Tactic:
rw [iSup, range_comp' (· + 1)]

Premises used: iSup, HAdd.hAdd, OfNat.ofNat, Set.range_comp'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 ∈ range f, i < a

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
apply : #(↑(range f) : Type (u + 1)) < (lift.{u + 1, u} a).cof
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) < a

Tactic:
apply sSup_add_one_lt_of_lt_cof _ (by simpa)

Premises used: Ordinal.sSup_add_one_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
rw : Cardinal.lift.{v, u + 1} #(↑(range f) : Type (u + 1)) < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
⊢ #(↑(range f) : Type (u + 1)) < (lift.{u + 1, u} a).cof

Tactic:
rw [← Cardinal.lift_lt.{_, v}]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
apply : Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
⊢ Cardinal.lift.{v, u + 1} #(↑(range f) : Type (u + 1)) < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof

Tactic:
apply mk_range_le_lift.trans_lt

Premises used: LE.le.trans_lt, Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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, 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
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
ha₁ : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
⊢ ∀ (i : β), f i < a

Tactic:
rw [← Cardinal.lift_lt.{_, u + 1}] at ha
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max 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

Tactic:
simpa [← lift_cof] using ha

Premises used: Ordinal.lift_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof

Tactic:
rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha

Premises used: Ordinal.lift_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
ha₁ : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
⊢ ∀ (i : α), f i < a

Tactic:
rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha

Premises used: Ordinal.lift_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ (i : α), f i + 1 < a

Tactic:
simpa using lift_iSup_add_one_lt_of_lt_cof ha hf

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 < a

Tactic:
(iSup_le_iSup_add_one f).trans_lt (lift_iSup_add_one_lt_of_lt_cof ha hf)

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof, Ordinal.iSup_le_iSup_add_one, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ (i : α), f i < a

Tactic:
simpa using lift_iSup_lt_of_lt_cof ha hf

Premises used: Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : Small.{u, v} β
f : β → Ordinal.{u}
by_contra! : ∀ (hf : Cardinal.lift.{u, v} #β < (lift.{v, u} (⨆ (i : β), f i + 1)).cof), False
⊢ (lift.{v, u} (⨆ (i : β), f i + 1)).cof ≤ Cardinal.lift.{u, v} #β

Tactic:
by_contra! hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : Small.{u, v} β
f : β → Ordinal.{u}
hf : Cardinal.lift.{u, v} #β < (lift.{v, u} (⨆ (i : β), f i + 1)).cof
⊢ False

Tactic:
(lift_iSup_add_one_lt_of_lt_cof hf <| Ordinal.lt_iSup_add_one _).false

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof, Ordinal.lt_iSup_add_one, LT.lt.false
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : Small.{u, v} β
f : β → Ordinal.{u}
hf : Cardinal.lift.{u, v} #β < (lift.{v, u} (⨆ (i : β), f i + 1)).cof
⊢ False

Tactic:
exact (lift_iSup_add_one_lt_of_lt_cof hf <| Ordinal.lt_iSup_add_one _).false

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof, Ordinal.lt_iSup_add_one, LT.lt.false
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Ordinal.{u}
⊢ cof (⨆ (i : α), f i + 1) ≤ #α

Tactic:
simpa using cof_lift_iSup_add_one_le f

Premises used: Ordinal.cof_lift_iSup_add_one_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rw : sSup (ord '' s) < a.ord
⊢ sSup s < a

Tactic:
rw [← ord_lt_ord, sSup_ord]

Premises used: Ordinal.sSup_ord, Cardinal.ord_lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
hs₁ : ∀ i ∈ ord '' s, i < a.ord
⊢ sSup (ord '' s) < a.ord

Tactic:
apply Ordinal.sSup_lt_of_lt_cof

Premises used: Ordinal.sSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ #(↑(ord '' s) : Type (u + 1)) < (lift.{u + 1, u} a.ord).cof

Tactic:
simpa [mk_image_eq ord_injective]

Premises used: Cardinal.mk_image_eq, Cardinal.ord_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ ∀ i ∈ ord '' s, i < a.ord

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rw : ⨆ (i : β), (f i).ord < a.ord
⊢ ⨆ (i : β), f i < a

Tactic:
rw [← ord_lt_ord, iSup_ord]

Premises used: Ordinal.iSup_ord, Cardinal.ord_lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
hf₁ : ∀ (i : β), (f i).ord < a.ord
⊢ ⨆ (i : β), (f i).ord < a.ord

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof

Premises used: Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ Cardinal.lift.{u, v} #β < (lift.{v, u} a.ord).cof

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
rw : ⨆ (i : α), (f i).ord < a.ord
⊢ ⨆ (i : α), f i < a

Tactic:
rw [← ord_lt_ord, iSup_ord]

Premises used: Ordinal.iSup_ord, Cardinal.ord_lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
ha₁ : #α < a.ord.cof
hf₁ : ∀ (i : α), (f i).ord < a.ord
⊢ ⨆ (i : α), (f i).ord < a.ord

Tactic:
apply Ordinal.iSup_lt_of_lt_cof

Premises used: Ordinal.iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ #α < a.ord.cof

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ∀ (i : α), (f i).ord < a.ord

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
⊢ Set.Nonempty.{u + 1} (α := Cardinal.{u})
    {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}

Tactic:
⟨_, ⟨_, _, lsub_typein o, mk_toType o⟩⟩

Premises used: Set.Nonempty, Ordinal.lsub_typein, And.intro, Cardinal.mk_toType, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
⊢ o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}

Tactic:
le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)

Premises used: le_csInf, csInf_le', Ordinal.cof_lsub_def_nonempty, le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
refine_2 :
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    o.cof
⊢ o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}

Tactic:
refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)

Premises used: le_csInf, csInf_le', Ordinal.cof_lsub_def_nonempty, le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
refine_1 : (lsub f).cof ≤ #ι
⊢ o.cof ≤ #ι

Tactic:
rw [← hf]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ (lsub f).cof ≤ #ι

Tactic:
cof_iSup_add_one_le f

Premises used: Ordinal.cof_iSup_add_one_le, Order.succ, Ordinal.lsub
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ (lsub f).cof ≤ #ι

Tactic:
exact cof_iSup_add_one_le f

Premises used: Ordinal.cof_iSup_add_one_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
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
⊢ 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'⟩

Premises used: Order.cof_eq, Ordinal.ToType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hS' : #(↑S : Type u) = o.cof), #(↑S : Type u) = o.cof
⊢ #(↑S : Type u) = o.cof

Tactic:
rwa [cof_toType] at hS'

Premises used: Ordinal.cof_toType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)
refine_2 : ∀ (a : Ordinal.{u}) (ha : a < o), a < lsub f
⊢ Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    o.cof

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'⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 < type fun (x1 x2 : o.ToType) ↦ x1 < x2

Tactic:
rw [← type_toType o] at ha

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
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
⊢ a < lsub f

Tactic:
rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩

Premises used: Subtype.mk, LT.lt, Ordinal.enum, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 ≤
    (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'

Premises used: Ordinal.typein_le_typein, Ordinal.typein_enum, not_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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' :
  a ≤
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      b
⊢ a < lsub f

Tactic:
hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)

Premises used: Subtype.mk, Ordinal.lt_lsub, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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' :
  a ≤
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : o.ToType) → Ordinal.{u})
      b
⊢ a < lsub f

Tactic:
exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
rw :
  ∃ (ι : Type u) (f : ι → Ordinal.{u}),
    lsub f = o ∧ #ι = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
⊢ ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = o.cof

Tactic:
rw [cof_eq_sInf_lsub]

Premises used: Ordinal.cof_eq_sInf_lsub
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
⊢ ∃ (ι : Type u) (f : ι → Ordinal.{u}),
    lsub f = o ∧ #ι = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}

Tactic:
csInf_mem (cof_lsub_def_nonempty o)

Premises used: csInf_mem, Set.Mem, setOf, Ordinal.cof_lsub_def_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
⊢ ∃ (ι : Type u) (f : ι → Ordinal.{u}),
    lsub f = o ∧ #ι = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}

Tactic:
exact csInf_mem (cof_lsub_def_nonempty o)

Premises used: csInf_mem, Ordinal.cof_lsub_def_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{u}
⊢ (lsub f).cof ≤ #ι

Tactic:
cof_iSup_add_one_le f

Premises used: Ordinal.cof_iSup_add_one_le, Order.succ, Ordinal.lsub
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
rw : (lift.{u, max u v} (lsub.{u, v} f)).cof ≤ Cardinal.lift.{max u v, u} #ι
⊢ (lsub.{u, v} f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← lift_id'.{u} (lsub f), ← Cardinal.lift_umax.{u, v}]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub.{u, v} f)).cof ≤ Cardinal.lift.{max u v, u} #ι

Tactic:
cof_lift_iSup_add_one_le _

Premises used: Order.succ, Ordinal.lsub, Ordinal.cof_lift_iSup_add_one_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub.{u, v} f)).cof ≤ Cardinal.lift.{max u v, u} #ι

Tactic:
exact cof_lift_iSup_add_one_le _

Premises used: Ordinal.cof_lift_iSup_add_one_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
rw :
  a ≤ sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a} ↔
    ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
rw [cof_eq_sInf_lsub]

Premises used: Ordinal.cof_eq_sInf_lsub
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
h :
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    b
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
rw : a ≤ #ι
⊢ a ≤ b

Tactic:
rw [← hb]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
h :
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    b
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Tactic:
H _ hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
h :
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    b
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Tactic:
exact H _ hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a} ↔
    ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
exact
    (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
      ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
        rw [← hb]
        exact H _ hf⟩

Premises used: Cardinal.mk, LE.le, Ordinal.cof_lsub_def_nonempty, _private.0.Ordinal.le_cof_iff_lsub.match_1, le_csInf_iff'', And.intro, Iff.intro, Exists.intro, Iff.trans, rfl