α : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ ∀ (a : WellOrder),
    type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent a}) = lift (Quotient.mk isEquivalent a)
α : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ type (Subrel (fun x x_1 => x < x_1) {o' | o' < o}) = lift o
refine' Quotient.inductionOn o _
case mk
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }}) =
    lift (Quotient.mk isEquivalent { α := α, r := r, wo := wo })
α : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ ∀ (a : WellOrder),
    type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent a}) = lift (Quotient.mk isEquivalent a)
rintro ⟨α, r, wo⟩
case mk
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }}) =
    lift (Quotient.mk isEquivalent { α := α, r := r, wo := wo })
case mk
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }}) =
    lift (Quotient.mk isEquivalent { α := α, r := r, wo := wo })
skip
case mk.a
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ { α := ↑{o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }},
      r := Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }},
      wo :=
        (_ :
          IsWellOrder (↑{o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }})
            (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }})) } ≈
    { α := ULift { α := α, r := r, wo := wo }.α, r := ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r,
      wo := (_ : IsWellOrder (ULift { α := α, r := r, wo := wo }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r)) }
case mk
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ type (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }}) =
    lift (Quotient.mk isEquivalent { α := α, r := r, wo := wo })
apply Quotient.sound
case mk.a.val
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }} ≃r
    ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r
case mk.a
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ { α := ↑{o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }},
      r := Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }},
      wo :=
        (_ :
          IsWellOrder (↑{o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }})
            (Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }})) } ≈
    { α := ULift { α := α, r := r, wo := wo }.α, r := ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r,
      wo := (_ : IsWellOrder (ULift { α := α, r := r, wo := wo }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r)) }
constructor
no goals
case mk.a.val
α✝ : Type ?u.105581
β : Type ?u.105584
γ : Type ?u.105587
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ Subrel (fun x x_1 => x < x_1) {o' | o' < Quotient.mk isEquivalent { α := α, r := r, wo := wo }} ≃r
    ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r
refine' ((RelIso.preimage Equiv.ulift r).trans (enumIso r).symm).symm