case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ inv (r • s) x z ↔ (inv s • inv r) x z
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
⊢ inv (r • s) = inv s • inv r
ext (x z)
no goals
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ inv (r • s) x z ↔ (inv s • inv r) x z
simp [comp, inv, flip, and_comm]