Theorem: Finperm.swap_comm (Bruhat/Finperm.lean)

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ swap a b = swap b a
Tactic:
rw [funext_support_iff]
State after:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).support = (swap b a).support ∧ ∀ i ∈ (swap a b).support, (swap a b) i = (swap b a) i

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).support = (swap b a).support ∧ ∀ i ∈ (swap a b).support, (swap a b) i = (swap b a) i
Tactic:
aesop
State after:
no goals