deriv

Stream: new members

[vxctyxeha]

i try to prove the follow do i have to use chain rule？ or may be there is easy way

import Mathlib

theorem my_favorite_theorem (x : ℝ) (hx : x ≠ 1) : deriv (fun t => (1 - t)⁻¹) x = (1 - x)^(-2 : ℝ) := by sorry

[Aaron Liu]

import Mathlib

theorem my_favorite_theorem (x : ℝ) (hx : x ≠ 1) :
    HasDerivAt (fun t => (1 - t)⁻¹) ((1 - x) ^ (-2 : ℤ)) x := by
  simpa using ((hasDerivAt_id x).const_sub 1).inv (sub_ne_zero.2 hx.symm)

[vxctyxeha]

thanks by the way did you use AI foe coding?