awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
rw rw₁ : o.card = o.card
⊢ (type fun (x1 x2 : o.ToType) ↦ x1 < x2).card = o.card

Tactic:
rw [Ordinal.type_toType]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hs : sᶜ.Nonempty
⊢ card
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        (WellFounded.min (r := r) ⋯ sᶜ hs)) ≤
    #(↑s : Type u)

Tactic:
IsWellFounded.wf.cardinalMk_subtype_lt_min_compl_le hs

Premises used: WellFounded.cardinalMk_subtype_lt_min_compl_le, IsWellFounded.wf
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ type (ULift.down ⁻¹'o r) = lift.{v, u} (type r)

Tactic:
rfl

Premises used: Ordinal.lift, Order.Preimage, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ (type fun (x1 x2 : ULift.{v, u} α) ↦ x1 < x2) = lift.{v, u} (type fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
rfl

Premises used: Ordinal.lift, Order.Preimage, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
⊢ lift.{v, u} (type r) = lift.{u, v} (type s)

Tactic:
((RelIso.preimage Equiv.ulift r).trans <|
      f.trans (RelIso.preimage Equiv.ulift s).symm).ordinal_type_eq

Premises used: Ordinal.lift, Equiv.ulift, RelIso.symm, RelIso.ordinal_type_eq, RelIso.trans, Order.Preimage, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : β ≃ α
⊢ type (α := β) ((⇑f : (a : β) → α) ⁻¹'o r) = type r

Tactic:
(RelIso.preimage f r).ordinal_type_eq

Premises used: RelIso.ordinal_type_eq, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
inst : IsWellOrder α r
f : β ≃ α
⊢ lift.{u, v} (type (α := β) ((⇑f : (a : β) → α) ⁻¹'o r)) = lift.{v, u} (type r)

Tactic:
(RelIso.preimage f r).ordinal_lift_type_eq

Premises used: RelIso.ordinal_lift_type_eq, Order.Preimage, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ lift.{max u v, u} = lift.{v, u}

Tactic:
funext fun a =>
    inductionOn a fun _ r _ =>
      Quotient.sound ⟨(RelIso.preimage Equiv.ulift r).trans (RelIso.preimage Equiv.ulift r).symm⟩

Premises used: funext, Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{max u_1 u_2}
⊢ lift.{u_1, max u_1 u_2} a = a

Tactic:
inductionOn a fun _ r _ => Quotient.sound ⟨RelIso.preimage Equiv.ulift r⟩

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ∀ (a : Ordinal.{u}), lift.{u, u} a = a

Tactic:
lift_id'.{u, u}

Premises used: Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u}
⊢ lift.{0, u} a = a

Tactic:
lift_id' a

Premises used: Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)
mpr : Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (r ≼i s)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: Nonempty.intro, _private.0.Ordinal.lift_type_le.match_1, InitialSeg, Nonempty
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp :
  lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) →
    (f :
        InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
          ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
          (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
      r ≼i s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: Ordinal.lift, Ordinal.type, LE.le, Nonempty.intro, _private.0.Ordinal.lift_type_le.match_2
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mpr :
  Nonempty (r ≼i s) →
    (f : r ≼i s) →
      InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f :
  InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ r ≼i s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).toInitialSeg)

Premises used: Equiv.ulift, RelIso.symm, InitialSeg.trans, RelIso.toInitialSeg, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : Nonempty (r ≼i s)
f : r ≼i s
⊢ InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)

Tactic:
exact (RelIso.preimage Equiv.ulift r).toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).symm.toInitialSeg)

Premises used: Equiv.ulift, RelIso.symm, InitialSeg.trans, RelIso.toInitialSeg, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
Quotient.eq'.trans ⟨?_, ?_⟩

Premises used: Ordinal.lift, Ordinal.type, Quotient.eq', Iff.intro, Iff.trans, Ordinal
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
refine_1 :
  (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    Nonempty (r ≃r s)
refine_2 :
  Nonempty (r ≃r s) →
    (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ }
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
refine Quotient.eq'.trans ⟨?_, ?_⟩

Premises used: Quotient.eq', Iff.intro, Iff.trans
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: Nonempty.intro, RelIso, Nonempty, _private.0.Ordinal.lift_type_eq.match_1
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
refine_1 :
  (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    (f :
        RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
          ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
          (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
      r ≃r s
⊢ (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ }

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: WellOrder.r, WellOrder.α, ULift, _private.0.Ordinal.lift_type_eq.match_2, Ordinal.lift._proof_1, Nonempty.intro, WellOrder.mk, ULift.down, Order.Preimage, Setoid.r
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
refine_2 :
  Nonempty (r ≃r s) →
    (f : r ≃r s) →
      RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ Nonempty (r ≃r s) →
    (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ }

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h :
  (isEquivalent : WellOrder → WellOrder → Prop)
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
      r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ }
f :
  RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ r ≃r s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)

Premises used: Equiv.ulift, RelIso.symm, RelIso.trans, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : Nonempty (r ≃r s)
f : r ≃r s
⊢ RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)

Tactic:
exact (RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm

Premises used: Equiv.ulift, RelIso.symm, RelIso.trans, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp : lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)
mpr : Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: _private.0.Ordinal.lift_type_lt.match_1, PrincipalSeg, Nonempty.intro, Nonempty
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp :
  lift.{max v w, u} (type r) < lift.{max u w, v} (type s) →
    (f :
        PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
          ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
          (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
      r ≺i s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)

Tactic:
fun ⟨f⟩ ↦ ⟨?_⟩

Premises used: Ordinal.lift, Ordinal.type, _private.0.Ordinal.lift_type_lt.match_2, Nonempty.intro, LT.lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mpr :
  Nonempty (r ≺i s) →
    (f : r ≺i s) →
      PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
f :
  PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
⊢ r ≺i s

Tactic:
exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r).symm).transInitial
      (RelIso.preimage Equiv.ulift s).toInitialSeg

