awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type r = type s ↔ Nonempty.{u_1 + 1} (r ≃r s)

Tactic:
Quotient.eq'

Premises used: Ordinal.type, Quotient.eq', Ordinal
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : r ≃r s
⊢ type r = type s

Tactic:
type_eq.2 ⟨h⟩

Premises used: Iff.mpr, Ordinal.type_eq, Nonempty.intro
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : IsEmpty α
⊢ type r = 0

Tactic:
(RelIso.relIsoOfIsEmpty r _).ordinal_type_eq

Premises used: RelIso.relIsoOfIsEmpty, RelIso.ordinal_type_eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α

Tactic:
⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩

Premises used: Ordinal.type_eq_zero_of_empty, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
refine : ∀ (h : type r = 0), IsEmpty α
⊢ type r = 0 ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h : type r = 0
let : ∀ (s : RelIso (β := PEmpty.{u + 1}) r emptyRelation), IsEmpty α
⊢ IsEmpty α

Tactic:
let ⟨s⟩ := type_eq.1 h
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h : type r = 0
s : RelIso (β := PEmpty.{u + 1}) r emptyRelation
⊢ IsEmpty α

Tactic:
s.toEquiv.isEmpty

Premises used: Equiv.isEmpty, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h : type r = 0
s : RelIso (β := PEmpty.{u + 1}) r emptyRelation
⊢ IsEmpty α

Tactic:
exact s.toEquiv.isEmpty

Premises used: Equiv.isEmpty, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ type r ≠ 0 ↔ Nonempty α

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h : Nonempty α
⊢ type r ≠ 0

Tactic:
type_ne_zero_iff_nonempty.2 h

Premises used: Iff.mpr, Ordinal.type_ne_zero_iff_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ type (α := PEmpty.{u_1 + 1}) emptyRelation = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ type (α := Empty) emptyRelation = 0

Tactic:
type_eq_zero_of_empty _

Premises used: Ordinal.type_eq_zero_of_empty
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Nonempty α
inst_2 : Subsingleton α
intro : ∀ (val : Unique α), type r = 1
⊢ type r = 1

Tactic:
cases nonempty_unique α

Premises used: nonempty_unique
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Nonempty α
inst_2 : Subsingleton α
val : Unique α
⊢ type r = 1

Tactic:
(RelIso.ofUniqueOfIrrefl r _).ordinal_type_eq

Premises used: RelIso.ordinal_type_eq, RelIso.ofUniqueOfIrrefl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Nonempty α
inst_2 : Subsingleton α
val : Unique α
⊢ type r = 1

Tactic:
exact (RelIso.ofUniqueOfIrrefl r _).ordinal_type_eq

Premises used: RelIso.ordinal_type_eq, RelIso.ofUniqueOfIrrefl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ type r = 1 ↔ Nonempty.{max 1 (u + 1)} (Unique α)

Tactic:
⟨fun h ↦ let ⟨s⟩ := type_eq.1 h; ⟨s.toEquiv.unique⟩,
    fun ⟨_⟩ ↦ type_eq_one_of_unique r⟩

Premises used: Ordinal.type_eq, Equiv.unique, Unique, Ordinal.type, _private.0.Ordinal.type_eq_one_iff_unique.match_2, Nonempty.intro, Iff.intro, Iff.mp, Ordinal.type_eq_one_of_unique, Nonempty, RelIso.toEquiv, _private.0.Ordinal.type_eq_one_iff_unique.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ type (α := PUnit.{u_1 + 1}) emptyRelation = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ type (α := Unit) emptyRelation = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) = 0 ↔ o = 0
rw₁ rw₂ : o = 0 ↔ o = 0
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0

Tactic:
rw [← @type_eq_zero_iff_isEmpty o.ToType (· < ·), type_toType]

Premises used: Ordinal.type_eq_zero_iff_isEmpty, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ IsEmpty.{u_1 + 1} (ToType 0)

Tactic:
isEmpty_toType_iff.2 rfl

Premises used: Iff.mpr, Ordinal.isEmpty_toType_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) ≠ 0 ↔ o ≠ 0
rw₁ rw₂ : o ≠ 0 ↔ o ≠ 0
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0

Tactic:
rw [← @type_ne_zero_iff_nonempty o.ToType (· < ·), type_toType]

Premises used: Ordinal.type_ne_zero_iff_nonempty, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ NeZero.{u_1 + 1} (R := Ordinal.{u_1}) 1

Tactic:
⟨type_ne_zero_of_nonempty _⟩

Premises used: NeZero.mk, Ordinal.type_ne_zero_of_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Ne.{u_1 + 2} (α := Ordinal.{u_1}) 1 0

Tactic:
_root_.one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Nontrivial Ordinal.{u}

Tactic:
⟨⟨1, 0, one_ne_zero⟩⟩

Premises used: Nontrivial.mk, Exists.intro, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
motive : Ordinal.{u_1} → Prop
o : Ordinal.{u_1}
type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r], motive (Ordinal.type r)
⊢ motive o

