α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ∪ support g
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ⊔ support g
simp only [sup_eq_union]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ ↑f x = x ∧ ↑g x = x → ↑f (↑g x) = x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ∪ support g
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
hf : ↑f x = x
hg : ↑g x = x
⊢ ↑f (↑g x) = x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ ↑f x = x ∧ ↑g x = x → ↑f (↑g x) = x
rintro ⟨hf, hg⟩
no goals
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
hf : ↑f x = x
hg : ↑g x = x
⊢ ↑f (↑g x) = x
rw [hg, hf]