awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
rw :
  Eq (α := ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2))
          ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
                x1 < x2) (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
              (a : ToType 1) → Ordinal.{u_1})
            a)
          ⋯) :
      ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
          uniqueToTypeOne._proof_1) :
      ToType 1)
⊢ a =
    (enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
        uniqueToTypeOne._proof_1)

Tactic:
rw [← enum_typein (α := ToType 1) (· < ·) a]

Premises used: Ordinal.enum_typein, LT.lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
h :
  Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
⊢ Eq (α := ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2))
          ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
                x1 < x2) (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
              (a : ToType 1) → Ordinal.{u_1})
            a)
          ⋯) :
      ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
          uniqueToTypeOne._proof_1) :
      ToType 1)

Tactic:
congr
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
h :
  LT.lt (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (1 : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})

Tactic:
rw [← lt_one_iff]

Premises used: Order.lt_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ LT.lt (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (1 : Ordinal.{u_1})

Tactic:
apply typein_lt_self

Premises used: Ordinal.typein_lt_self
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ToType 1
⊢ 0 ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
x : ToType 1
⊢ x =
    (enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
        uniqueToTypeOne._proof_1)

Tactic:
Unique.eq_default x

Premises used: Unique.eq_default
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
simp_rw : Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsTop x
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsMax x

Tactic:
simp_rw [← isTop_iff_isMax]

Premises used: isTop_iff_isMax
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
mp : Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) → ∃ (x : α), IsTop x
mpr : (∃ (x : α), IsTop x) → Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsTop x

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
⊢ ∃ (x : α), IsTop x

Tactic:
⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩

Premises used: Subtype.mk, LT.lt, Exists.intro, Ordinal.enum, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
mp : a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
mp₁ :
  ∀ (b : α),
    b ≤
      (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) a ⋯)
⊢ ∃ (x : α), IsTop x

Tactic:
refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
mp : a < type fun (x1 x2 : α) ↦ x1 < x2
mp₁ : a < succ a
mp₂ mp₃ : a ≤ a
⊢ a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
rw [mem_Iio, ← ha, lt_succ_iff]

Premises used: Set.mem_Iio, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
b : α
mp :
  (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})
      b <
    type fun (x1 x2 : α) ↦ x1 < x2
⊢ b ≤
    (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) a ⋯)

Tactic:
rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]

Premises used: Ordinal.enum_typein, Order.lt_succ_iff, not_lt, Ordinal.enum_le_enum, LT.lt, Subtype.mk_le_mk
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
b : α
⊢ (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})
      b <
    type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
typein_lt_type ..

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
b : α
⊢ (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})
      b <
    type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
exact typein_lt_type ..

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩

Premises used: Set.Mem, eq_of_forall_lt_iff, setOf, PrincipalSeg.toRelEmbedding, LT.lt, Exists.intro, Set.range, DFunLike.coe, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
mpr :
  ∀ (o : Ordinal.{u}),
    o <
        succ
          ((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})
            a) ↔
      o < type fun (x1 x2 : α) ↦ x1 < x2
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
refine ⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
mpr :
  o ≤
      (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})
        a ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2
⊢ o <
      succ
        ((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})
          a) ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
rw [lt_succ_iff]

Premises used: Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o ≤
      (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})
        a ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨fun h ↦ h.trans_lt (typein_lt_type _ _), fun h ↦ ?_⟩

Premises used: Ordinal.typein_lt_type, LT.lt, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
mpr :
  ∀ (h : o < type fun (x1 x2 : α) ↦ x1 < x2),
    o ≤
      (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})
        a
⊢ o ≤
      (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})
        a ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
refine ⟨fun h ↦ h.trans_lt (typein_lt_type _ _), fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < type fun (x1 x2 : α) ↦ x1 < x2
mpr :
  (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) o h) ≤
    a
⊢ o ≤
    (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})
      a

Tactic:
rw [← typein_enum _ h, typein_le_typein, not_lt]

Premises used: Ordinal.typein_le_typein, Ordinal.typein_enum, not_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < type fun (x1 x2 : α) ↦ x1 < x2
⊢ (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) o h) ≤
    a

Tactic:
apply ha
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : OrderTop α
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
type_lt_mem_range_succ_iff.2 ⟨⊤, isMax_top⟩

Premises used: Iff.mpr, isMax_top, Ordinal.type_lt_mem_range_succ_iff, Exists.intro, Top.top
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
rw : (∃ (x : α), IsMax x) ↔ ¬∀ (x : α), ¬IsMax x
⊢ IsSuccPrelimit (type fun (x1 x2 : α) ↦ x1 < x2) ↔ NoMaxOrder α

Tactic:
rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff_mem_range_succ,
    type_lt_mem_range_succ_iff]

Premises used: not_iff_not, Ordinal.type_lt_mem_range_succ_iff, Order.not_isSuccPrelimit_iff_mem_range_succ, noMaxOrder_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ (∃ (x : α), IsMax x) ↔ ¬∀ (x : α), ¬IsMax x

Tactic:
simp [IsMax]

Premises used: IsMax
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
h : NoMaxOrder α
⊢ IsSuccPrelimit (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
isSuccPrelimit_type_lt_iff.2 h

Premises used: Iff.mpr, Ordinal.isSuccPrelimit_type_lt_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
x : ToType 1
rw :
  Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
              (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
            (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
              uniqueToTypeOne._proof_1) :
          ToType 1) :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
rw₁ rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
⊢ Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        x :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})

Tactic:
rw [one_toType_eq x, typein_enum]

