α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s (swap (swap x)) (swap (swap y))
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s x y
rw [← swap_swap x, ← swap_swap y]
no goals
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s (swap (swap x)) (swap (swap y))
exact h.swap