Theorem: Weight.pair_swap_eq (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ pair w (Weight.comp a (Equiv.swap i j)) = pair (Weight.comp w (Equiv.swap i j)) a
Tactic:
convert (pair_perm' w a _).symm
State after:
case h.e'_2.h.e'_4.h.e'_4
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ Equiv.swap i j = (Equiv.swap i j)⁻¹

State before:
case h.e'_2.h.e'_4.h.e'_4
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ Equiv.swap i j = (Equiv.swap i j)⁻¹
Tactic:
simp only [Equiv.swap_inv]
State after:
no goals