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 (fun x => f (g x)) 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 (fun x => f (g x)) x = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv (fun x => f (g x)) 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 (fun x => f (g x)) x = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv (fun x => f (g x)) x) x
Tactic:
refine DifferentiableAt.hasDerivAt ?_
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 (fun x => f (g x)) x = fg' x
⊢ DifferentiableAt 𝕜 (fun x => 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 (fun x => f (g x)) x = fg' x
⊢ DifferentiableAt 𝕜 (fun x => f (g x)) x
Tactic:
exact DifferentiableAt.comp x hf hg
State after:
no goals