awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (a b : { x : α // x ∈ s }), a < b → (↑a : α) < (↑b : α)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
apply : (type fun (x1 x2 : α) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2
⊢ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
apply (RelEmbedding.ofMonotone Subtype.val (by simp)).ordinal_type_le.antisymm

Premises used: LE.le.antisymm, RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, Subtype.val
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
rw : cof α ≤ #{ x : α // x ∈ s }
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2

Tactic:
rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk]

Premises used: Cardinal.ord_le, Cardinal.ord_cardinalMk, Order.cof_eq_cardinalMk, Ordinal.card_type
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ cof α ≤ #{ x : α // x ∈ s }

Tactic:
cof_le hs

Premises used: Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ cof α ≤ #{ x : α // x ∈ s }

Tactic:
exact cof_le hs

Premises used: Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
a o : α
s : Set α
hs : IsCofinal s
ho : o ∈ s
H : ∀ b < a, (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α) < o
rw : a ≤ ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)
⊢ (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) ≤ o

Tactic:
rw [← Subtype.coe_mk o ho, Subtype.coe_le_coe, ← OrderIso.le_symm_apply]

Premises used: Subtype.coe_mk, Subtype.coe_le_coe, OrderIso.le_symm_apply
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
a o : α
s : Set α
hs : IsCofinal s
ho : o ∈ s
H : ∀ b < a, (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α) < o
H₁ : ∀ c < a, c < ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)
⊢ a ≤ ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)

Tactic:
apply le_of_forall_lt

Premises used: le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
a o : α
s : Set α
hs : IsCofinal s
ho : o ∈ s
H : ∀ b < a, (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α) < o
⊢ ∀ c < a, c < ((enum s hs).symm : (a : { x : α // x ∈ s }) → α) (Subtype.mk (p := Membership.mem s) o ho)

Tactic:
simpa [OrderIso.lt_symm_apply]

Premises used: OrderIso.lt_symm_apply
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
inst_3 : SuccOrder α
a o : α
s : Set α
hs : IsCofinal s
ha : o ∈ s
H : (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) < o
⊢ (↑((enum s hs : (a : α) → (↑s : Type u_1)) (succ a)) : α) ≤ o

Tactic:
enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_

Premises used: LT.lt.trans_le', Order.enum_le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
inst_3 : SuccOrder α
a o : α
s : Set α
hs : IsCofinal s
ha : o ∈ s
H : (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) < o
refine :
  ∀ (b : α) (hb : b < succ a),
    LE.le.{u_1} (α := α) (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α)
      (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α)
⊢ (↑((enum s hs : (a : α) → (↑s : Type u_1)) (succ a)) : α) ≤ o

Tactic:
refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_

Premises used: LT.lt.trans_le', Order.enum_le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
inst_3 : SuccOrder α
a o : α
s : Set α
hs : IsCofinal s
ha : o ∈ s
H : (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α) < o
b : α
hb : b < succ a
⊢ LE.le.{u_1} (α := α) (↑((enum s hs : (a : α) → (↑s : Type u_1)) b) : α)
    (↑((enum s hs : (a : α) → (↑s : Type u_1)) a) : α)

Tactic:
simpa using le_of_lt_succ hb

Premises used: Order.le_of_lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
x : α
rw :
  (OrderIso.symm OrderIso.Set.univ : (a : α) → (↑Set.univ : Type u_1)) x =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) Set.univ x) x ⋯
⊢ (enum Set.univ ⋯ : (a : α) → (↑Set.univ : Type u_1)) x =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) Set.univ x) x ⋯

Tactic:
rw [← Subsingleton.allEq OrderIso.Set.univ.symm (enum univ .univ)]

Premises used: Set.univ, OrderIso.symm, OrderIso.Set.univ, Subsingleton.allEq, IsCofinal.univ, Order.enum
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
x : α
⊢ (OrderIso.symm OrderIso.Set.univ : (a : α) → (↑Set.univ : Type u_1)) x =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) Set.univ x) x ⋯

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ cof ℤ = ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2).cof = Order.cof α

Tactic:
liftOnWellOrder_type ..

Premises used: Ordinal.liftOnWellOrder_type, Ordinal.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
rw : Order.cof o.ToType
| o.cof

Tactic:
rw [← type_toType o, cof_type]