Premises used: Ordinal.typein_enum, Ordinal.one_toType_eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
x y : o.ToType
⊢ LE.le (α := Ordinal.{u_1})
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
              (typein fun (x1 x2 : o.ToType) ↦ x1 < x2) :
            (a : o.ToType) → Ordinal.{u_1})
          x :
        Ordinal.{u_1})
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
              (typein fun (x1 x2 : o.ToType) ↦ x1 < x2) :
            (a : o.ToType) → Ordinal.{u_1})
          y :
        Ordinal.{u_1}) ↔
    x ≤ y

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
a : (succ o).ToType
rw :
  (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
          x1 < x2) (typein fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) :
        (a : (succ o).ToType) → Ordinal.{u_1})
      a <
    succ o
⊢ a ≤
    (enum fun (x1 x2 : (succ o).ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → (succ o).ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) o ⋯)

Tactic:
rw [← enum_typein (α := (succ o).ToType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk,
    ← lt_succ_iff]

Premises used: Ordinal.enum_le_enum', Ordinal.enum_typein, Order.lt_succ_iff, LT.lt, Subtype.mk_le_mk
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
          x1 < x2) (typein fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) :
        (a : (succ o).ToType) → Ordinal.{u_1})
      a <
    succ o

Tactic:
apply typein_lt_self

Premises used: Ordinal.typein_lt_self
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
⊢ Eq.{u + 2} (α := Ordinal.{u})
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) α)
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) β)

Tactic:
congr_arg sInf <| ext fun o ↦ ⟨?_, ?_⟩

Premises used: Set.ext, iInf, congr_arg, Iff.intro, InfSet.sInf
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
refine_1 :
  ∀ (o : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u})
        (range fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop)) o →
      Membership.mem (γ := Set Ordinal.{u})
        (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop)) o
refine_2 :
  ∀ (o : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u})
        (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop)) o →
      Membership.mem (γ := Set Ordinal.{u})
        (range fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop)) o
⊢ Eq.{u + 2} (α := Ordinal.{u})
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) α)
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) β)

Tactic:
refine congr_arg sInf <| ext fun o ↦ ⟨?_, ?_⟩

Premises used: Set.ext, congr_arg, Iff.intro, InfSet.sInf
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop))
    ((fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop))
      (Subtype.mk (p := fun (r : α → α → Prop) ↦ IsWellOrder α r) r hr))

Tactic:
⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩

Premises used: Set.Mem, setOf, RelIso.IsWellOrder.preimage, Subtype.mk, Exists.intro, Set.range, Ordinal.type_preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
refine_1 : β ≃ α
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop))
    ((fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop))
      (Subtype.mk (p := fun (r : α → α → Prop) ↦ IsWellOrder α r) r hr))

Tactic:
refine ⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop))
    ((fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop))
      (Subtype.mk (p := fun (r : β → β → Prop) ↦ IsWellOrder β r) r hr))

Tactic:
⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩

Premises used: Set.Mem, setOf, RelIso.IsWellOrder.preimage, Subtype.mk, Exists.intro, Set.range, Ordinal.type_preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
refine_2 : α ≃ β
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop))
    ((fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop))
      (Subtype.mk (p := fun (r : β → β → Prop) ↦ IsWellOrder β r) r hr))

Tactic:
refine ⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ β ≃ α

Tactic:
exacts [f.symm, f]

Premises used: Equiv.symm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
⊢ (#α).ord = ⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop)

Tactic:
(rfl)

Premises used: Cardinal.ord, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u_1
⊢ ∃ (r : α → α → Prop) (x : IsWellOrder α r), (#α).ord = type r

Tactic:
let ⟨r, wo⟩ := ciInf_mem fun r : { r // IsWellOrder α r } => @type α r.1 r.2
  ⟨r.1, r.2, wo.symm⟩

Premises used: Cardinal.mk, Exists, ciInf_mem, Ordinal.type, _private.0.Cardinal.exists_ord_eq.match_1, Cardinal.ord, Exists.intro, Eq.symm, Subtype.val, Eq, Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u_1
⊢ ∃ (x : LinearOrder α) (x_1 : WellFoundedLT α), (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
let ⟨r, _, hr⟩ := exists_ord_eq α
  let := linearOrderOfSTO r
  ⟨this, inferInstance, hr⟩

Premises used: _private.0.Cardinal.exists_ord_eq_type_lt.match_1, Cardinal.mk, Exists, Ordinal.type, inferInstance, Cardinal.ord, LT.lt, Exists.intro, Cardinal.exists_ord_eq, linearOrderOfSTO, Eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
h : IsWellOrder α r
⊢ (#α).ord ≤ type r

Tactic:
ciInf_le' _ (Subtype.mk r h)

Premises used: ciInf_le', Cardinal.ord, Subtype.mk
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
⊢ c.ord.card = c

Tactic:
c.inductionOn fun α ↦ let ⟨r, _, e⟩ := exists_ord_eq α; e ▸ card_type r

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ GaloisConnection ord card

Tactic:
fun c o ↦ c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_

Premises used: Cardinal.inductionOn, GaloisConnection
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
refine :
  ∀ (c : Cardinal.{u_1}) (o : Ordinal.{u_1}) (α β : Type u_1) (s : β → β → Prop) (x : IsWellOrder β s),
    (#α).ord ≤ type s ↔ #α ≤ (type s).card
⊢ GaloisConnection ord card

Tactic:
refine fun c o ↦ c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
let : ∀ (r : α → α → Prop) (w : IsWellOrder α r) (e : (#α).ord = type r), (#α).ord ≤ type s ↔ #α ≤ (type s).card
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
let ⟨r, _, e⟩ := exists_ord_eq α
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
mp : (#α).ord ≤ type s → #α ≤ (type s).card
mpr : #α ≤ (type s).card → (#α).ord ≤ type s
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
constructor