Theorem: perm_conj (Bruhat/Goal.lean)

State before:
α : Type u_1
f g : Equiv.Perm α
a b : α
hab : f a = b
⊢ g (f (g.symm (g a))) = g b
Tactic:
rw [Equiv.symm_apply_apply, hab]
State after:
no goals