simp only [Weight.comp, Equiv.Perm.coe_mul]
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    w' ∘ ⇑(Tuple.sort w') ∘ ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort ((w' ∘ ⇑(Tuple.sort w')) ∘ ⇑(Tuple.sort w)))