awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (∃ (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 : (∃ (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
Tactic: tauto
-- 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
⊢ (∃ (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 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
Tactic: tauto
-- 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
⊢ (∃ (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 →
        ∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
Tactic: tauto
-- 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
⊢ (∃ (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 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
Tactic: tauto
-- 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
⊢ (∃ (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 mp₁₀ : (w : FormalMultilinearSeries 𝕜 E F) → (w_1 : E → F) → f =ᶠ[𝓝[insert x s] x] w_1 → HasFPowerSeriesAt w_1 w x → E → F
Tactic: tauto
-- 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
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have simp : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
  ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
Tactic: simp only [analyticWithinAt_iff_exists_analyticAt]
-- 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
⊢ (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1 : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) →
  ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
Tactic: refine ⟨?_, ?_⟩
-- 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
refine_1 :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) →
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
⊢ (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_2 : (∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) →
  ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x
Tactic: refine ⟨?_, ?_⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1 : ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}),
  ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
Tactic: rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1 : f x = g' x
Tactic: refine ⟨g', ?_, ?_, ?_⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
refine_1 : f x = g' x
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1₁ : EqOn f g' (insert x s)
Tactic: refine ⟨g', ?_, ?_, ?_⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
refine_1 : f x = g' x
refine_1₁ : EqOn f g' (insert x s)
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1₂ : AnalyticAt 𝕜 g' x
Tactic: refine ⟨g', ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
⊢ f x = g' x
have this : x ∈ u ∩ insert x s
Tactic: have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
y : E
hy : y ∈ insert x s
⊢ f y = g' y
have pos : ∀ (h'y : y ∈ u), f y = g' y
Tactic: by_cases h'y : y ∈ u
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
y : E
hy : y ∈ insert x s
pos : ∀ (h'y : y ∈ u), f y = g' y
⊢ f y = g' y
have neg : ∀ (h'y : y ∉ u), f y = g' y
Tactic: by_cases h'y : y ∈ u
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
y : E
hy : y ∈ insert x s
h'y : y ∈ u
⊢ f y = g' y
have this : y ∈ u ∩ insert x s
Tactic: have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
⊢ AnalyticAt 𝕜 g' x
have refine_1 : g =ᶠ[𝓝 x] g'
Tactic: apply hg.congr
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
⊢ g =ᶠ[𝓝 x] g'
have h : ∀ (a : E),
  Membership.mem (γ := Set E) {x : E | x ∈ u → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ g x = g' x) x} x} a
Tactic: filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
-- 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
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
h :
  ∀ (a : E),
    Membership.mem (γ := Set E) {x : E | x ∈ u → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ g x = g' x) x} x} a
⊢ g =ᶠ[𝓝 x] g'
have h₁ : ∀ a ∈ u, g a = g' a
Tactic: filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
-- 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
g : E → F
hf : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ f =ᶠ[𝓝[insert x s] x] g
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x_1 : E | x_1 ∈ insert x s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f x = g x) x} x_1} a
Tactic: filter_upwards [self_mem_nhdsWithin] using hf
-- 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
g : E → F
hf : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E | x_1 ∈ insert x s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f x = g x) x} x_1} a
⊢ f =ᶠ[𝓝[insert x s] x] g
have h₁ : ∀ a ∈ insert x s, f a = g a
Tactic: filter_upwards [self_mem_nhdsWithin] using hf
-- 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
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have simp : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
  ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
Tactic: classical
  simp only [analyticWithinAt_iff_exists_analyticAt]
  refine ⟨?_, ?_⟩
  · rintro ⟨g, hf, hg⟩
    rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
    let g' := Set.piecewise u g f
    refine ⟨g', ?_, ?_, ?_⟩
    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
      simpa [g', xu, this] using hu this
    · intro y hy
      by_cases h'y : y ∈ u
      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
        simpa [g', h'y, this] using hu this
      · simp [g', h'y]
    · apply hg.congr
      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
  · rintro ⟨g, -, hf, hg⟩
    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
-- 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
simp :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_1 : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) →
  ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
Tactic: classical
  simp only [analyticWithinAt_iff_exists_analyticAt]
  refine ⟨?_, ?_⟩
  · rintro ⟨g, hf, hg⟩
    rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
    let g' := Set.piecewise u g f
    refine ⟨g', ?_, ?_, ?_⟩
    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
      simpa [g', xu, this] using hu this
    · intro y hy
      by_cases h'y : y ∈ u
      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
        simpa [g', h'y, this] using hu this
      · simp [g', h'y]
    · apply hg.congr
      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
  · rintro ⟨g, -, hf, hg⟩
    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
-- 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
simp :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
refine_1 :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) →
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
have refine_2 : (∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) →
  ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x
Tactic: classical
  simp only [analyticWithinAt_iff_exists_analyticAt]
  refine ⟨?_, ?_⟩
  · rintro ⟨g, hf, hg⟩
    rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
    let g' := Set.piecewise u g f
    refine ⟨g', ?_, ?_, ?_⟩
    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
      simpa [g', xu, this] using hu this
    · intro y hy
      by_cases h'y : y ∈ u
      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
        simpa [g', h'y, this] using hu this
      · simp [g', h'y]
    · apply hg.congr
      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
  · rintro ⟨g, -, hf, hg⟩
    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