awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
refine : ∀ (x : F), LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
⊢ v.IsEquiv w

Tactic:
refine isEquiv_iff_lt_one_iff.2 fun x ↦ ?_

Premises used: Iff.mpr, AbsoluteValue.isEquiv_iff_lt_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
rw : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ)
| LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
rw [← WithAbs.ofAbs_toAbs v x]

Premises used: WithAbs.ofAbs_toAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
conv_lhs :
  LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
conv_lhs => rw [← WithAbs.ofAbs_toAbs v x]

Premises used: WithAbs.ofAbs_toAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
rw : LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)
| LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
rw [← WithAbs.ofAbs_toAbs w x]

Premises used: WithAbs.ofAbs_toAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
conv_rhs :
  LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
conv_rhs => rw [← WithAbs.ofAbs_toAbs w x]

Premises used: WithAbs.ofAbs_toAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
rw :
  Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0) ↔
    Filter.Tendsto.{0, u_1} (β := WithAbs w) (fun (n : ℕ) ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)

Tactic:
rw [← WithAbs.norm_eq_apply_ofAbs, ← WithAbs.norm_eq_apply_ofAbs,
    ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]

Premises used: tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, WithAbs.norm_eq_apply_ofAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h_1 :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
h : Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto.{0, u_1} (β := WithAbs w) (fun (n : ℕ) ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)

Tactic:
simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h

Premises used: Continuous.tendsto, Function.comp_def, Filter.Tendsto.comp, OfNat.ofNat, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h_1 :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
h : Filter.Tendsto.{0, u_1} (β := WithAbs w) (fun (n : ℕ) ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)

Tactic:
simpa [Function.comp_def] using (hi.continuous_iff (f := (WithAbs.congr v w (.refl F)).symm)).2
      continuous_id |>.tendsto 0 |>.comp h

Premises used: Iff.mpr, Continuous.tendsto, Function.comp_def, continuous_id, Filter.Tendsto.comp, Topology.IsEmbedding.continuous_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
x : F
⊢ Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0) ↔
    Filter.Tendsto.{0, u_1} (β := WithAbs w) (fun (n : ℕ) ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)

Tactic:
exact ⟨fun h ↦ by simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h, fun h ↦ by
    simpa [Function.comp_def] using (hi.continuous_iff (f := (WithAbs.congr v w (.refl F)).symm)).2
      continuous_id |>.tendsto 0 |>.comp h ⟩
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f p x

Tactic:
⟨r, hf⟩

Premises used: Exists.intro, HasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Tactic:
⟨p, hf⟩

Premises used: AnalyticAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 f x

Tactic:
hf.hasFPowerSeriesAt.analyticAt

Premises used: HasFPowerSeriesOnBall.hasFPowerSeriesAt, HasFPowerSeriesAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
⟨r, hf⟩

Premises used: HasFPowerSeriesWithinAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
⟨p, hf⟩

Premises used: AnalyticWithinAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
hf.hasFPowerSeriesWithinAt.analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.analyticWithinAt, HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + z))

Tactic:
hf.hasSum hz

Premises used: HasFPowerSeriesOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 r) z
h : x + y + z - y = x + z
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z - y))

Tactic:
convert! hf.hasSum hz using 2

Premises used: HasFPowerSeriesOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ x + y + z - y = x + z

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
simp : ∀ (hz1 : z = 0 ∨ x + y + z + -y ∈ s), z = 0 ∨ x + z ∈ s
⊢ x + z ∈ insert x s

Tactic:
simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢

Premises used: Set.image_add_right, add_eq_left, Set.add_singleton, Set.mem_insert_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
hz1 : z = 0 ∨ x + y + z + -y ∈ s
⊢ z = 0 ∨ x + z ∈ s

Tactic:
abel_nf at hz1
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
hz1 : z = 0 ∨ x + z ∈ s
⊢ z = 0 ∨ x + z ∈ s

Tactic:
assumption
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ x + z ∈ insert x s

Tactic:
have : x + z ∈ insert x s := by
      simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
      abel_nf at hz1
      assumption
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
this : x + z ∈ insert x s
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + z))

Tactic:
hf.hasSum this hz2

Premises used: HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
this : x + z ∈ insert x s
h : x + y + z - y = x + z
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z - y))

Tactic:
convert! hf.hasSum this hz2 using 2

Premises used: HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
this : x + z ∈ insert x s
⊢ x + y + z - y = x + z

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
y : E
obtain : ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesOnBall f p x r), HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)
⊢ HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)

Tactic:
obtain ⟨r, hf⟩ := hf
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)

Tactic:
⟨r, hf.comp_sub _⟩

Premises used: HasFPowerSeriesOnBall.comp_sub, Exists.intro, HasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)

Tactic:
exact ⟨r, hf.comp_sub _⟩
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
y : E
obtain :
  ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s x r),
    HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)
⊢ HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)

Tactic:
obtain ⟨r, hf⟩ := hf
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)

Tactic:
⟨r, hf.comp_sub _⟩

Premises used: HasFPowerSeriesWithinOnBall.comp_sub, HasFPowerSeriesWithinAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)

Tactic:
exact ⟨r, hf.comp_sub _⟩
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
x : E
hf : AnalyticAt 𝕜 f x
y : E
obtain :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesAt f p x),
    AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)

Tactic:
obtain ⟨p, hf⟩ := hf
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
x y : E
p : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f p x
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)

Tactic:
⟨p, hf.comp_sub _⟩

Premises used: HasFPowerSeriesAt.comp_sub, AnalyticAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
x y : E
p : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f p x
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)

Tactic:
exact ⟨p, hf.comp_sub _⟩
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ x + -y ∈ s

Tactic:
simp only [add_singleton, image_add_right, mem_preimage] at hx

Premises used: Set.image_add_right, Set.add_singleton, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x = x - y + y

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
rw : AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x - y + y)
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) x

Tactic:
rw [show x = (x - y) + y by abel]
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x + -y ∈ s

Tactic:
hx
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
h : x - y = x + -y
⊢ x - y ∈ s

Tactic:
convert! hx using 1
-- Module: Mathlib.Analysis.Analytic.Basic
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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y = x + -y

Tactic:
abel