awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β_1 : Type v
γ : Type w
r_1 : α → α → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a : Ordinal.{u}
β : Type u
s : β → β → Prop
wo : IsWellOrder β s
g : s ≺i r
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range (ι := α)
      (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) ⋯) :
        (a : α) → Ordinal.{u}))
    (type s)

Tactic:
exact ⟨_, g.subrelIso.ordinal_type_eq⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a : α
⊢ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a) =
    ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a

Tactic:
rfl

Premises used: Ordinal.type, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ (typein r).top (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) = type r

Tactic:
rfl

Premises used: Ordinal.type, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a : α
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a < type r

Tactic:
(typein r).lt_top a

Premises used: PrincipalSeg.lt_top, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
i : o.ToType
simp_rw :
  (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})
      i <
    type fun (x1 x2 : o.ToType) ↦ x1 < x2
⊢ (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})
      i <
    o

Tactic:
simp_rw [← type_toType o]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
i : o.ToType
⊢ (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})
      i <
    type fun (x1 x2 : o.ToType) ↦ x1 < x2

Tactic:
apply typein_lt_type

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i s
⊢ ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : β) → Ordinal.{u_1})
      (f.top (r := r) (s := s)) =
    type r

Tactic:
f.subrelIso.ordinal_type_eq

Premises used: PrincipalSeg.subrelIso, Ordinal.type, RelIso.ordinal_type_eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a b : α
⊢ LT.lt (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
        Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
        Ordinal.{u}) ↔
    r a b

Tactic:
(typein r).map_rel_iff

Premises used: PrincipalSeg.toRelEmbedding, RelEmbedding.map_rel_iff, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a b : α
rw :
  ¬LT.lt (α := Ordinal.{u})
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
          Ordinal.{u})
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
          Ordinal.{u}) ↔
    ¬r b a
rw₁ rw₂ : ¬r b a ↔ ¬r b a
⊢ LE.le (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
        Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
        Ordinal.{u}) ↔
    ¬r b a

Tactic:
rw [← not_lt, typein_lt_typein]

Premises used: Ordinal.typein_lt_typein, not_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ Injective (α := α) (β := Ordinal.{u})
    (⇑((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})

Tactic:
(typein r).injective

Premises used: RelEmbedding.injective, PrincipalSeg.toRelEmbedding, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a b : α
⊢ Eq (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
        Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
        Ordinal.{u}) ↔
    a = b

Tactic:
(typein_injective r).eq_iff

Premises used: Function.Injective.eq_iff, Ordinal.typein_injective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o : Ordinal.{u}
⊢ Membership.mem (γ := Set Ordinal.{u})
      (range (ι := α)
        (⇑((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u}))
      o ↔
    o < type r

Tactic:
(typein r).mem_range_iff_rel

Premises used: PrincipalSeg.mem_range_iff_rel, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o : Ordinal.{u}
h : o < type r
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range (ι := α)
      (⇑((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u}))
    o

Tactic:
(typein r).mem_range_of_rel_top h

Premises used: PrincipalSeg.mem_range_of_rel_top, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ SurjOn (α := α)
    (⇑((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u}) univ
    (Iio (type r))

Tactic:
(typein r).surjOn

Premises used: setOf, PrincipalSeg.surjOn, Set.Iio, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
x : α
⊢ type (α := (↑(Iio x) : Type u)) LT.lt =
    (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (typein LT.lt) :
        (a : α) → Ordinal.{u})
      x

Tactic:
rfl

Premises used: Set.Mem, setOf, Ordinal.type, Subrel, Set.Iio, Order.Preimage, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o : Ordinal.{u}
h : o < type r
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) o h) :
        α) =
    o

Tactic:
(typein r).apply_subrelIso _

Premises used: PrincipalSeg.apply_subrelIso, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : s ≺i r
h : type s < type r
⊢ (enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r)) (type s) h) =
    f.top (r := s) (s := r)

Tactic:
(typein r).injective <| (typein_enum _ _).trans (typein_top _).symm

