awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
f_lim.mono ts

Premises used: ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
exact f_lim.mono ts

Premises used: ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
⊢ y ∈ s

Tactic:
have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y

Tactic:
(f_diff.continuousOn y this).mono ts

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y

Tactic:
exact (f_diff.continuousOn y this).mono ts

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
⊢ ∀ y ∈ closure t, ContinuousWithinAt f t y

Tactic:
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y := by
    rw [t_closure]
    intro y hy
    by_cases h : y = a
    · rw [h]; exact f_lim.mono ts
    · have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
      exact (f_diff.continuousOn y this).mono ts
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
simp : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
simp only [toSpanSingleton_deriv.symm]

Premises used: toSpanSingleton_deriv, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')

Premises used: ContinuousLinearMap.smulRight, tendsto_nhdsWithin_mono_left, deriv, Continuous.continuousAt, ContinuousLinearMap.toSpanSingleton, IsBoundedBilinearMap.continuous_right, Filter.Tendsto.comp, LinearMap.toSpanSingleton, Set.Ioo_subset_Ioi_self, isBoundedBilinearMap_smulRight
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')

Premises used: tendsto_nhdsWithin_mono_left, Continuous.continuousAt, IsBoundedBilinearMap.continuous_right, Filter.Tendsto.comp, Set.Ioo_subset_Ioi_self, isBoundedBilinearMap_smulRight
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (1 : ℝ →L[ℝ] ℝ) e)) := by
    simp only [toSpanSingleton_deriv.symm]
    exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
rw : HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a
⊢ HasDerivWithinAt f e (Icc a b) a

Tactic:
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]

Premises used: hasDerivWithinAt_iff_hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a

Tactic:
hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'

Premises used: hasFDerivWithinAt_closure_of_tendsto_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a

Tactic:
exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'

Premises used: hasFDerivWithinAt_closure_of_tendsto_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasDerivWithinAt f e (Icc a b) a

Tactic:
have : HasDerivWithinAt f e (Icc a b) a := by
    rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
    exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
this : HasDerivWithinAt f e (Icc a b) a
⊢ HasDerivWithinAt f e (Ici a) a

Tactic:
this.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE ab)

Premises used: Icc_mem_nhdsGE, HasDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
this : HasDerivWithinAt f e (Icc a b) a
⊢ HasDerivWithinAt f e (Ici a) a

Tactic:
exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE ab)

Premises used: Icc_mem_nhdsGE, HasDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
⊢ ∃ b ∈ Iio a, Ico b a ⊆ s

Tactic:
mem_nhdsLT_iff_exists_Ico_subset.1 hs

Premises used: mem_nhdsLT_iff_exists_Ico_subset, Set.Mem, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
obtain : ∀ (b : ℝ) (ba : b ∈ Iio a) (sab : Ico b a ⊆ s), HasDerivWithinAt f e (Iic a) a
⊢ HasDerivWithinAt f e (Iic a) a

Tactic:
obtain ⟨b, ba, sab⟩ : ∃ b ∈ Iio a, Ico b a ⊆ s := mem_nhdsLT_iff_exists_Ico_subset.1 hs

Premises used: mem_nhdsLT_iff_exists_Ico_subset, Iff.mp, Set.Iio
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
⊢ t ⊆ s

Tactic:
have ts : t ⊆ s := Subset.trans Ioo_subset_Ico_self sab
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
⊢ DifferentiableOn ℝ f t

Tactic:
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
⊢ Convex ℝ t

Tactic:
have t_conv : Convex ℝ t := convex_Ioo b a
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
⊢ IsOpen t

Tactic:
have t_open : IsOpen t := isOpen_Ioo
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
⊢ closure t = Icc b a

Tactic:
have t_closure : closure t = Icc b a := closure_Ioo (ne_of_lt ba)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
rw : ∀ y ∈ Icc b a, ContinuousWithinAt f t y
⊢ ∀ y ∈ closure t, ContinuousWithinAt f t y

Tactic:
rw [t_closure]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
pos : ∀ (h : y = a), ContinuousWithinAt f t y
neg : ∀ (h : ¬y = a), ContinuousWithinAt f t y
⊢ ContinuousWithinAt f t y

Tactic:
by_cases h : y = a
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
pos : ContinuousWithinAt f t a
⊢ ContinuousWithinAt f t y

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
f_lim.mono ts

Premises used: ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
exact f_lim.mono ts

Premises used: ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
⊢ y ∈ s

Tactic:
have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y

Tactic:
(f_diff.continuousOn y this).mono ts

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y

Tactic:
exact (f_diff.continuousOn y this).mono ts

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
⊢ ∀ y ∈ closure t, ContinuousWithinAt f t y

Tactic:
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y := by
    rw [t_closure]
    intro y hy
    by_cases h : y = a
    · rw [h]; exact f_lim.mono ts
    · have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
      exact (f_diff.continuousOn y this).mono ts
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
simp : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
simp only [toSpanSingleton_deriv.symm]

Premises used: toSpanSingleton_deriv, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
⊢ Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))

Tactic:
Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')

Premises used: ContinuousLinearMap.smulRight, tendsto_nhdsWithin_mono_left, deriv, Set.Ioo_subset_Iio_self, Continuous.continuousAt, ContinuousLinearMap.toSpanSingleton, IsBoundedBilinearMap.continuous_right, Filter.Tendsto.comp, LinearMap.toSpanSingleton, isBoundedBilinearMap_smulRight