Theorem: swap_conj (Bruhat/Goal.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap ((Equiv.swap a b) c) ((Equiv.swap a b) d)
Tactic:
rw [Equiv.swap_apply_apply]
State after:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap a b * Equiv.swap c d * (Equiv.swap a b)⁻¹

State before:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap a b * Equiv.swap c d * (Equiv.swap a b)⁻¹
Tactic:
rfl
State after:
no goals