Premises used: Ordinal.typein_top, RelEmbedding.injective, PrincipalSeg.toRelEmbedding, Ordinal.typein_enum, Eq.symm, Eq.trans, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a : α
⊢ (enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a)
          ⋯ :
        { x : Ordinal.{u} // x ∈ Iio (type r) }) =
    a

Tactic:
enum_type (PrincipalSeg.ofElement r a)

Premises used: Ordinal.type, PrincipalSeg.ofElement, Ordinal.enum_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o₁ o₂ : (↑(Iio (type r)) : Type (u + 1))
⊢ r ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₁)
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₂) ↔
    o₁ < o₂

Tactic:
(enum _).map_rel_iff

Premises used: RelIso.map_rel_iff, Ordinal.enum
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o₁ o₂ : (↑(Iio (type r)) : Type (u + 1))
rw : ¬o₁ < o₂ ↔ o₂ ≤ o₁
rw₁ rw₂ : o₂ ≤ o₁ ↔ o₂ ≤ o₁
⊢ ¬r ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₁)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₂) ↔
    o₂ ≤ o₁

Tactic:
rw [enum_lt_enum (r := r), not_lt]

Premises used: Ordinal.enum_lt_enum, not_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u_1}
o₁ o₂ : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))
rw :
  LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    ¬LT.lt (α := a.ToType)
        ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
              (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
            o₂ :
          a.ToType)
        ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
              (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
            o₁ :
          a.ToType)
rw₁ rw₂ :
  LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType)
⊢ LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    o₁ ≤ o₂

Tactic:
rw [← enum_le_enum, not_lt]

Premises used: not_lt, Ordinal.enum_le_enum
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o₁ o₂ : (↑(Iio (type r)) : Type (u + 1))
⊢ Eq (α := α) ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₁ : α)
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₂ : α) ↔
    o₁ = o₂

Tactic:
EmbeddingLike.apply_eq_iff_eq _

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h0 : 0 < type r
a : α
rw :
  Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0 ≤
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a) ⋯
⊢ ¬r a
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0))

Tactic:
rw [← enum_typein r a, enum_le_enum r]

Premises used: Ordinal.enum_typein, Ordinal.enum_le_enum
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0 ≤
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a) ⋯

Tactic:
bot_le (α := Ordinal)

Premises used: bot_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0 ≤
    Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a) ⋯

Tactic:
exact bot_le (α := Ordinal)

Premises used: bot_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
rw :
  ¬a <
      (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 ⋯)
⊢ (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 ⋯) ≤
    a

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ ¬a <
      (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 ⋯)

Tactic:
apply enum_zero_le

Premises used: Ordinal.enum_zero_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (hr : o < type r) (hs : o < type s),
    Eq (α := β)
      ((f : (a : α) → β)
          ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) o hr) :
            α) :
        β)
      ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) o hs) :
        β)

Tactic:
inductionOn o ?_

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
refine :
  ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst_2 : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s),
    Eq (α := β)
      ((f : (a : α) → β)
          ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (type r_1) hr) :
            α) :
        β)
      ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) (type r_1) hs) :
        β)
⊢ ∀ (hr : o < type r) (hs : o < type s),
    Eq (α := β)
      ((f : (a : α) → β)
          ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) o hr) :
            α) :
        β)
      ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) o hs) :
        β)

Tactic:
refine inductionOn o ?_
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
rw : (f : (a : α) → β) (g.top (r := t) (s := r)) = (g.transRelIso (r := t) (s := r) (t := s) f).top (r := t) (s := s)
⊢ Eq (α := β)
    ((f : (a : α) → β)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (type t) ⋯) :
          α) :
      β)
    ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) (type t) ⋯) :
      β)

Tactic:
rw [enum_type g, enum_type (g.transRelIso f)]

Premises used: PrincipalSeg.transRelIso, Ordinal.enum_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ (f : (a : α) → β) (g.top (r := t) (s := r)) = (g.transRelIso (r := t) (s := r) (t := s) f).top (r := t) (s := s)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
hr : o < type r
⊢ Eq (α := β)
    ((f : (a : α) → β)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) o hr) :
          α) :
      β)
    ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) o ⋯) :
      β)

