have help : w' = w'.comp (Tuple.sort w') ↔ Monotone w'
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w') ↔ Monotone 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'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))