case h.e'_4
α✝ : Type ?u.98043
β✝ : Type ?u.98046
γ : Type ?u.98049
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
hr : o < type r
⊢ type s = type r
α✝ : Type ?u.98043
β✝ : Type ?u.98046
γ : Type ?u.98049
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
hr : o < type r
⊢ o < type s
convert hr using 1
case h.e'_4.a
α✝ : Type ?u.98043
β✝ : Type ?u.98046
γ : Type ?u.98049
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
hr : o < type r
⊢ { α := β, r := s, wo := inst✝ } ≈ { α := α, r := r, wo := inst✝¹ }
case h.e'_4
α✝ : Type ?u.98043
β✝ : Type ?u.98046
γ : Type ?u.98049
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
hr : o < type r
⊢ type s = type r
apply Quotient.sound
no goals
case h.e'_4.a
α✝ : Type ?u.98043
β✝ : Type ?u.98046
γ : Type ?u.98049
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
hr : o < type r
⊢ { α := β, r := s, wo := inst✝ } ≈ { α := α, r := r, wo := inst✝¹ }
exact ⟨f.symm⟩