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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp (Weight.comp w σ) τ = Weight.comp w (σ * τ)
Tactic:
simp only [Weight.comp, Equiv.Perm.coe_mul]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ (w ∘ ⇑σ) ∘ ⇑τ = w ∘ ⇑σ ∘ ⇑τ

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ (w ∘ ⇑σ) ∘ ⇑τ = w ∘ ⇑σ ∘ ⇑τ
Tactic:
rfl
State after:
no goals