α : Type u_2
β : Type u_3
γ : Type u_1
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (PrincipalSeg.trans f g).top g.top
α : Type u_2
β : Type u_3
γ : Type u_1
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t h.top g.top
rw [Subsingleton.elim h (f.trans g)]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (PrincipalSeg.trans f g).top g.top
apply PrincipalSeg.lt_top