Theorem: ContDiffOn.continuousOn_derivWithin'' (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
by_cases hab : a = b
State after:
case pos
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)

case neg
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : ¬a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)

State before:
case pos
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
simp [continuousOn_singleton, hab]
State after:
no goals

State before:
case neg
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : ¬a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
refine h.continuousOn_derivWithin (uniqueDiffOn_Icc (min_lt_max.2 hab)) hn
State after:
no goals