α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), ↑f (enum r (type r_1) hr) = enum s (type r_1) hs
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ : Type ?u.97551
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) (hs : o < type s), ↑f (enum r o hr) = enum s o hs
refine' inductionOn o _
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), ↑f (enum r (type r_1) hr) = enum s (type r_1) hs
rintro γ t wo ⟨g⟩ ⟨h⟩
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
skip
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f g.top = (PrincipalSeg.ltEquiv g f).top
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f (enum r (type t) (_ : Nonempty (t ≺i r))) = enum s (type t) (_ : Nonempty (t ≺i s))
rw [enum_type g, enum_type (PrincipalSeg.ltEquiv g f)]
no goals
case intro.intro
α✝ : Type ?u.97545
β✝ : Type ?u.97548
γ✝ : Type ?u.97551
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ ↑f g.top = (PrincipalSeg.ltEquiv g f).top
rfl