awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))
have inl : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x)
  (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) 0 f) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
inl :
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) 0 f) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))
have inr : ∀ (hc : c ≠ 0),
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))
have inl : fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x =
  HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
    (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
inl :
  fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))
have inr : ∀ (hc : c ≠ 0),
  fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))
have inr : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
Tactic: rw [fderivWithin_comp_smul_eq_fderivWithin_smul, fderivWithin_const_smul_field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
⊢ fderiv 𝕜 (fun (x : E) ↦ f (c • x)) x = HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
have rw : HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
  HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
Tactic: rw [← fderivWithin_univ, fderivWithin_comp_smul _ uniqueDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
⊢ HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
have inl : HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
    (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 univ)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) =
  HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0 (fderiv 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
inl :
  HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 univ)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0 (fderiv 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
⊢ HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
have inr : ∀ (hc : c ≠ 0),
  HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin.{u_1, u_1, u_3} 𝕜 (F := F) (fun (a : 𝕜) ↦ f (-a)) s x : 𝕜 →L[𝕜] F)
    (-fderivWithin 𝕜 f (-s) (-x) : 𝕜 →L[𝕜] F)
have t1 : Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (HSMul.hSMul (α := 𝕜) (-1) x)) s x)
  (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) (-1) f) (HSMul.hSMul (α := 𝕜) (-1) s) (HSMul.hSMul (α := 𝕜) (-1) x))
Tactic: have t1 := fderivWithin_comp_smul_eq_fderivWithin_smul (-1 : 𝕜) (f := f) (s := s) (x := x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t1 :
  Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (HSMul.hSMul (α := 𝕜) (-1) x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) (-1) f) (HSMul.hSMul (α := 𝕜) (-1) s) (HSMul.hSMul (α := 𝕜) (-1) x))
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin.{u_1, u_1, u_3} 𝕜 (F := F) (fun (a : 𝕜) ↦ f (-a)) s x : 𝕜 →L[𝕜] F)
    (-fderivWithin 𝕜 f (-s) (-x) : 𝕜 →L[𝕜] F)
have t1₁ : Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (-x)) s x) (fderivWithin 𝕜 (-f) (-s) (-x))
Tactic: simp only [neg_smul, one_smul, Set.neg_smul_set] at t1
Cleared hypotheses: t1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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)
⊢ HasDerivWithinAt f e (Ici a) a
have obtain : ∀ (b : ℝ) (ab : a < b) (sab : Ioc a b ⊆ s), HasDerivWithinAt f e (Ici a) a
Tactic: obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have ts : t ⊆ s
Tactic: have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_diff : DifferentiableOn ℝ f t
Tactic: have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_conv : Convex ℝ t
Tactic: have t_conv : Convex ℝ t := convex_Ioo a b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_open : IsOpen t
Tactic: have t_open : IsOpen t := isOpen_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_closure : closure t = Icc a b
Tactic: have t_closure : closure t = Icc a b := closure_Ioo ab.ne
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
have rw : ∀ y ∈ Icc a b, ContinuousWithinAt f t y
Tactic: rw [t_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
⊢ ContinuousWithinAt f t y
have pos : ∀ (h : y = a), ContinuousWithinAt f t y
Tactic: by_cases h : y = a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
pos : ∀ (h : y = a), ContinuousWithinAt f t y
⊢ ContinuousWithinAt f t y
have neg : ∀ (h : ¬y = a), ContinuousWithinAt f t y
Tactic: by_cases h : y = a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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 y
have pos : ContinuousWithinAt f t a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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 y
have this : y ∈ s
Tactic: have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_cont : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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))
have simp : Tendsto (β := ℝ →L[ℝ] E) (fun (x : ℝ) ↦ toSpanSingleton ℝ (deriv f x)) (𝓝[t] a) (𝓝 (smulRight (S := ℝ) 1 e))
Tactic: simp only [toSpanSingleton_deriv.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Ici a) a
have t_diff' : 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')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
have rw : HasFDerivWithinAt f (toSpanSingleton ℝ e) (closure t) a
Tactic: rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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 (Ici a) a
have this : 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'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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)
⊢ HasDerivWithinAt f e (Iic a) a
have obtain : ∀ (b : ℝ) (ba : b ∈ Iio a) (sab : Ico b a ⊆ s), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Iic a) a
have ts : t ⊆ s
Tactic: have ts : t ⊆ s := Subset.trans Ioo_subset_Ico_self sab
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Iic a) a
have t_diff : DifferentiableOn ℝ f t
Tactic: have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Iic a) a
have t_conv : Convex ℝ t
Tactic: have t_conv : Convex ℝ t := convex_Ioo b a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Iic a) a
have t_open : IsOpen t
Tactic: have t_open : IsOpen t := isOpen_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (hypothesis)
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
⊢ HasDerivWithinAt f e (Iic a) a
have t_closure : closure t = Icc b a
Tactic: have t_closure : closure t = Icc b a := closure_Ioo (ne_of_lt ba)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
have rw : ∀ y ∈ Icc b a, ContinuousWithinAt f t y
Tactic: rw [t_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
⊢ ContinuousWithinAt f t y
have pos : ∀ (h : y = a), ContinuousWithinAt f t y
Tactic: by_cases h : y = a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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
⊢ ContinuousWithinAt f t y
have neg : ∀ (h : ¬y = a), ContinuousWithinAt f t y
Tactic: by_cases h : y = a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Extend (goal)
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 y
have pos : ContinuousWithinAt f t a
Tactic: rw [h]