case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.30404
δ : Type ?u.30407
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)

case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.30404
δ : Type ?u.30407
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.30404
δ : Type ?u.30407
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
x y a b : α ⊕ β
h : LiftRel r s a b
⊢ Lex r s a b
cases h
no goals
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.30404
δ : Type ?u.30407
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)
exact Lex.inl ‹_›
no goals
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.30404
δ : Type ?u.30407
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)
exact Lex.inr ‹_›