case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
a✝¹ : α
c✝ : γ
a✝ : r₁ a✝¹ c✝
⊢ LiftRel r₂ s₂ (inl a✝¹) (inl c✝)

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