rwa [← h]
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 n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
h :
  w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
no goals