awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
h'y : x + (y + z) ∈ insert x s
hy₁ : Membership.mem (γ := Set E) (Metric.eball 0 r) (y + z)
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]

Premises used: add_assoc, HasFPowerSeriesWithinOnBall.sum, HasFPowerSeriesWithinOnBall.r_le, LT.lt.trans_le, FormalMultilinearSeries.changeOrigin_eval
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ insert (x + y) s ⊆ insert (x + y) (insert x s)

Tactic:
apply insert_subset_insert (subset_insert _ _)

Premises used: Set.subset_insert, Set.insert_subset_insert
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ insert (x + y) s ⊆ insert (x + y) (insert x s)

Tactic:
have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert (x + y) (insert x s)
⊢ insert (x + y) s ⊆ insert x s

Tactic:
rw [insert_eq_of_mem hy] at this

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert x s
h'y : x + (y + z) ∈ insert (x + y) s
⊢ x + (y + z) ∈ insert x s

Tactic:
apply this
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert x s
⊢ x + (y + z) ∈ insert (x + y) s

Tactic:
simpa [add_assoc] using h'z

Premises used: add_assoc
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y + z)

Tactic:
mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)

Premises used: Iff.mpr, lt_of_le_of_lt, Set.Mem, enorm_add_le, mem_eball_zero_iff
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y + z)

Tactic:
exact mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)

Premises used: Iff.mpr, lt_of_le_of_lt, mem_eball_zero_iff
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
      · have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
        rw [insert_eq_of_mem hy] at this
        apply this
        simpa [add_assoc] using h'z
      exact mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
rw :
  HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
apply : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin y).radius) z
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)

Tactic:
apply (p.changeOrigin y).hasSum

Premises used: FormalMultilinearSeries.hasSum, FormalMultilinearSeries.changeOrigin
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin y).radius) z

Tactic:
Metric.eball_subset_eball (le_trans ?_ p.changeOrigin_radius) hz

Premises used: Metric.eball_subset_eball, Set.Mem, FormalMultilinearSeries.changeOrigin_radius, le_trans
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
refine : r - ‖y‖ₑ ≤ p.radius - (↑‖y‖₊ : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin y).radius) z

Tactic:
refine Metric.eball_subset_eball (le_trans ?_ p.changeOrigin_radius) hz

Premises used: Metric.eball_subset_eball, FormalMultilinearSeries.changeOrigin_radius, le_trans
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ r - ‖y‖ₑ ≤ p.radius - (↑‖y‖₊ : ℝ≥0∞)

Tactic:
tsub_le_tsub hf.r_le le_rfl

Premises used: le_rfl, tsub_le_tsub, HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ r - ‖y‖ₑ ≤ p.radius - (↑‖y‖₊ : ℝ≥0∞)

Tactic:
exact tsub_le_tsub hf.r_le le_rfl

Premises used: le_rfl, tsub_le_tsub, HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : (↑‖y‖₊ : ℝ≥0∞) < r
rw :
  ∀ (hf : HasFPowerSeriesWithinOnBall f p univ x r) (h : (↑‖y‖₊ : ℝ≥0∞) < r),
    HasFPowerSeriesWithinOnBall f (p.changeOrigin y) univ (x + y) (r - (↑‖y‖₊ : ℝ≥0∞))
⊢ HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - (↑‖y‖₊ : ℝ≥0∞))

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ Membership.mem (γ := Set E) (insert x univ) (x + y)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ HasFPowerSeriesWithinOnBall f (p.changeOrigin y) univ (x + y) (r - (↑‖y‖₊ : ℝ≥0∞))

Tactic:
exact hf.changeOrigin h (by simp)

Premises used: HasFPowerSeriesWithinOnBall.changeOrigin
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r

Tactic:
simpa [edist_eq_enorm_sub] using h.2

Premises used: edist_eq_enorm_sub, And.right
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r

Tactic:
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h.2
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this : (↑‖y - x‖₊ : ℝ≥0∞) < r
⊢ x + (y - x) ∈ insert x s

Tactic:
simpa using h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this : (↑‖y - x‖₊ : ℝ≥0∞) < r
⊢ HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s (x + (y - x)) (r - ‖y - x‖ₑ)

Tactic:
have := hf.changeOrigin this (by simpa using h.1)
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s (x + (y - x)) (r - ‖y - x‖ₑ)
⊢ HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s y (r - ‖y - x‖ₑ)

Tactic:
rw [add_sub_cancel] at this

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s y (r - ‖y - x‖ₑ)
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
this.analyticWithinAt

Premises used: HasFPowerSeriesWithinOnBall.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s y (r - ‖y - x‖ₑ)
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
exact this.analyticWithinAt

Premises used: HasFPowerSeriesWithinOnBall.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ Metric.eball x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ Metric.eball x r
hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
⊢ y ∈ Metric.eball x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
rw : AnalyticWithinAt 𝕜 f univ y
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [← analyticWithinAt_univ]

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ y ∈ insert x univ ∩ Metric.eball x r

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f univ y

Tactic:
exact hf.analyticWithinAt_of_mem (by simpa using h)

Premises used: HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticOn 𝕜 f (insert x s ∩ Metric.eball x r)

Tactic:
fun _ hy ↦ ((analyticWithinAt_insert (y := x)).2 (hf.analyticWithinAt_of_mem hy)).mono
    inter_subset_left

Premises used: Iff.mpr, AnalyticOn, HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem, Set.inter_subset_left, AnalyticWithinAt.mono, analyticWithinAt_insert
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ AnalyticOnNhd 𝕜 f (Metric.eball x r)

Tactic:
fun _y hy => hf.analyticAt_of_mem hy

Premises used: AnalyticOnNhd, HasFPowerSeriesOnBall.analyticAt_of_mem
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
rw : ∀ (x : E), Membership.mem (γ := Set E) {x : E | AnalyticAt 𝕜 f x} x → {x : E | AnalyticAt 𝕜 f x} ∈ 𝓝 x
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : E | AnalyticAt 𝕜 f x}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ {x : E | AnalyticAt 𝕜 f x} ∈ 𝓝 x

Tactic:
mem_of_superset (Metric.eball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy

Premises used: HasFPowerSeriesOnBall.analyticAt_of_mem, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ {x : E | AnalyticAt 𝕜 f x} ∈ 𝓝 x

Tactic:
exact mem_of_superset (Metric.eball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy

Premises used: HasFPowerSeriesOnBall.analyticAt_of_mem, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
⊢ ∀ᶠ (y : E) in 𝓝 x, AnalyticAt 𝕜 f y

Tactic:
(isOpen_analyticAt 𝕜 f).mem_nhds h

Premises used: Set.Mem, Filter.Eventually, setOf, IsOpen.mem_nhds, isOpen_analyticAt
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
⊢ ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s

Tactic:
h.eventually_analyticAt.exists_mem

Premises used: AnalyticOnNhd, Filter.Eventually.exists_mem, AnalyticAt.eventually_analyticAt
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
⊢ ∃ (r : ℝ), 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r)

Tactic:
Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h

Premises used: Set.Mem, AnalyticOnNhd, setOf, Set.Subset, Metric.isOpen_iff, AnalyticAt, isOpen_analyticAt, Iff.mp