Theorem: deriv.comp_of_tower (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 : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g x)
Tactic:
rw [← hasDerivAt_deriv_iff] at hf hg
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 : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : HasDerivAt f (deriv f (g x)) (g x)
hg : HasDerivAt g (deriv g x) x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g 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 : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : HasDerivAt f (deriv f (g x)) (g x)
hg : HasDerivAt g (deriv g x) x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g x)
Tactic:
exact (HasDerivAt.comp_of_tower x hf hg).deriv
State after:
no goals