awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
C :
  ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
⊢ ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) a)),
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a) y
have simp : ∀ᶠ (y : E) in 𝓝 a,
  HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
    y
Tactic: simp only [h0, OpenPartialHomeomorph.left_inv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
C :
  ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
⊢ ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a) y
have h₁ : ∀ (x : E)
  (hx :
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) x)))
  (h'x : x ∈ f.source),
  HasSum
    (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a) x
Tactic: filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
C :
  ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
⊢ HasFPowerSeriesAt (↑f.symm : F → E) (p.leftInv i a) ((↑f : E → F) a)
have D : ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) a)),
  HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
    y
Tactic: have D : ∀ᶠ (y : E) in 𝓝 (f.symm (f a)),
      HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a) y := by
    simp only [h0, OpenPartialHomeomorph.left_inv]
    filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x
    simpa [h'x] using hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
C :
  ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) a)),
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a) y
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦
          (↑f : E → F) ((↑f.symm : F → E) z) - (↑f : E → F) a)
      ((↑f.symm : F → E) z)
have this : ContinuousAt (↑f.symm : F → E) ((↑f : E → F) a)
Tactic: have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
C :
  ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) a)),
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a) y
⊢ HasFPowerSeriesAt (↑f.symm : F → E) (p.leftInv i a) ((↑f : E → F) a)
have E₁ : ∀ᶠ (z : F) in 𝓝 ((↑f : E → F) a),
  HasSum
    (fun (n : ℕ) ↦
      (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦
        (↑f : E → F) ((↑f.symm : F → E) z) - (↑f : E → F) a)
    ((↑f.symm : F → E) z)
Tactic: have E : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (f.symm z) - f a)
      (f.symm z) := by
    have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)
    exact this D
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
have h₁ : ∀ (z : F) (hz : z ∈ f.target)
  (h'z :
    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)),
  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: filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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)
⊢ HasFPowerSeriesAt (↑f.symm : F → E_1) (p.leftInv i a) ((↑f : E_1 → F) a)
have F₁ : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ HasFPowerSeriesAt (↑f.symm : F_1 → E_1) (p.leftInv i a) ((↑f : E_1 → F_1) a)
have 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)
Tactic: rcases EMetric.mem_nhds_iff.1 F with ⟨r, r_pos, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
have 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))
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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
have simp : ∀ (hy : ‖y‖ₑ < r ∧ ‖y‖ₑ < (p.leftInv i a).radius), ‖y‖ₑ < r
Tactic: simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
      add_sub_cancel_right] at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
⊢ 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))
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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) (a 0)
have h : a 0 = HPow.hPow (α := 𝕜) (β := ℕ) 0 0 • a 0
Tactic: convert! hasSum_single (α := E) 0 fun b h ↦ _