Premises used: PrincipalSeg.transInitial, PrincipalSeg.relIsoTrans, Equiv.ulift, RelIso.symm, RelIso.toInitialSeg, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
h : Nonempty (r ≺i s)
f : r ≺i s
⊢ PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
    ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
    (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)

Tactic:
exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
      (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

Premises used: PrincipalSeg.transInitial, PrincipalSeg.relIsoTrans, Equiv.ulift, RelIso.symm, RelIso.toInitialSeg, RelIso.preimage
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type v
s : β → β → Prop
h_1 : IsWellOrder β s
rw : lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
rw [← lift_umax]

Premises used: Ordinal.lift_umax
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type v
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s

Tactic:
lift_type_le.{_, _, u}

Premises used: Ordinal.lift_type_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type v
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s

Tactic:
exact lift_type_le.{_, _, u}
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{v}
simp_rw : lift.{u, v} a ≤ lift.{u, v} b ∧ lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ b ≤ a
⊢ lift.{u, v} a = lift.{u, v} b ↔ a = b

Tactic:
simp_rw [le_antisymm_iff, lift_le]

Premises used: le_antisymm_iff, Ordinal.lift_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{v}
simp_rw : lift.{u, v} a ≤ lift.{u, v} b ∧ ¬lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ ¬b ≤ a
⊢ lift.{u, v} a < lift.{u, v} b ↔ a < b

Tactic:
simp_rw [lt_iff_le_not_ge, lift_le]

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

Tactic:
f.subrelIso.ordinal_lift_type_eq

Premises used: PrincipalSeg.subrelIso, Ordinal.type, RelIso.ordinal_lift_type_eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
nth_rw :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} o

Tactic:
nth_rw 2 [← o.type_toType]

Premises used: Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
rw :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u, u + 1} (type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2)
rw₁ :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2
rw₂ rw₃ :
  Eq (α := Ordinal.{u + 1})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o :
      Ordinal.{u + 1})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o :
      Ordinal.{u + 1})
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)

Tactic:
rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]

Premises used: RelIso.ordinal_lift_type_eq, OrderIso.toRelIsoLT, Ordinal.ToType.mk, Ordinal.type_Iio_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
⊢ (type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2) = lift.{u + 1, u} o

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (a b : Ordinal.{v}), a < b → lift.{u, v} a < lift.{u, v} b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
refine :
  ∀ (a : Ordinal.{v}) (b : Ordinal.{max u v}) (α : Type v) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type (max u v))
    (s : β → β → Prop) (x_1 : IsWellOrder β s)
    (h :
      type s <
        (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
              x1 < x2) lift.{u, v} liftInitialSeg._proof_1 :
            (a : Ordinal.{v}) → Ordinal.{max u v})
          (type r)),
    Membership.mem (γ := Set Ordinal.{max u v})
      (range (ι := Ordinal.{v})
        (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
              x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
          (a : Ordinal.{v}) → Ordinal.{max u v}))
      (type s)
⊢ (fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) ≼i fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2

Tactic:
refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp),
    fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
h :
  type s <
    (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (type r)
⊢ Nonempty (s ≺i r)

Tactic:
rw [RelEmbedding.ofMonotone_coe, ← lift_id'.{max u v} (type s),
    ← lift_umax.{v, u}, lift_type_lt] at h

Premises used: Ordinal.lift_type_lt, RelEmbedding.ofMonotone_coe
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
h : Nonempty (s ≺i r)
obtain :
  ∀ (f : s ≺i r),
    Membership.mem (γ := Set Ordinal.{max u v})
      (range (ι := Ordinal.{v})
        (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
              x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
          (a : Ordinal.{v}) → Ordinal.{max u v}))
      (type s)
⊢ Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)

Tactic:
obtain ⟨f⟩ := h