Tactic:
Quot.inductionOn o fun ⟨α, r, _⟩ ↦ type α r

Premises used: Quot.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
motive : Ordinal.{u_1} → Ordinal.{u_2} → Prop
o₁ : Ordinal.{u_1}
o₂ : Ordinal.{u_2}
type :
  ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop)
    [inst_1 : IsWellOrder β s], motive (Ordinal.type r) (Ordinal.type s)
⊢ motive o₁ o₂

Tactic:
Quotient.inductionOn₂ o₁ o₂ fun ⟨α, r, _⟩ ⟨β, s, _⟩ ↦ type α r β s

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
motive : Ordinal.{u_1} → Ordinal.{u_2} → Ordinal.{u_3} → Prop
o₁ : Ordinal.{u_1}
o₂ : Ordinal.{u_2}
o₃ : Ordinal.{u_3}
type :
  ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop)
    [inst_1 : IsWellOrder β s] (γ : Type u_3) (t : γ → γ → Prop) [inst_2 : IsWellOrder γ t],
    motive (Ordinal.type r) (Ordinal.type s) (Ordinal.type t)
⊢ motive o₁ o₂ o₃

Tactic:
Quotient.inductionOn₃ o₁ o₂ o₃ fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ↦ type α r β s γ t

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
motive : Ordinal.{u_1} → Prop
o : Ordinal.{u_1}
type :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], motive (Ordinal.type fun (x1 x2 : α) ↦ x1 < x2)
⊢ motive o

Tactic:
inductionOn o fun α r wo ↦ @type α (linearOrderOfSTO r) wo.toIsWellFounded

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
change :
  ⟦{ α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }⟧.liftOn' (fun (w : WellOrder.{u_1}) ↦ f w.α)
      ⋯ =
    f γ
⊢ (type fun (x1 x2 : γ) ↦ x1 < x2).liftOnWellOrder f c = f γ

Tactic:
change Quotient.liftOn' ⟦_⟧ _ _ = _

Premises used: Quotient.liftOn', Quotient.mk
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
rw : f { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }.α = f γ
⊢ ⟦{ α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }⟧.liftOn' (fun (w : WellOrder.{u_1}) ↦ f w.α)
      ⋯ =
    f γ

Tactic:
rw [Quotient.liftOn'_mk]

Premises used: Quotient.liftOn'_mk
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
h : linearOrderOfSTO { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ }.r = inst
⊢ f { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }.α = f γ

Tactic:
congr
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
⊢ linearOrderOfSTO { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ }.r = inst

Tactic:
LinearOrder.ext_lt fun _ _ ↦ Iff.rfl

Premises used: Iff.rfl, LinearOrder.ext_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
⊢ linearOrderOfSTO { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ }.r = inst

Tactic:
exact LinearOrder.ext_lt fun _ _ ↦ Iff.rfl

Premises used: Iff.rfl, LinearOrder.ext_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : r ≼i s
⊢ type r ≤ type s

Tactic:
⟨h⟩

Premises used: Nonempty.intro
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : r ↪r s
⊢ type r ≤ type s

Tactic:
⟨h.collapse⟩

Premises used: Nonempty.intro, RelEmbedding.collapse
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : r ≺i s
⊢ type r < type s

Tactic:
⟨h⟩

Premises used: Nonempty.intro
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o ≤ 0 ↔ o = 0

Tactic:
le_bot_iff

Premises used: le_bot_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ ¬o < 0

Tactic:
not_lt_bot

Premises used: not_lt_bot
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ∀ (a : Ordinal.{u_1}), a = 0 ∨ 0 < a

Tactic:
eq_bot_or_bot_lt

Premises used: eq_bot_or_bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type r ≤ type s ↔ Nonempty.{u_1 + 1} (r ≼i s)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type r ≤ type s ↔ Nonempty.{u_1 + 1} (r ↪r s)

Tactic:
⟨fun ⟨f⟩ => ⟨f⟩, fun ⟨f⟩ => ⟨f.collapse⟩⟩

Premises used: Ordinal.type, LE.le, Nonempty.intro, RelEmbedding, InitialSeg.toRelEmbedding, RelEmbedding.collapse, Iff.intro, Nonempty, _private.0.Ordinal.type_le_iff'.match_1, _private.0.Ordinal.type_le_iff'.match_2
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type r < type s ↔ Nonempty.{u_1 + 1} (r ≺i s)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
rw : Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
⊢ (type fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ≤ type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
rw [type_le_iff']

Premises used: Ordinal.type_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
⟨⟨Embedding.subtype _, ?_⟩⟩

Premises used: RelEmbedding.mk, Nonempty.intro, Function.Embedding.subtype
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
refine :
  ∀ {a b : (↑s : Type u)},
    LT.lt (α := α) ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) a : α)
        ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) b : α) ↔
      a < b
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
refine ⟨⟨Embedding.subtype _, ?_⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
⊢ ∀ {a b : (↑s : Type u)},
    LT.lt (α := α) ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) a : α)
        ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) b : α) ↔
      a < b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
