rw [help.mpr hw', comp_comp, eq_comm]
case h.e'_4
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.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
case h.e'_4
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'
⊢ Weight.comp w'
      (Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))) =
    Weight.comp w' (Tuple.sort w')