Premises used: Ordinal.cof_type, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
conv_rhs : Order.cof o.ToType = o.cof
conv_rhs₁ : Order.cof o.ToType = Order.cof o.ToType
⊢ Order.cof o.ToType = o.cof

Tactic:
conv_rhs => rw [← type_toType o, cof_type]

Premises used: Ordinal.cof_type, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
type :
  ∀ (α : Type u) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
    Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
      (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
⊢ Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof

Tactic:
cases o using inductionOnWellOrder with | type α

Premises used: Ordinal.type
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
type : Cardinal.lift.{v, u} (Order.cof α) = (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof
type₁ : Cardinal.lift.{v, u} (Order.cof α) = (Ordinal.type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2).cof
type₂ : Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)
type₃ : Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
type₄ : Cardinal.lift.{max u v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
type₅ type₆ :
  Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α)) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
⊢ Cardinal.lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2).cof =
    (lift.{v, u} (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)).cof

Tactic:
rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]

Premises used: Ordinal.type_lt_ulift, Ordinal.cof_type, OrderIso.lift_cof_congr, Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
x : α
⊢ Order.cof (↑(Iio x) : Type u) =
    cof
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        x)

Tactic:
(cof_type _).symm

Premises used: Set.Mem, Ordinal.cof_type, setOf, Ordinal.type, Subrel, Eq.symm, Set.Iio, Order.Preimage
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
rw :
  cof
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦
            x1 < x2) (typein fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o) =
    (lift.{u + 1, u} o).cof
rw₁ rw₂ : (lift.{u + 1, u} o).cof = (lift.{u + 1, u} o).cof
⊢ Order.cof (↑(Iio o) : Type (u + 1)) = (lift.{u + 1, u} o).cof

Tactic:
rw [Order.cof_Iio, typein_ordinal]

Premises used: Order.cof_Iio, Ordinal.typein_ordinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.cof ≤ o.card

Tactic:
simpa using cof_le_cardinalMk o.ToType

Premises used: Ordinal.ToType, Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
c : Cardinal.{u_1}
⊢ c.ord.cof ≤ c

Tactic:
simpa using cof_le_card c.ord

Premises used: Ordinal.cof_le_card, Cardinal.ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.cof.ord ≤ o

Tactic:
(ord_le_ord.2 (cof_le_card o)).trans (ord_card_le o)

Premises used: Iff.mpr, Ordinal.cof_le_card, Cardinal.ord_le_ord, LE.le.trans, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
rw : Order.cof o.ToType = 0 ↔ o = 0
rw₁ : IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
rw₂ rw₃ : o = 0 ↔ o = 0
⊢ o.cof = 0 ↔ o = 0

Tactic:
rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]

Premises used: Order.cof_eq_zero_iff, Ordinal.cof_toType, Ordinal.isEmpty_toType_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.cof ≠ 0 ↔ o ≠ 0

Tactic:
cof_eq_zero.not

Premises used: Iff.not, Ordinal.cof_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ 0 < o.cof ↔ 0 < o

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ cof 0 = 0

Tactic:
cof_eq_zero.2 rfl

Premises used: Iff.mpr, Ordinal.cof_eq_zero, rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ (o + 1).cof = 1

Tactic:
cof_eq_one_iff.2 (mem_range_self o)

Premises used: Set.mem_range_self, Iff.mpr, Ordinal.cof_eq_one_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ cof 1 = 1

Tactic:
simpa using cof_add_one 0

Premises used: Ordinal.cof_add_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ (succ o).cof = 1

Tactic:
cof_add_one o

Premises used: Ordinal.cof_add_one, Order.succ
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
rw : ¬1 < o.cof ↔ ¬IsSuccLimit o
rw₁ : o.cof ≤ 1 ↔ ¬IsSuccLimit o
rw₂ : o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
rw₃ : o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)
rw₄ : o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
rw₅ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ ¬IsSuccPrelimit o
rw₆ : o.cof = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
rw₇ : o = 0 ∨ o.cof = 1 ↔ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
rw₈ rw₉ :
  o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o ↔
    o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o
⊢ 1 < o.cof ↔ IsSuccLimit o

Tactic:
rw [← not_iff_not, not_lt, Cardinal.le_one_iff, isSuccLimit_iff,
    not_and_or, not_ne_iff, not_isSuccPrelimit_iff_mem_range_succ, cof_eq_zero, cof_eq_one_iff]

