α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ ↑(match ltOrEq f with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ ↑(leLT f g).toRelEmbedding a = ↑g.toRelEmbedding (↑f a)
delta InitialSeg.leLT
case inl
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
h : ltOrEq f = Sum.inl f'
⊢ ↑(match Sum.inl f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)

case inr
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
h : ltOrEq f = Sum.inr f'
⊢ ↑(match Sum.inr f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ ↑(match ltOrEq f with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
cases' h : f.ltOrEq with f' f'
no goals
case inl
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
h : ltOrEq f = Sum.inl f'
⊢ ↑(match Sum.inl f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
simp only [PrincipalSeg.trans_apply, f.ltOrEq_apply_left]
no goals
case inr
α : Type u_3
β : Type u_1
γ : Type u_2
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
h : ltOrEq f = Sum.inr f'
⊢ ↑(match Sum.inr f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
simp only [PrincipalSeg.equivLT_apply, f.ltOrEq_apply_right]