α✝ : Type ?u.108718
β✝ : Type ?u.108721
γ : Type ?u.108724
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
α✝ : Type ?u.108718
β✝ : Type ?u.108721
γ : Type ?u.108724
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
haveI := @RelEmbedding.isWellOrder _ _ (@Equiv.ulift.{max v w} α ⁻¹'o r) r
  (RelIso.preimage Equiv.ulift.{max v w} r) _
α✝ : Type ?u.108718
β✝ : Type ?u.108721
γ : Type ?u.108724
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this✝ : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
this : IsWellOrder (ULift β) (↑Equiv.ulift ⁻¹'o s)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
α✝ : Type ?u.108718
β✝ : Type ?u.108721
γ : Type ?u.108724
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
haveI := @RelEmbedding.isWellOrder _ _ (@Equiv.ulift.{max u w} β ⁻¹'o s) s
  (RelIso.preimage Equiv.ulift.{max u w} s) _
no goals
α✝ : Type ?u.108718
β✝ : Type ?u.108721
γ : Type ?u.108724
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
this✝ : IsWellOrder (ULift α) (↑Equiv.ulift ⁻¹'o r)
this : IsWellOrder (ULift β) (↑Equiv.ulift ⁻¹'o s)
⊢ lift (type r) < lift (type s) ↔ Nonempty (r ≺i s)
exact ⟨fun ⟨f⟩ =>
  ⟨(f.equivLT (RelIso.preimage Equiv.ulift r).symm).ltLe
      (InitialSeg.ofIso (RelIso.preimage Equiv.ulift s))⟩,
  fun ⟨f⟩ =>
  ⟨(f.equivLT (RelIso.preimage Equiv.ulift r)).ltLe
      (InitialSeg.ofIso (RelIso.preimage Equiv.ulift s).symm)⟩⟩