Derivative_of_Inverse_Function
Disprovedcalculusproof-sketch-childproofwiki
If f'(x) != 0 and f is injective, then (f^{-1})'(f(x)) = 1/f'(x).
Preamble
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv import Mathlib.Tactic
Formal statement
theorem Derivative_of_Inverse_Function {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) (hf' : f' ≠ 0) (hfi : Function.Injective f) : HasDerivAt (Function.invFun f) (1 / f') (f x) := by sorry