Simplified0.3
\[\leadsto \color{blue}{\left(-s\right) \cdot \log \left(\frac{1}{\frac{u}{1 + e^{\frac{-\pi}{s}}} + \frac{1 - u}{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 1 u) (+.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<= *-rgt-identity_binary32 (*.f32 u 1)) (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))) (/.f32 (-.f32 1 u) (+.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-*r/_binary32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s)))))) (/.f32 (-.f32 1 u) (+.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 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (Rewrite=> div-sub_binary32 (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (/.f32 u (+.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 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (/.f32 (Rewrite<= *-lft-identity_binary32 (*.f32 1 u)) (+.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 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (-.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (Rewrite<= associate-*l/_binary32 (*.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) u))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (Rewrite=> cancel-sign-sub-inv_binary32 (+.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s)))) (*.f32 (neg.f32 (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (PI.f32) s))))) u))))) -1))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (Rewrite<= +-commutative_binary32 (+.f32 (*.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))): 0 points increase in error, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (+.f32 (Rewrite=> *-commutative_binary32 (*.f32 u (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, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (Rewrite<= associate-+l+_binary32 (+.f32 (+.f32 (*.f32 u (/.f32 1 (+.f32 1 (exp.f32 (/.f32 (neg.f32 (PI.f32)) s))))) (*.f32 u (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, 0 points decrease in error
(*.f32 (neg.f32 s) (log.f32 (+.f32 (/.f32 1 (+.f32 (Rewrite<= distribute-lft-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, 0 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