α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f⁻¹ x = x ∨ ↑g x = x
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
⊢ Disjoint f⁻¹ g
intro x
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f x = x ∨ ↑g x = x
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f⁻¹ x = x ∨ ↑g x = x
rw [inv_eq_iff_eq, eq_comm]
no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f x = x ∨ ↑g x = x
exact h x