-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
mp :
  (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) →
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
mpr :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x) →
    ∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
mp₁ mp₂ mp₃ :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (w_1 : E → F),
    f =ᶠ[𝓝[insert x s] x] w_1 →
      HasFPowerSeriesAt w_1 w x →
        ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
mpr₁ mpr₂ mpr₃ :
  ∀ (w : E → F),
    f =ᶠ[𝓝[insert x s] x] w →
      ∀ (w_1 : FormalMultilinearSeries 𝕜 E F),
        HasFPowerSeriesAt w w_1 x →
          ∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
mp₄ mp₅ mp₆ :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (w_1 : E → F),
    f =ᶠ[𝓝[insert x s] x] w_1 →
      HasFPowerSeriesAt w_1 w x →
        ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
mpr₄ mpr₅ mpr₆ :
  ∀ (w : E → F),
    f =ᶠ[𝓝[insert x s] x] w →
      ∀ (w_1 : FormalMultilinearSeries 𝕜 E F),
        HasFPowerSeriesAt w w_1 x →
          ∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
mp₇ mp₈ :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (w_1 : E → F),
    f =ᶠ[𝓝[insert x s] x] w_1 →
      HasFPowerSeriesAt w_1 w x →
        ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
mp₉ :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (w_1 : E → F),
    f =ᶠ[𝓝[insert x s] x] w_1 →
      HasFPowerSeriesAt w_1 w x →
        f =ᶠ[𝓝[insert x s] x] w_1 ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt w_1 p x
mp₁₀ :
  (w : FormalMultilinearSeries 𝕜 E F) → (w_1 : E → F) → f =ᶠ[𝓝[insert x s] x] w_1 → HasFPowerSeriesAt w_1 w x → E → F
mp₁₁ :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (w_1 : E → F),
    f =ᶠ[𝓝[insert x s] x] w_1 →
      HasFPowerSeriesAt w_1 w x →
        f =ᶠ[𝓝[insert x s] x] w_1 ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt w_1 p x
mp₁₂ :
  (w : FormalMultilinearSeries 𝕜 E F) → (w_1 : E → F) → f =ᶠ[𝓝[insert x s] x] w_1 → HasFPowerSeriesAt w_1 w x → E → F
mpr₇ mpr₈ :
  ∀ (w : E → F),
    f =ᶠ[𝓝[insert x s] x] w →
      ∀ (w_1 : FormalMultilinearSeries 𝕜 E F),
        HasFPowerSeriesAt w w_1 x →
          ∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
mpr₉ :
  ∀ (w : E → F),
    f =ᶠ[𝓝[insert x s] x] w →
      ∀ (w_1 : FormalMultilinearSeries 𝕜 E F),
        HasFPowerSeriesAt w w_1 x → ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g w_1 x
⊢ (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
have mpr₁₀ : (w : E → F) →
  f =ᶠ[𝓝[insert x s] x] w →
    (w_1 : FormalMultilinearSeries 𝕜 E F) → HasFPowerSeriesAt w w_1 x → FormalMultilinearSeries 𝕜 E F
Tactic: tauto