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 : ℝ
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:
exact Tendsto.comp
      (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')

Premises used: tendsto_nhdsWithin_mono_left, Set.Ioo_subset_Iio_self, Continuous.continuousAt, IsBoundedBilinearMap.continuous_right, Filter.Tendsto.comp, 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 : ℝ
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 : ℝ) ↦ 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_Iio_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 : ℝ
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
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 b a) 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 : ℝ
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
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 : ℝ
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
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 : ℝ
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
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
⊢ HasDerivWithinAt f e (Icc b a) a

Tactic:
have : HasDerivWithinAt f e (Icc b a) 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 : ℝ
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
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
this : HasDerivWithinAt f e (Icc b a) a
⊢ HasDerivWithinAt f e (Iic a) a

Tactic:
this.mono_of_mem_nhdsWithin (Icc_mem_nhdsLE ba)

Premises used: HasDerivWithinAt.mono_of_mem_nhdsWithin, Icc_mem_nhdsLE
-- 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
t_diff' : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
this : HasDerivWithinAt f e (Icc b a) a
⊢ HasDerivWithinAt f e (Iic a) a

Tactic:
exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsLE ba)

Premises used: HasDerivWithinAt.mono_of_mem_nhdsWithin, Icc_mem_nhdsLE
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ DifferentiableOn ℝ f (Ioi x)

Tactic:
have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
      (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
hasDerivWithinAt_Ici_of_tendsto_deriv : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] x) (𝓝 (g x))
⊢ HasDerivWithinAt f (g x) (Ici x) x

Tactic:
apply
      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin

Premises used: ContinuousAt.continuousWithinAt, self_mem_nhdsWithin, hasDerivWithinAt_Ici_of_tendsto_deriv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ Tendsto g (𝓝[>] x) (𝓝 (g x))

Tactic:
have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
apply : g =ᶠ[𝓝[>] x] fun (x : ℝ) ↦ deriv f x
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] x) (𝓝 (g x))

Tactic:
apply this.congr' _

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
apply :
  ∀ (y : ℝ) (hy : y ∈ Ioi x),
    Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y
⊢ g =ᶠ[𝓝[>] x] fun (x : ℝ) ↦ deriv f x

Tactic:
apply mem_of_superset self_mem_nhdsWithin fun y hy => _

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Ioi x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y

Tactic:
(f_diff y (ne_of_gt hy)).deriv.symm

Premises used: Set.Mem, HasDerivAt.deriv, setOf, ne_of_gt, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Ioi x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y

Tactic:
exact (f_diff y (ne_of_gt hy)).deriv.symm

Premises used: HasDerivAt.deriv, ne_of_gt, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivWithinAt f (g x) (Ici x) x

Tactic:
have A : HasDerivWithinAt f (g x) (Ici x) x := by
    have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
      (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_gt hy)).deriv.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ DifferentiableOn ℝ f (Iio x)

Tactic:
have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
      (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
hasDerivWithinAt_Iic_of_tendsto_deriv : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))
⊢ HasDerivWithinAt f (g x) (Iic x) x

Tactic:
apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin

Premises used: hasDerivWithinAt_Iic_of_tendsto_deriv, ContinuousAt.continuousWithinAt, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto g (𝓝[<] x) (𝓝 (g x))

Tactic:
have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
apply : g =ᶠ[𝓝[<] x] fun (x : ℝ) ↦ deriv f x
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))

Tactic:
apply this.congr' _

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
apply :
  ∀ (y : ℝ) (hy : y ∈ Iio x),
    Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y
⊢ g =ᶠ[𝓝[<] x] fun (x : ℝ) ↦ deriv f x

Tactic:
apply mem_of_superset self_mem_nhdsWithin fun y hy => _

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y

Tactic:
(f_diff y (ne_of_lt hy)).deriv.symm

Premises used: Set.Mem, HasDerivAt.deriv, setOf, Eq.symm, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = (fun (x : ℝ) ↦ deriv f x) x) x} y

Tactic:
exact (f_diff y (ne_of_lt hy)).deriv.symm

Premises used: HasDerivAt.deriv, Eq.symm, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivWithinAt f (g x) (Iic x) x

Tactic:
have B : HasDerivWithinAt f (g x) (Iic x) x := by
    have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
      (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_lt hy)).deriv.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x

Tactic:
simpa using B.union A

Premises used: HasDerivWithinAt.union
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
inl :
  ∀ (f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1) (hf : ContinuousAt f y) (hg : ContinuousAt g y),
    HasDerivAt f (g y) y
inr : ∀ (hne : y ≠ x), HasDerivAt f (g y) y
⊢ HasDerivAt f (g y) y

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y

Tactic:
hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg

Premises used: hasDerivAt_of_hasDerivAt_of_ne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y

Tactic:
exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg

Premises used: hasDerivAt_of_hasDerivAt_of_ne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Tactic:
f_diff y hne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y

Tactic:
exact f_diff y hne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
L : Filter (E × E)
x : E × E
⊢ 0 x =
    HSub.hSub (β := F) (HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x.1 : F) ((f : (a : E) → F) x.2 : F))
      ((f : (a : E) → F) (x.1 - x.2) : F)

Tactic:
simp only [f.map_sub, sub_self, Pi.zero_apply]

Premises used: sub_self, ContinuousLinearMap.map_sub, Pi.zero_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
⊢ HasStrictFDerivAt (⇑f : (a : E) → F) f x

Tactic:
f.hasFDerivAtFilter

Premises used: ContinuousLinearMap.hasFDerivAtFilter, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt (⇑f : (a : E) → F) f s x

Tactic:
f.hasFDerivAtFilter

Premises used: HasFDerivWithinAt, ContinuousLinearMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
⊢ HasFDerivAt (⇑f : (a : E) → F) f x

Tactic:
f.hasFDerivAtFilter

Premises used: HasFDerivAt, ContinuousLinearMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
f.hasFDerivAt.differentiableAt

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s x

Tactic:
f.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, ContinuousLinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
fun _ =>
  f.differentiableAt

Premises used: Differentiable, ContinuousLinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
s : Set E
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
f.differentiable.differentiableOn

Premises used: ContinuousLinearMap.differentiable, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
⊢ fderiv 𝕜 (⇑f : (a : E) → F) x = f

Tactic:
f.hasFDerivAt.fderiv

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
rw : fderiv 𝕜 (⇑f : (a : E) → F) x = f
⊢ fderivWithin 𝕜 (⇑f : (a : E) → F) s x = f

Tactic:
rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]

Premises used: DifferentiableAt.fderivWithin, ContinuousLinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f : (a : E) → F) x = f

Tactic:
f.fderiv

Premises used: ContinuousLinearMap.fderiv