awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
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 : α) ⋯)
          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) ∨
      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))
⊢ 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)

Tactic:
apply (trichotomous_of r _ _).resolve_right

Premises used: Or.resolve_right, trichotomous_of
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
h :
  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 : α) ⋯)
      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)
⊢ False

Tactic:
simp_all [Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)
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 : α) ⋯ <
        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 : α) ⋯)
          (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 : α) ⋯))),
    False
⊢ False

Tactic:
obtain ⟨x, z, hz, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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})
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)
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 : α) ⋯ <
    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 : α) ⋯)
      (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 : α) ⋯))
⊢ False

Tactic:
(hz _ hxy').asymm hxy

Premises used: LT.lt.asymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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})
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)
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 : α) ⋯ <
    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 : α) ⋯)
      (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 : α) ⋯))
⊢ False

Tactic:
exact (hz _ hxy').asymm hxy

Premises used: LT.lt.asymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
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 α
⊢ (Order.cof α).ord.cof = Order.cof α

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α

Premises used: Ordinal.exists_ord_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rw : Order.cof (↑s : Type u_1) = Order.cof α
⊢ (Order.cof α).ord.cof = Order.cof α

Tactic:
rw [← hs', cof_type]

Premises used: Ordinal.cof_type
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 α
a₁ : Order.cof α ≤ Order.cof (↑s : Type u_1)
⊢ Order.cof (↑s : Type u_1) = Order.cof α

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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) ≤ #(↑s : Type u_1)
⊢ Order.cof (↑s : Type u_1) ≤ Order.cof α

Tactic:
rw [← card_ord (Order.cof α), ← hs', card_type]

Premises used: Ordinal.card_type, Cardinal.card_ord, Order.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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) ≤ #(↑s : Type u_1)

Tactic:
cof_le_cardinalMk s

Premises used: Set.Elem, Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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) ≤ #(↑s : Type u_1)

Tactic:
exact cof_le_cardinalMk s

Premises used: Set.Elem, Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 : ∀ (s_1 : Set (↑s : Type u_1)), IsCofinal s_1 → Order.cof α ≤ #(↑s_1 : Type u_1)
⊢ Order.cof α ≤ Order.cof (↑s : Type u_1)

Tactic:
rw [le_cof_iff]

Premises used: Order.le_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ ∀ (s_1 : Set (↑s : Type u_1)), IsCofinal s_1 → Order.cof α ≤ #(↑s_1 : Type u_1)

Tactic:
fun t ht ↦ (cof_le (hs.trans ht)).trans_eq (mk_image_eq Subtype.val_injective)

Premises used: LE.le.trans_eq, Subtype.val_injective, IsCofinal.trans, Cardinal.mk_image_eq, Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ ∀ (s_1 : Set (↑s : Type u_1)), IsCofinal s_1 → Order.cof α ≤ #(↑s_1 : Type u_1)

Tactic:
exact fun t ht ↦ (cof_le (hs.trans ht)).trans_eq (mk_image_eq Subtype.val_injective)

Premises used: LE.le.trans_eq, Subtype.val_injective, IsCofinal.trans, Cardinal.mk_image_eq, Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.cof.ord.cof = o.cof

Tactic:
simpa using Order.cof_ord_cof o.ToType

Premises used: Order.cof_ord_cof, Ordinal.ToType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 β)
refine_1 : ∀ (i : β), Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) (f i)
⊢ 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
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 β)
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)
        ⋯)
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
have := lift_cof_congr_of_strictMono this ?_
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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)))
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)))
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i + 1)) = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
rw [← Cardinal.lift_inj.{_, max (u + 1) v}, Cardinal.lift_lift.{_, _, v},
        Cardinal.lift_umax.{_, u + 1}, Cardinal.lift_umax.{_, u + 1}, this]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.{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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ ∃ (i : β), b ≤ f i

Tactic:
rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb

Premises used: Set.mem_Iio, Ordinal.lt_iSup_add_one_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
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) ⋯)
          y ∧
        Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
            hb_1 ≤
          y
⊢ ∃ (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

Tactic:
obtain ⟨i, hi⟩ := hb
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
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) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
          hb ≤
        y

Tactic:
⟨_, Set.mem_range_self i, hi⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
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) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u}) ↦ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) x) b
          hb ≤
        y

Tactic:
exact ⟨_, Set.mem_range_self i, hi⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
refine_1 : f i < ⨆ (i : β), f i + 1
⊢ Membership.mem (γ := Set Ordinal.{u}) (Iio (⨆ (i : β), f i + 1)) (f i)

Tactic:
rw [mem_Iio]

Premises used: Set.mem_Iio
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i < ⨆ (i : β), f i + 1

Tactic:
(lt_add_one _).trans_le <| le_ciSup bddAbove_of_small _

Premises used: lt_add_one, Ordinal.bddAbove_of_small, le_ciSup, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
β : Type v
inst : LinearOrder β
inst_1 : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i < ⨆ (i : β), f i + 1

Tactic:
exact (lt_add_one _).trans_le <| le_ciSup bddAbove_of_small _

Premises used: lt_add_one, Ordinal.bddAbove_of_small, le_ciSup, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
γ : Type u
inst : LinearOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ cof (⨆ (i : γ), f i + 1) = Order.cof γ

Tactic:
simpa using lift_cof_iSup_add_one hf

Premises used: Ordinal.lift_cof_iSup_add_one
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 β)
rw₁ rw₂ : Cardinal.lift.{u, v} (Order.cof β) = Cardinal.lift.{u, v} (Order.cof β)
⊢ Cardinal.lift.{v, u} (cof (⨆ (i : β), f i)) = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
rw [← iSup_add_one hf, lift_cof_iSup_add_one hf]

Premises used: Ordinal.lift_cof_iSup_add_one, Ordinal.iSup_add_one
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
γ : Type u
inst : LinearOrder γ
inst_1 : NoMaxOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ cof (⨆ (i : γ), f i) = Order.cof γ

Tactic:
simpa using lift_cof_iSup hf

Premises used: Ordinal.lift_cof_iSup