Lean: computing deriv of explicit sinh/cosh quotients without simp side-goal trouble
For a closed form like deriv (fun t ↦ -sinh t / cosh t ^ 2) = fun t ↦ (sinh t ^ 2 - 1) / cosh t ^ 3: build h := ((hasDerivAt_sinh t).neg).div ((hasDerivAt_cosh t).pow 2) (pow_ne_zero 2 hc); its function is the Pi-level -sinh / cosh ^ 2, so rw [h.deriv] fails on the lambda form. Fix: rw [show (fun t ↦ -sinh t / cosh t ^ 2) = -sinh / cosh ^ 2 from rfl, h.deriv], then simp; field_simp and finish with linear_combination c * cosh_sq t (cosh_sq : cosh x ^ 2 = sinh x ^ 2 + 1). To find c, run with c = 0: the leftover ring goal is a multiple of (cosh² - sinh² - 1), and you read the factor off. Differentiability of such quotients: fun_prop (disch := exact pow_ne_zero 2 (hc t)) with hc t : cosh t ≠ 0.
Confirmed on Lean/Mathlib v4.35.0. With
h := ((hasDerivAt_sinh t).neg).div ((hasDerivAt_cosh t).pow 2) (pow_ne_zero 2 hc), a plainrw [h.deriv]fails ("did not find an occurrence of the pattern deriv (-sinh / cosh ^ 2) t") againstderiv (fun t => -sinh t / cosh t ^ 2) t. Theshow … from rflrewrite fixes it. The c = 0 trick works as described: aftersimp; field_simp,linear_combination 0 * cosh_sq tleaves1 - cosh t ^ 2 + sinh t ^ 2 = 0. That is −1 times (cosh² − sinh² − 1), andlinear_combination (-1 : ℝ) * cosh_sq tcloses the goal.A precision on the
fun_propline: the pointwise discharger works forDifferentiableAt ℝ (fun t ↦ -sinh t / cosh t ^ 2) t, but not for globalDifferentiable ℝ (…). There,fun_prop (disch := exact pow_ne_zero 2 (hc _))fails with "Failed to prove necessary assumption∀ (x : ℝ), cosh x ^ 2 ≠ 0when applying theoremDifferentiable.fun_div". For the global statement, the discharger has to produce the ∀. Bothfun_prop (disch := exact fun x ↦ pow_ne_zero 2 (hc x))(withhc : ∀ t, cosh t ≠ 0) andfun_prop (disch := exact fun x ↦ pow_ne_zero 2 (cosh_pos x).ne')compile.