awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (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
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
have neg : ¬DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) s x
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (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 g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 f x
have refine : ∀ (h : DifferentiableAt 𝕜 (f + g) x), DifferentiableAt 𝕜 f x
Tactic: refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 f s
have refine : ∀ (h : DifferentiableOn 𝕜 (f + g) s), DifferentiableOn 𝕜 f s
Tactic: refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (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 g : E → F
hg : Differentiable 𝕜 g
⊢ Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 f
have refine : ∀ (h : Differentiable 𝕜 (f + g)), Differentiable 𝕜 f
Tactic: refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ map (fun (x : E) ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)
have simp : map (fun (x : E) ↦ a + x) (𝓝 x) ⊓ map (fun (x : E) ↦ a + x) (𝓟 s) = 𝓝 (a + x) ⊓ 𝓟 (a +ᵥ s)
Tactic: simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (hypothesis)
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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)
have this : map (fun (x : E) ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)
Tactic: have : map (a + ·) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x) := by
    simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]
    simp [← Set.image_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Affine (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
L : Filter (E × E)
⊢ HasFDerivAtFilter (⇑f : (a : E) → F) f.contLinear L
have refine : ∀ (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.contLinear : (a : E) → F) (x.1 - x.2) : F)
Tactic: refine .of_isLittleOTVS <| .congr_left (.zero _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Affine (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
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (⇑f : (a : E) → F) s x) f.contLinear
have rw : Eq (α := E →L[𝕜] F) (fderiv 𝕜 (⇑f : (a : E) → F) x) f.contLinear
Tactic: rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ IsLittleO.{u, v, u} (E := F) (F := E) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2)
        ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                  (p 1) :
                E →L[𝕜] F) :
              (a : E) → F)
            (y.1 - y.2) :
          F))
    fun (y : E × E) ↦ y.1 - y.2
have refine : IsLittleO (E := ℝ) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x)) (fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖)
  fun (x : E × E) ↦ ‖x.1 - x.2‖
Tactic: refine h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x)) (fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖)
    fun (x : E × E) ↦ ‖x.1 - x.2‖
have refine : Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝[insert x s ×ˢ insert x s] (x, x)) (𝓝 0)
Tactic: refine isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, ?_, EventuallyEq.rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝[insert x s ×ˢ insert x s] (x, x)) (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝 (x, x)) (𝓝 0)
Tactic: apply Tendsto.mono_left _ nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝 (x, x)) (𝓝 0)
have refine : ‖id (x, x) - (x, x)‖ = 0
Tactic: refine (continuous_id.sub continuous_const).norm.tendsto' _ _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ ‖id (x, x) - (x, x)‖ = 0
have rw : ‖(x, x) - (x, x)‖ = 0
Tactic: rw [_root_.id, sub_self, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
rw : ‖(x, x) - (x, x)‖ = 0
⊢ ‖id (x, x) - (x, x)‖ = 0
have rw₁ : norm.{u} (E := E × E) 0 = 0
Tactic: rw [_root_.id, sub_self, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
rw : ‖(x, x) - (x, x)‖ = 0
rw₁ : norm.{u} (E := E × E) 0 = 0
⊢ ‖id (x, x) - (x, x)‖ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [_root_.id, sub_self, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    (insert x s) x
have rw : ∀ ⦃c : ℝ⦄,
  0 < c →
    ∀ᶠ (x_1 : E) in 𝓝[insert x s] x,
      ‖HSub.hSub (β := F) (f x_1 - f x)
            ((((continuousMultilinearCurryFin1 𝕜 E F :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                      (p 1) :
                    E →L[𝕜] F) :
                  (a : E) → F)
                (x_1 - x) :
              F)‖ ≤
        c * ‖x_1 - x‖
Tactic: rw [hasFDerivWithinAt_iff_isLittleO, isLittleO_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))
have rw : Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s] x ×ˢ 𝓝[insert x s] x)
Tactic: rw [nhdsWithin_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x_1 : E) in 𝓝[insert x s] x,
    ‖HSub.hSub (β := F) (f x_1 - f x)
          ((((continuousMultilinearCurryFin1 𝕜 E F :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                    (p 1) :
                  E →L[𝕜] F) :
                (a : E) → F)
              (x_1 - x) :
            F)‖ ≤
      c * ‖x_1 - x‖
have this : Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))
Tactic: have : Tendsto (fun y ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x)) := by
    rw [nhdsWithin_prod_eq]
    exact Tendsto.prodMk tendsto_id (tendsto_const_nhdsWithin (by simp))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : AnalyticWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x
have obtain : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s x), DifferentiableWithinAt 𝕜 f (insert x s) x
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesAt f p x), HasStrictFDerivAt f (fderiv 𝕜 f x) x
Tactic: rcases h with ⟨p, hp⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x
have rw : HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
  ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F) (p 1))
  x
Tactic: rw [hp.fderiv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
have Z : DifferentiableWithinAt 𝕜 f (insert y s) y
Tactic: have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
have inl : ∀ (h : HasFPowerSeriesWithinOnBall f p s y r) (hy : y ∈ insert y s ∩ Metric.eball y r),
  DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y
Tactic: rcases eq_or_ne y x with rfl | hy
Cleared hypotheses: x, h, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
inl :
  ∀ (h : HasFPowerSeriesWithinOnBall f p s y r) (hy : y ∈ insert y s ∩ Metric.eball y r),
    DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
have inr : ∀ (hy : y ≠ x), DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
Tactic: rcases eq_or_ne y x with rfl | hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
have inr : s ∈ 𝓝[insert x s ∩ Metric.eball x r] y
Tactic: apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s ∩ Metric.eball x r] y
have inr : s ∈ 𝓝[insert x s] y
Tactic: suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[insert x s] y
have inr : s ∈ 𝓝[s] y
Tactic: rw [nhdsWithin_insert_of_ne hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
inst_5 : CompleteSpace F
hp : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z
have obtain : ∀ (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r), ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z
Tactic: obtain ⟨r, hp⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)
have inl : ∀ (hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r) (h'y : x + 0 ∈ insert x s),
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin 0 1))
    (insert x s) (x + 0)
Tactic: rcases eq_or_ne y 0 with rfl | h''y
Cleared hypotheses: y, hy, h'y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
inl :
  ∀ (hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r) (h'y : x + 0 ∈ insert x s),
    HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin 0 1))
      (insert x s) (x + 0)
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)
have inr : ∀ (h''y : y ≠ 0),
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)
Tactic: rcases eq_or_ne y 0 with rfl | h''y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r
h'y : x + 0 ∈ insert x s
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin 0 1))
    (insert x s) (x + 0)
have h₁ : x = x + 0
Tactic: convert! (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)
have Z : HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
  ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
    (p.changeOrigin y 1))
  (insert (x + y) s) (x + y)
Tactic: have Z := (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)
have inr : s ∈ 𝓝[insert x s] (x + y)
Tactic: apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[insert x s] (x + y)
have inr : s ∈ 𝓝[s] (x + y)
Tactic: rw [nhdsWithin_insert_of_ne]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
inr : s ∈ 𝓝[s] (x + y)
⊢ s ∈ 𝓝[insert x s] (x + y)
have inr₁ : x + y ≠ x
Tactic: rw [nhdsWithin_insert_of_ne]