Theorem: HasDerivAt.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
g' : 𝕜'
f' : F
hf : HasDerivAt f f' (g x)
hg : HasDerivAt g g' x
⊢ HasDerivAt (fun x => f (g x)) (g' • f') x
Tactic:
rw [hasDerivAt_iff_hasFDerivAt] 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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ HasFDerivAt (fun x => f (g x)) (ContinuousLinearMap.smulRight 1 (g' • f')) 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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ HasFDerivAt (fun x => f (g x)) (ContinuousLinearMap.smulRight 1 (g' • f')) x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.comp x (hf.restrictScalars 𝕜) 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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
      (ContinuousLinearMap.smulRight 1 g') =
    ContinuousLinearMap.smulRight 1 (g' • f')

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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
      (ContinuousLinearMap.smulRight 1 g') =
    ContinuousLinearMap.smulRight 1 (g' • f')
Tactic:
refine ContinuousLinearMap.ext ?_
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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ∀ (x : 𝕜),
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
          (ContinuousLinearMap.smulRight 1 g'))
        x =
      (ContinuousLinearMap.smulRight 1 (g' • f')) 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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ∀ (x : 𝕜),
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
          (ContinuousLinearMap.smulRight 1 g'))
        x =
      (ContinuousLinearMap.smulRight 1 (g' • f')) x
Tactic:
intro m
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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
m : 𝕜
⊢ (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
        (ContinuousLinearMap.smulRight 1 g'))
      m =
    (ContinuousLinearMap.smulRight 1 (g' • f')) m

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
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
m : 𝕜
⊢ (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
        (ContinuousLinearMap.smulRight 1 g'))
      m =
    (ContinuousLinearMap.smulRight 1 (g' • f')) m
Tactic:
simp
State after:
no goals