case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

case neg
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have A := H.hasDerivWithinAt.Ici_of_Ioi
case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
no goals
case pos
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
simpa using (uniqueDiffOn_Ici x).eq left_mem_Ici A B
case neg
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
case neg
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
rw [derivWithin_zero_of_not_differentiableWithinAt H,
  derivWithin_zero_of_not_differentiableWithinAt]
no goals
case neg
𝕜 : 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 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
rwa [differentiableWithinAt_Ioi_iff_Ici] at H