Theorem: HasDerivAt.comp_of_deriv' (ForML/Util.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (fg' x) x
Tactic:
rw [← hf']
State after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv g x • _root_.deriv f (g x)) x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv g x • _root_.deriv f (g x)) x
Tactic:
exact comp_of_tower x hf.hasDerivAt hg.hasDerivAt
State after:
no goals