Theorem: Weight.pair_perm' (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair w (Weight.comp a σ⁻¹)
Tactic:
rw [← pair_perm w _ σ]
State after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair (Weight.comp w σ) (Weight.comp (Weight.comp a σ⁻¹) σ)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair (Weight.comp w σ) (Weight.comp (Weight.comp a σ⁻¹) σ)
Tactic:
simp only [comp_comp, mul_left_inv, comp_one]
State after:
no goals