α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ a ∈ support f ∪ support g → a ∈ support (f * g)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ support (f * g) = support f ∪ support g
refine' le_antisymm (support_mul_le _ _) fun a => _
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ ↑f (↑g a) = a → ↑f a = a ∧ ↑g a = a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ a ∈ support f ∪ support g → a ∈ support (f * g)
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ ↑f (↑g a) = a → ↑f a = a ∧ ↑g a = a
exact
  (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
    ⟨(congr_arg f hg).symm.trans h, hg⟩