𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g✝ : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ False
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g✝ : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
⊢ ¬DifferentiableWithinAt 𝕜 g s a
intro hg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g✝ : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
this : HasDerivWithinAt id (0 * derivWithin g s a) s a
⊢ False
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g✝ : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ False
have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g✝ : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
this : HasDerivWithinAt id (0 * derivWithin g s a) s a
⊢ False
simpa using hsu.eq_deriv _ this (hasDerivWithinAt_id _ _)