case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a₁✝ a₂✝ : α
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)

case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
b₁✝ b₂✝ : β
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)

case sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a✝ : α
b✝ : β
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
h : Lex r₁ s₁ x y
⊢ Lex r₂ s₂ x y
cases h
no goals
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a₁✝ a₂✝ : α
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)
exact Lex.inl (hr _ _ ‹_›)
no goals
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
b₁✝ b₂✝ : β
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)
exact Lex.inr (hs _ _ ‹_›)
no goals
case sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.31025
δ : Type ?u.31028
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a✝ : α
b✝ : β
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)
exact Lex.sep _ _