awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
h : g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) = u
⊢ LipschitzWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F))

Tactic:
convert! hu
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
h : ∀ (x : E), HSub.hSub (β := (a : E) → F) g (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) x = u x
⊢ g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) = u

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
x : E
⊢ HSub.hSub (β := (a : E) → F) g (⇑(↑f' : E →L[ℝ] F) : (a : E) → F) x = u x

Tactic:
simp only [g, add_sub_cancel_left, ContinuousLinearEquiv.coe_coe, Pi.sub_apply]

Premises used: add_sub_cancel_left, ContinuousLinearEquiv.coe_coe, Pi.sub_apply
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
⊢ 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]
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := f'.symm.finiteDimensional
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)
this : FiniteDimensional ℝ E
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s

Tactic:
⟨hg.toHomeomorph g hc, fg⟩

Premises used: ApproximatesLinearOn.toHomeomorph, Exists.intro
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)
this : FiniteDimensional ℝ E
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s

Tactic:
exact ⟨hg.toHomeomorph g hc, fg⟩
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOn 𝕜 f (Metric.eball x r)
⊢ AnalyticOnNhd 𝕜 f (Metric.eball x r)

Tactic:
rw [Metric.isOpen_eball.analyticOn_iff_analyticOnNhd] at h

Premises used: IsOpen.analyticOn_iff_analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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 : 𝕜))
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
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x r

Tactic:
set p := FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial)

Premises used: HDiv.hDiv, Nat.cast, Nat.factorial, FormalMultilinearSeries.ofScalars, iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ :
  FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p ≤ 0 → False
⊢ 0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p

Tactic:
order
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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 (𝕜 := 𝕜) g p x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p)

Tactic:
simpa using (p.hasFPowerSeriesOnBall (by order)).comp_sub x

Premises used: HasFPowerSeriesOnBall.comp_sub, FormalMultilinearSeries.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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 (𝕜 := 𝕜) 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
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ AnalyticOnNhd 𝕜 g (Metric.eball x (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜) p))

Tactic:
simpa using p.analyticOnNhd.comp_sub x

Premises used: AnalyticOnNhd.comp_sub, FormalMultilinearSeries.analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ 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
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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))
⊢ AnalyticOnNhd 𝕜 g (Metric.eball x r)

Tactic:
replace hg' : AnalyticOnNhd 𝕜 g (Metric.eball x r) := hg'.mono (Metric.eball_subset_eball hr)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ ∀ (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'

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
apply : Set.EqOn g f (Metric.eball x r)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r

Tactic:
apply (hg.mono hr_pos hr).congr

Premises used: HasFPowerSeriesOnBall.congr, HasFPowerSeriesOnBall.mono
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
symm : Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn g f (Metric.eball x r)

Tactic:
symm
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ x ∈ Metric.eball x r

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
apply : f =ᶠ[nhds x] g
⊢ Set.EqOn f g (Metric.eball x r)

Tactic:
apply hg' (Metric.isConnected_eball hr_pos).isPreconnected (show x ∈ Metric.eball x r by simpa) ?_

Premises used: IsConnected.isPreconnected, Metric.isConnected_eball
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ x ∈ Metric.eball x r

Tactic:
simp [hr_pos]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
⊢ AnalyticAt 𝕜 f x

Tactic:
have hf : AnalyticAt 𝕜 f x := h _ (by simp [hr_pos])
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x

Tactic:
apply AnalyticAt.hasFPowerSeriesAt at hf

Premises used: AnalyticAt.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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
rw : ∃ ε > 0, Metric.eball x ε ⊆ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x}
⊢ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x} ∈ nhds x

Tactic:
rw [EMetric.mem_nhds_iff]

Premises used: EMetric.mem_nhds_iff
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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
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}
⊢ ∃ ε > 0, Metric.eball x ε ⊆ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = g x) x}

Tactic:
obtain ⟨ε, hf⟩ := hf
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
ε : 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:
⟨ε, hf.r_pos, hf.unique (hg.mono hf.r_pos hf.r_le)⟩

Premises used: HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.unique, And.intro, Exists.intro, HasFPowerSeriesOnBall.mono, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
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)
ε : 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:
exact ⟨ε, hf.r_pos, hf.unique (hg.mono hf.r_pos hf.r_le)⟩
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hr :
  0 <
    FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜))
hs :
  AnalyticOn 𝕜 f
    (Metric.eball x
      (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
    (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)))

Tactic:
hs.hasFPowerSeriesOnSubball hr le_rfl

Premises used: le_rfl, AnalyticOn.hasFPowerSeriesOnSubball