𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a
refine' ⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, _⟩
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
⊢ ContinuousWithinAt (dslope f a) s x
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
rintro ⟨hc, hd⟩ x hx
case intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x

case intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
hne : x ≠ a
⊢ ContinuousWithinAt (dslope f a) s x
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
⊢ ContinuousWithinAt (dslope f a) s x
rcases eq_or_ne x a with (rfl | hne)
no goals
case intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x

case intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
hne : x ≠ a
⊢ ContinuousWithinAt (dslope f a) s x
exacts [(continuousAt_dslope_same.2 hd).continuousWithinAt,
  (continuousWithinAt_dslope_of_ne hne).2 (hc x hx)]