awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
⊢ LipschitzWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F))
have h : g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) = u
Tactic: convert! hu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
⊢ g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) = u
have h : ∀ (x : E), HSub.hSub (β := (a : E) → F) g (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) x = u x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s
have hg : ApproximatesLinearOn g (↑f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c)
Tactic: have hg : ApproximatesLinearOn g (f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c) := by
    apply LipschitzOnWith.approximatesLinearOn
    rw [lipschitzOnWith_univ]
    convert! hu
    ext x
    simp only [g, add_sub_cancel_left, ContinuousLinearEquiv.coe_coe, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
hg : ApproximatesLinearOn g (↑f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c)
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s
have this : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := f'.symm.finiteDimensional
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOn 𝕜 f (Metric.eball x r)
⊢ r ≤
      FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
        (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) →
    HasFPowerSeriesOnBall (𝕜 := 𝕜) f
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x r
have h₁ : AnalyticOnNhd 𝕜 f (Metric.eball x r)
Tactic: rw [Metric.isOpen_eball.analyticOn_iff_analyticOnNhd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
hr :
  r ≤
    FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜))
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x r
have set : let p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜);
∀ (hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p),
  HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
Tactic: set p := FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial)
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
⊢ 0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
have order : ¬0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p → False
Tactic: order
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
order order₁ order₂ order₃ : ¬0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p → False
⊢ 0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
have order₄ : FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p ≤ 0 → False
Tactic: order
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
have hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
Tactic: have hg : HasFPowerSeriesOnBall g p x p.radius := by
    simpa using (p.hasFPowerSeriesOnBall (by order)).comp_sub x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
have hg' : AnalyticOnNhd 𝕜 g (Metric.eball x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p))
Tactic: have hg' : AnalyticOnNhd 𝕜 g (Metric.eball x p.radius) := by
    simpa using p.analyticOnNhd.comp_sub x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' : AnalyticOnNhd 𝕜 g (Metric.eball x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p))
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
have hg'₁ : AnalyticOnNhd 𝕜 g (Metric.eball x r)
Tactic: replace hg' : AnalyticOnNhd 𝕜 g (Metric.eball x r) := hg'.mono (Metric.eball_subset_eball hr)
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' : AnalyticOnNhd 𝕜 g (Metric.eball x r)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
have hg'₁ : ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
  Set.EqOn f g (Metric.eball x r)
Tactic: apply h.eqOn_of_preconnected_of_eventuallyEq at hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
have apply : Set.EqOn g f (Metric.eball x r)
Tactic: apply (hg.mono hr_pos hr).congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn g f (Metric.eball x r)
have symm : Set.EqOn f g (Metric.eball x r)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn f g (Metric.eball x r)
have apply : f =ᶠ[nhds x] g
Tactic: apply hg' (Metric.isConnected_eball hr_pos).isPreconnected (show x ∈ Metric.eball x r by simpa) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
⊢ f =ᶠ[nhds x] g
have hf : AnalyticAt 𝕜 f x
Tactic: have hf : AnalyticAt 𝕜 f x := h _ (by simp [hr_pos])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
hf : AnalyticAt 𝕜 f x
⊢ f =ᶠ[nhds x] g
have hf₁ : HasFPowerSeriesAt (𝕜 := 𝕜) f
  (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
Tactic: apply AnalyticAt.hasFPowerSeriesAt at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
hf :
  HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
⊢ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x} ∈ nhds x
have rw : ∃ ε > 0, Metric.eball x ε ⊆ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x}
Tactic: rw [EMetric.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 :=
  FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)
hr : r ≤ FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)
hg' :
  ∀ (hU : IsPreconnected (Metric.eball x r)) {z₀ : 𝕜} (h₀ : z₀ ∈ Metric.eball x r) (hfg : f =ᶠ[nhds z₀] g),
    Set.EqOn f g (Metric.eball x r)
hf :
  HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
⊢ ∃ ε > 0, Metric.eball x ε ⊆ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x}
have obtain : ∀ (ε : ENNReal)
  (hf :
    HasFPowerSeriesOnBall (𝕜 := 𝕜) f
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x ε),
  ∃ ε > 0, Metric.eball x ε ⊆ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x}
Tactic: obtain ⟨ε, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDerivWithin n f univ = iteratedDeriv n f
have h : ∀ (x : 𝕜), iteratedDerivWithin n f univ x = iteratedDeriv n f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x
have h : ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
h : ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x
have h₁ : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
h : ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
h₁ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x
have h₂ : Eq.{u_2 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
have rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_eq_iteratedFDeriv hs h hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
have rw₁ : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_eq_iteratedFDeriv hs h hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
rw₁ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
have rw₂ : Eq.{u_2 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_eq_iteratedFDeriv hs h hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin n f s =
    Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
have h : ∀ (x : 𝕜),
  iteratedDerivWithin n f s x =
    Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDerivWithin n f s)
have rw : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
  (Function.comp (β := F)
    (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
      (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
Tactic: rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]