case inl
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ dslope (↑f ∘ g) b b = ↑f (dslope g b b)

case inr
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ dslope (↑f ∘ g) a b = ↑f (dslope g a b)
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
⊢ dslope (↑f ∘ g) a b = ↑f (dslope g a b)
rcases eq_or_ne b a with (rfl | hne)
case inl
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ deriv (↑f ∘ g) b = ↑f (deriv g b)
case inl
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ dslope (↑f ∘ g) b b = ↑f (dslope g b b)
simp only [dslope_same]
no goals
case inl
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ deriv (↑f ∘ g) b = ↑f (deriv g b)
exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv
no goals
case inr
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ dslope (↑f ∘ g) a b = ↑f (dslope g a b)
simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b