α : Type u_1
f g h✝ : Perm α
h : Disjoint f⁻¹ g
⊢ Disjoint f g
α : Type u_1
f g h : Perm α
⊢ Disjoint f⁻¹ g ↔ Disjoint f g
refine' ⟨fun h => _, Disjoint.inv_left⟩
no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f⁻¹ g
⊢ Disjoint f g
convert h.inv_left