rw : Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2)
⊢ (type fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2

Tactic:
rw [type_le_iff']

Premises used: Ordinal.type_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2)

Tactic:
⟨⟨embeddingOfSubset _ _ h, ?_⟩⟩

Premises used: RelEmbedding.mk, Nonempty.intro, Set.embeddingOfSubset
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
refine :
  ∀ {a b : (↑s : Type u)},
    LT.lt (α := (↑t : Type u)) ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) a : (↑t : Type u))
        ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) b : (↑t : Type u)) ↔
      a < b
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2)

Tactic:
refine ⟨⟨embeddingOfSubset _ _ h, ?_⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ ∀ {a b : (↑s : Type u)},
    LT.lt (α := (↑t : Type u)) ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) a : (↑t : Type u))
        ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) b : (↑t : Type u)) ↔
      a < b

Tactic:
aesop
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
α β : Ordinal.{u_1}
h : α ≤ β
apply : (type fun (x1 x2 : α.ToType) ↦ x1 < x2) ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2
⊢ (fun (x1 x2 : α.ToType) ↦ x1 < x2) ≼i fun (x1 x2 : β.ToType) ↦ x1 < x2

Tactic:
apply Classical.choice (type_le_iff.mp _)

Premises used: Ordinal.type_le_iff, Classical.choice, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
α β : Ordinal.{u_1}
h : α ≤ β
rwa : α ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2
rwa₁ rwa₂ rwa₃ rwa₄ : α ≤ β
⊢ (type fun (x1 x2 : α.ToType) ↦ x1 < x2) ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2

Tactic:
rwa [type_toType, type_toType]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
α β : Ordinal.{u_1}
h : α < β
apply : (type fun (x1 x2 : α.ToType) ↦ x1 < x2) < type fun (x1 x2 : β.ToType) ↦ x1 < x2
⊢ (fun (x1 x2 : α.ToType) ↦ x1 < x2) ≺i fun (x1 x2 : β.ToType) ↦ x1 < x2

Tactic:
apply Classical.choice (type_lt_iff.mp _)

Premises used: Ordinal.type_lt_iff, Classical.choice, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
α β : Ordinal.{u_1}
h : α < β
rwa : α < type fun (x1 x2 : β.ToType) ↦ x1 < x2
rwa₁ rwa₂ rwa₃ rwa₄ : α < β
⊢ (type fun (x1 x2 : α.ToType) ↦ x1 < x2) < type fun (x1 x2 : β.ToType) ↦ x1 < x2

Tactic:
rwa [type_toType, type_toType]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
refine_1 :
  ∀ (a b : α) (ha : r a b) (a_1 : { x : α // r x a }),
    Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
      (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
            (a : { x : α // r x a }) → α)
          a_1 :
        α)
refine_2 :
  ∀ (a b : α) (ha : r a b),
    Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
      ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))
refine_3 :
  ∀ (a : Ordinal.{u}),
    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}))
        a →
      a < type r
refine_4 :
  ∀ a < type 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}))
      a
⊢ r ≺i fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2

Tactic:
refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
ha : r a b
c : α
hc : r c a
⊢ Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
    (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
          (a : { x : α // r x a }) → α)
        (Subtype.mk (p := fun (x : α) ↦ r x a) c hc) :
      α)

Tactic:
trans hc ha

Premises used: trans, Set.Mem
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
ha : r a b
c : α
hc : r c a
⊢ Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
    (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
          (a : { x : α // r x a }) → α)
        (Subtype.mk (p := fun (x : α) ↦ r x a) c hc) :
      α)

Tactic:
exact trans hc ha
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
ha : r a b
⊢ Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
    ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))

Tactic:
ha

Premises used: Set.Mem
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
ha : r a b
⊢ Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
    ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))

Tactic:
exact ha
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
b : α
⊢ (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})
      b <
    type r

Tactic:
(PrincipalSeg.ofElement _ _).ordinal_type_lt

Premises used: PrincipalSeg.ordinal_type_lt, PrincipalSeg.ofElement
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
b : α
⊢ (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})
      b <
    type r

Tactic:
exact (PrincipalSeg.ofElement _ _).ordinal_type_lt

Premises used: PrincipalSeg.ordinal_type_lt, PrincipalSeg.ofElement
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type 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}))
      a

Tactic:
inductionOn a ?_

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a : Ordinal.{u}
refine_4 :
  ∀ (α_1 : Type u) (r_2 : α_1 → α_1 → Prop) [inst_1 : IsWellOrder α_1 r_2],
    type r_2 < type 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 r_2)
⊢ a < type 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}))
      a

Tactic:
refine inductionOn a ?_
-- 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:
⟨_, g.subrelIso.ordinal_type_eq⟩

Premises used: PrincipalSeg.subrelIso, Set.Mem, setOf, Exists.intro, RelIso.ordinal_type_eq, Set.range