How to use deriv.comp?

Stream: new members

[Adomas Baliuka]

How does one use the chain rule with deriv? Is there a trick to get the _ ∘ _ to unify? Can one do this example nicely? (Yes, one can use deriv.log here but I want to see how to use deriv.comp)

import Mathlib
open Real

@[simp] lemma deriv_one_minus (x : ℝ) : deriv (fun (y : ℝ) ↦ 1 - y) x = -1 := by
  have onem (y : ℝ) : 1 - y = -(y + -1) := by ring
  simp_rw [onem]
  simp

@[simp] lemma diff_1_minusp (p : ℝ) : DifferentiableAt ℝ (fun p => 1 - p) p := by
  have (p : ℝ) : 1 - p = -(p - 1) := by ring
  simp_rw [this]
  apply differentiableAt_neg_iff.mpr
  apply DifferentiableAt.add_const
  simp

lemma deriv_log_one_sub (x : ℝ) (hh : x ≠ 1): deriv (fun p ↦ log (1 - p)) x = -(1-x)⁻¹ := by
  have (x : ℝ) : log (1 - x) = ((fun x ↦ log x) ∘ (1 - ·)) x := by simp
  simp_rw [this]
  rw [deriv.comp]  -- How to apply chain rule without this ugly hack?
  · simp
  · simp
    exact sub_ne_zero.mpr hh.symm
  · simp

[Ruben Van de Velde]

You might rewrite with Function.comp_def first. Or maybe we need a deriv.comp' with the lambda version