Theorem: Equiv.Perm.support'_prod (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f✝ f g : Perm α
⊢ support' (f * g) ⊆ support' f ∪ support' g
Tactic:
refine fun x hx ↦ by_contra <| fun h ↦ hx ?_
State after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : x ∉ support' f ∪ support' g
⊢ (f * g) x = x

State before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : x ∉ support' f ∪ support' g
⊢ (f * g) x = x
Tactic:
simp only [mem_union, not_or, not_mem_support'] at h
State after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ (f * g) x = x

State before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ (f * g) x = x
Tactic:
rw [coe_mul, Function.comp_apply]
State after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ f (g x) = x

State before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ f (g x) = x
Tactic:
simp [h.1, h.2]
State after:
no goals