Simplified0.3
\[\leadsto \color{blue}{\left(-s\right) \cdot \log \left(\frac{1}{\frac{u}{1 + e^{\frac{-\pi}{s}}} - \frac{u + -1}{1 + e^{\frac{\pi}{s}}}} + -1\right)}
\]
Proof
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (/.f32 u (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 (+.f32 u -1) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (/.f32 (Rewrite<= *-lft-identity_binary32 (*.f32 1 u)) (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 (+.f32 u -1) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (Rewrite<= associate-*l/_binary32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u)) (/.f32 (+.f32 u -1) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (/.f32 (+.f32 u (Rewrite<= metadata-eval (neg.f32 1))) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (/.f32 (Rewrite<= sub-neg_binary32 (-.f32 u 1)) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 22 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (Rewrite=> div-sub_binary32 (-.f32 (/.f32 u (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))))) -1))): 0 points increase in error, 22 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (-.f32 (/.f32 (Rewrite<= *-rgt-identity_binary32 (*.f32 u 1)) (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (-.f32 (Rewrite<= associate-*r/_binary32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (-.f32 (Rewrite<= *-commutative_binary32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u)) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (Rewrite<= *-lft-identity_binary32 (*.f32 1 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (Rewrite=> cancel-sign-sub-inv_binary32 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (*.f32 (neg.f32 1) (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (*.f32 (Rewrite=> metadata-eval -1) (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (Rewrite<= neg-mul-1_binary32 (neg.f32 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))))) -1))): 22 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (Rewrite<= sub0-neg_binary32 (-.f32 0 (-.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))))) -1))): 0 points increase in error, 22 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (Rewrite<= associate-+l-_binary32 (+.f32 (-.f32 0 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u)) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (+.f32 (Rewrite<= neg-sub0_binary32 (neg.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (+.f32 (Rewrite<= distribute-lft-neg-out_binary32 (*.f32 (neg.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))) u)) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 22 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (Rewrite<= associate-+l+_binary32 (+.f32 (+.f32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) u) (*.f32 (neg.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))) u)) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) -1))): 22 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (Rewrite<= distribute-rgt-in_binary32 (*.f32 u (+.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (neg.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 22 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 u (Rewrite<= sub-neg_binary32 (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 u (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) (Rewrite<= metadata-eval (neg.f32 1))))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (Rewrite<= sub-neg_binary32 (-.f32 (/.f32 1 (+.f32 (*.f32 u (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))))) 1)))): 0 points increase in error, 0 points decrease in error