α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint (g * h) f
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint f (g * h)
rw [disjoint_comm]
no goals
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint (g * h) f
exact H1.symm.mul_left H2.symm