awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E_1 F
a : E_1
i : E_1 ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F
h : HasFPowerSeriesAt (↑f : E_1 → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F) :
        (a : E_1 →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F)
      (↑i : E_1 →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E_1) ∘ (↑f : E_1 → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) (a + y) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F → E_1) ((↑f : E_1 → F) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      y
E :
  ∀ᶠ (z : F) in 𝓝 ((↑f : E_1 → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F) ((↑f.symm : F → E_1) z) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E_1 → F) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)

Tactic:
have F : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ z - f a) (f.symm z) := by
    filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z
    simpa [hz] using h'z
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
rcases :
  ∀ (r : ℝ≥0∞) (r_pos : r > 0)
    (hr :
      Metric.eball ((↑f : E_1 → F_1) a) r ⊆
        {x : F_1 |
          (fun (z : F_1) ↦
              HasSum
                (fun (n : ℕ) ↦
                  (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
                ((↑f.symm : F_1 → E_1) z))
            x}),
    HasFPowerSeriesAt (↑f.symm : F_1 → E_1) (p.leftInv i a) ((↑f : E_1 → F_1) a)
⊢ HasFPowerSeriesAt (↑f.symm : F_1 → E_1) (p.leftInv i a) ((↑f : E_1 → F_1) a)

Tactic:
rcases EMetric.mem_nhds_iff.1 F with ⟨r, r_pos, hr⟩

Premises used: EMetric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
⊢ HasFPowerSeriesAt (↑f.symm : F_1 → E_1) (p.leftInv i a) ((↑f : E_1 → F_1) a)

Tactic:
⟨min r (p.leftInv i a).radius, min_le_right _ _,
    lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩

Premises used: lt_min, HasFPowerSeriesAt.radius_pos, FormalMultilinearSeries.radius, HasFPowerSeriesOnBall.mk, min_le_right, Exists.intro, FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos, HasFPowerSeriesAt, Min.min, FormalMultilinearSeries.leftInv
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
refine :
  ∀ {y : F_1} (hy : Membership.mem (γ := Set F_1) (Metric.eball 0 (min r (p.leftInv i a).radius)) y),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ y)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a + y))
⊢ HasFPowerSeriesAt (↑f.symm : F_1 → E_1) (p.leftInv i a) ((↑f : E_1 → F_1) a)

Tactic:
refine ⟨min r (p.leftInv i a).radius, min_le_right _ _,
    lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
y : F_1
hy : Membership.mem (γ := Set F_1) (Metric.eball 0 (min r (p.leftInv i a).radius)) y
simp : ∀ (hy : ‖y‖ₑ < r ∧ ‖y‖ₑ < (p.leftInv i a).radius), ‖y‖ₑ < r
⊢ y + (↑f : E_1 → F_1) a ∈ Metric.eball ((↑f : E_1 → F_1) a) r

Tactic:
simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
      add_sub_cancel_right] at hy ⊢

Premises used: edist_eq_enorm_sub, sub_zero, add_sub_cancel_right, lt_min_iff, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
y : F_1
hy : ‖y‖ₑ < r ∧ ‖y‖ₑ < (p.leftInv i a).radius
⊢ ‖y‖ₑ < r

Tactic:
hy.1

Premises used: And.left
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
y : F_1
hy : ‖y‖ₑ < r ∧ ‖y‖ₑ < (p.leftInv i a).radius
⊢ ‖y‖ₑ < r

Tactic:
exact hy.1

Premises used: And.left
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
y : F_1
hy : Membership.mem (γ := Set F_1) (Metric.eball 0 (min r (p.leftInv i a).radius)) y
⊢ y + (↑f : E_1 → F_1) a ∈ Metric.eball ((↑f : E_1 → F_1) a) r

Tactic:
have : y + f a ∈ Metric.eball (f a) r := by
    simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
      add_sub_cancel_right] at hy ⊢
    exact hy.1
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F_1 : Type u_3
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace 𝕜 F_1
f : OpenPartialHomeomorph E_1 F_1
a : E_1
i : E_1 ≃L[𝕜] F_1
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F_1
h : HasFPowerSeriesAt (↑f : E_1 → F_1) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F_1) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F_1) :
        (a : E_1 →L[𝕜] F_1) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F_1)
      (↑i : E_1 →L[𝕜] F_1))
A : HasFPowerSeriesAt ((↑f.symm : F_1 → E_1) ∘ (↑f : E_1 → F_1)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) (a + y) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F_1) y - (↑f : E_1 → F_1) a)
      y
E :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F_1) ((↑f.symm : F_1 → E_1) z) - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
F :
  ∀ᶠ (z : F_1) in 𝓝 ((↑f : E_1 → F_1) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
      ((↑f.symm : F_1 → E_1) z)
r : ℝ≥0∞
r_pos : r > 0
hr :
  Metric.eball ((↑f : E_1 → F_1) a) r ⊆
    {x : F_1 |
      (fun (z : F_1) ↦
          HasSum
            (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F_1) a)
            ((↑f.symm : F_1 → E_1) z))
        x}
y : F_1
hy : Membership.mem (γ := Set F_1) (Metric.eball 0 (min r (p.leftInv i a).radius)) y
this : y + (↑f : E_1 → F_1) a ∈ Metric.eball ((↑f : E_1 → F_1) a) r
⊢ HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F_1) → E_1) fun (x : Fin n) ↦ y)
    ((↑f.symm : F_1 → E_1) ((↑f : E_1 → F_1) a + y))

Tactic:
simpa [add_comm] using hr this

Premises used: add_comm
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : ℕ → E
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) 0 n • a n) (HPow.hPow (α := 𝕜) (β := ℕ) 0 0 • a 0)

Tactic:
hasSum_single (α := E) 0 fun b h ↦ _

Premises used: hasSum_single, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : ℕ → E
h : a 0 = HPow.hPow (α := 𝕜) (β := ℕ) 0 0 • a 0
convert_2 : ∀ (b : ℕ) (h : b ≠ 0), HPow.hPow (α := 𝕜) 0 b • a b = 0
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) 0 n • a n) (a 0)

Tactic:
convert! hasSum_single (α := E) 0 fun b h ↦ _

Premises used: hasSum_single, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : ℕ → E
⊢ a 0 = HPow.hPow (α := 𝕜) (β := ℕ) 0 0 • a 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ HPow.hPow (α := 𝕜) 0 b • a b = 0

Tactic:
simp [*]