Premises used: not_iff_not, not_ne_iff, Order.not_isSuccPrelimit_iff_mem_range_succ, Ordinal.isSuccLimit_iff, Cardinal.le_one_iff, not_lt, not_and_or, Ordinal.cof_eq_one_iff, Ordinal.cof_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1

Tactic:
simpa using Order.cof_lt_aleph0_iff (α := o.ToType)

Premises used: Order.cof_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ 1 < o.cof

Tactic:
simp [← not_lt]

Premises used: not_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
rw : 1 < o.cof ↔ IsSuccLimit o
rw₁ rw₂ : IsSuccLimit o ↔ IsSuccLimit o
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o

Tactic:
rw [aleph0_le_cof_iff, one_lt_cof_iff]

Premises used: Ordinal.aleph0_le_cof_iff, Ordinal.one_lt_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
apply : ℵ₀ ≤ o.cof
apply₁ : o.card ≤ ℵ₀
⊢ o.cof = ℵ₀

Tactic:
apply ((cof_le_card _).trans _).antisymm

Premises used: LE.le.antisymm, Ordinal.cof_le_card, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
rwa : 1 < o.cof
rwa₁ rwa₂ rwa₃ rwa₄ : IsSuccLimit o
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, one_lt_cof_iff]

Premises used: Ordinal.aleph0_le_cof_iff, Ordinal.one_lt_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
rwa : o < (succ ℵ₀).ord
rwa₁ : o < ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
rwa₂ rwa₃ rwa₄ rwa₅ : o < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
⊢ o.card ≤ ℵ₀

Tactic:
rwa [card_le_iff, succ_aleph0, ord_aleph]

Premises used: Cardinal.card_le_iff, Cardinal.ord_aleph, Cardinal.succ_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ ω.cof = ℵ₀

Tactic:
cof_eq_aleph0_of_isSuccLimit isSuccLimit_omega0 omega0_lt_omega_one

Premises used: Ordinal.omega0_lt_omega_one, Ordinal.isSuccLimit_omega0, Ordinal.cof_eq_aleph0_of_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
obtain :
  ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u_1) = Order.cof α),
    ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord

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

Premises used: Order.exists_cof_eq
-- 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 α
obtain :
  ∀ (r : (↑s : Type u_1) → (↑s : Type u_1) → Prop) (hr : IsWellOrder (↑s : Type u_1) r)
    (hr' : (#(↑s : Type u_1)).ord = type r),
    ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_ord_eq s

Premises used: Set.Elem, Cardinal.exists_ord_eq
-- 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
⊢ IsCofinal.{u_1} (α := α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a})

Tactic:
have ht := hs.trans (isCofinal_setOf_imp_lt r)
-- 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})
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord

Tactic:
⟨_, ht, (ord_le.2 (cof_le ht)).antisymm' ?_⟩

Premises used: Iff.mpr, LE.le.antisymm', Cardinal.ord_le, And.intro, Exists.intro
-- 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})
refine :
  (type
      fun
        (x1 x2 :
          (↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a}) :
            Type u_1)) ↦
      x1 < x2) ≤
    (Order.cof α).ord
⊢ ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord

Tactic:
refine ⟨_, ht, (ord_le.2 (cof_le ht)).antisymm' ?_⟩
-- 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})
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)
⊢ (type
      fun
        (x1 x2 :
          (↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                {a : (↑s : Type u_1) | ∀ (b : (↑s : Type u_1)), r b a → b < a}) :
            Type u_1)) ↦
      x1 < x2) ≤
    (Order.cof α).ord

Tactic:
rw [← hs', hr', type_le_iff']

Premises used: Ordinal.type_le_iff'
-- 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})
⊢ 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:
⟨.ofMonotone (fun x ↦ ⟨x.1, ?_⟩) fun x y hxy ↦ ?_⟩

Premises used: Nonempty.intro, Subtype.mk, RelEmbedding.ofMonotone, Subtype.val
-- 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})
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
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 : α) ⋯)
        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)
⊢ 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:
refine ⟨.ofMonotone (fun x ↦ ⟨x.1, ?_⟩) fun x y hxy ↦ ?_⟩
-- 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 :
  (↑(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:
grind