Tactic:
relIso_enum' _ _ _ _

Premises used: Ordinal.relIso_enum'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Iio o) : Type (u + 1))

Tactic:
⟨_, ⟨ToType.mk.toEquiv⟩⟩

Premises used: Small.mk, Nonempty.intro, Ordinal.ToType.mk, Exists.intro, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
rw : Small.{u, u + 1} (↑(Iio o ∪ {o}) : Type (u + 1))
⊢ Small.{u, u + 1} (↑(Iic o) : Type (u + 1))

Tactic:
rw [← Iio_union_right]

Premises used: Set.Iio_union_right
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Iio o ∪ {o}) : Type (u + 1))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Ico a b) : Type (u + 1))

Tactic:
small_subset Ico_subset_Iio_self

Premises used: Set.Ico_subset_Iio_self, small_subset
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Icc a b) : Type (u + 1))

Tactic:
small_subset Icc_subset_Iic_self

Premises used: Set.Icc_subset_Iic_self, small_subset
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Ioo a b) : Type (u + 1))

Tactic:
small_subset Ioo_subset_Iio_self

Premises used: Set.Ioo_subset_Iio_self, small_subset
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Ioc a b) : Type (u + 1))

Tactic:
small_subset Ioc_subset_Iic_self

Premises used: Set.Ioc_subset_Iic_self, small_subset
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_1}
ho : 0 < o
rwa rwa₁ rwa₂ rwa₃ : 0 ∈ Iio o
⊢ 0 ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)

Tactic:
rwa [type_toType]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
⊢ False

Tactic:
simp at ho
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
ho : 0 < o
⊢ Eq (α := o.ToType)
    ((enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 ⋯) :
      o.ToType)
    (have H := toTypeOrderBot ⋯;
    (⊥ : o.ToType))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ WellFounded fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2

Tactic:
wellFounded_iff_wellFounded_subrel.mpr (·.induction_on fun ⟨_, _, wo⟩ ↦
    RelHomClass.wellFounded (enum _) wo.wf)

Premises used: Iff.mpr, Quot.induction_on, wellFounded_iff_wellFounded_subrel
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ WellFoundedLT Ordinal.{u_1}

Tactic:
⟨lt_wf⟩

Premises used: IsWellFounded.mk, Ordinal.lt_wf
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
p : Ordinal.{u} → Prop
i : Ordinal.{u}
h : ∀ (j : Ordinal.{u}), (∀ k < j, p k) → p j
⊢ p i

Tactic:
WellFoundedLT.induction i h

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≼i s
a : α
rw :
  Eq (α := Ordinal.{u_1})
    (((f.transPrincipal (r := r) (s := s) (t := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) (typein s)).toRelEmbedding (r :=
            r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
          (a : α) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
rw₁ :
  Eq (α := Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
g : r ≺i fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2
rw₂ :
  Eq (α := Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
g₁ : r ≺i fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2
⊢ Eq (α := Ordinal.{u_1})
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : β) → Ordinal.{u_1})
        ((f : (a : α) → β) a : β) :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})

Tactic:
rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]

Premises used: InitialSeg.transPrincipal, InitialSeg.transPrincipal_apply, PrincipalSeg.eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ (type r).card = #α

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.mk', rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
x : α
⊢ card (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x) =
    #{ y : α // r y x }

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.mk', rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ o₁ ≤ o₂ → o₁.card ≤ o₂.card

Tactic:
inductionOn o₁ fun _ _ _ => inductionOn o₂ fun _ _ _ ⟨⟨⟨f, _⟩, _⟩⟩ => ⟨f⟩

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ card 0 = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero, Quotient.map, Ordinal.card, Quot.map
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ card 1 = 1

Tactic:
mk_eq_one _

Premises used: Quotient.map, Ordinal.card, Quot.map, Cardinal.mk_eq_one