awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun (i : Fin 0) ↦ 0
zero_mem : Membership.mem (γ := Set E) (Metric.eball 0 r) 0
this : ∀ (i : ℕ), i ≠ 0 → Eq.{u_3 + 1} (α := F) ((pf i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ 0 : F) (0 : F)
⊢ x + 0 ∈ insert x s

Tactic:
simp
-- 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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun (i : Fin 0) ↦ 0
zero_mem : Membership.mem (γ := Set E) (Metric.eball 0 r) 0
this : ∀ (i : ℕ), i ≠ 0 → Eq.{u_3 + 1} (α := F) ((pf i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ 0 : F) (0 : F)
⊢ f (x + 0) = (pf 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0

Tactic:
have A := (hf.hasSum (by simp) zero_mem).unique (hasSum_single _ this)
-- 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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun (i : Fin 0) ↦ 0
zero_mem : Membership.mem (γ := Set E) (Metric.eball 0 r) 0
this : ∀ (i : ℕ), i ≠ 0 → Eq.{u_3 + 1} (α := F) ((pf i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ 0 : F) (0 : F)
A : f (x + 0) = (pf 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
simpa [v_eq] using A.symm

Premises used: Eq.symm
-- 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
v : Fin 0 → E
rw : ∀ (hf : HasFPowerSeriesWithinOnBall f pf univ x r) (v : Fin 0 → E), (pf 0 : (a : (i : Fin 0) → E) → F) v = f x
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_univ
-- 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf univ x r
v : Fin 0 → E
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
hf.coeff_zero v

Premises used: HasFPowerSeriesWithinOnBall.coeff_zero
-- 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf univ x r
v : Fin 0 → E
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
exact hf.coeff_zero v

Premises used: HasFPowerSeriesWithinOnBall.coeff_zero
-- 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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
v : Fin 0 → E
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.coeff_zero v

Premises used: _private.0.HasFPowerSeriesWithinAt.eventually.match_1, HasFPowerSeriesWithinOnBall.coeff_zero, OfNat.ofNat, Eq, DFunLike.coe
-- 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
v : Fin 0 → E
⊢ (pf 0 : (a : (i : Fin 0) → E) → F) v = f x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.coeff_zero v

Premises used: HasFPowerSeriesOnBall.coeff_zero, _private.0.HasFPowerSeriesAt.radius_pos.match_1, OfNat.ofNat, Eq, DFunLike.coe
-- 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
⊢ Membership.mem (γ := Set E) ∅ x → AnalyticWithinAt 𝕜 f ∅ x

Tactic:
simp
-- 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
⊢ Membership.mem (γ := Set E) ∅ x → AnalyticAt 𝕜 f x

Tactic:
simp
-- 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
⊢ AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x

Tactic:
simp [AnalyticWithinAt, AnalyticAt]

Premises used: AnalyticWithinAt, 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
⊢ AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ

Tactic:
simp only [AnalyticOn, analyticWithinAt_univ, AnalyticOnNhd]

Premises used: AnalyticOn, AnalyticOnNhd, analyticWithinAt_univ
-- 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 t : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
h : t ⊆ s
obtain : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s x), AnalyticWithinAt 𝕜 f t x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
obtain ⟨p, hp⟩ := 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
s t : Set E
x : E
h : t ⊆ s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
⟨p, hp.mono h⟩

Premises used: HasFPowerSeriesWithinAt.mono, 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
s t : Set E
x : E
h : t ⊆ s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
exact ⟨p, hp.mono 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
s : Set E
x : E
hf : AnalyticAt 𝕜 f x
⊢ AnalyticWithinAt 𝕜 f univ x

Tactic:
rw [← analyticWithinAt_univ] at hf

Premises used: analyticWithinAt_univ
-- 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
x : E
hf : AnalyticWithinAt 𝕜 f univ x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
apply hf.mono (subset_univ _)

Premises used: Set.subset_univ, AnalyticWithinAt.mono
-- 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
⊢ AnalyticOn 𝕜 f s

Tactic:
fun x hx ↦ (hf x hx).analyticWithinAt

Premises used: AnalyticOn, AnalyticAt.analyticWithinAt
-- 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 g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s x), AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
rcases hf with ⟨p, hp⟩
-- 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 g : E → F
s : Set E
x : E
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
⟨p, hp.congr hs hx⟩

Premises used: AnalyticWithinAt, HasFPowerSeriesWithinAt.congr, 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 g : E → F
s : Set E
x : E
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
exact ⟨p, hp.congr hs 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 g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[insert x s] x] f
apply : g x = f x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs)

Premises used: AnalyticWithinAt.congr_of_eventuallyEq, Set.subset_insert, nhdsWithin_mono
-- 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 g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[insert x s] x] f
⊢ g x = f x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s) hs

Premises used: mem_of_mem_nhdsWithin, Set.mem_insert
-- 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 g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : EqOn g f s
hx : g x = f x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx

Premises used: Set.EqOn.eventuallyEq_nhdsWithin, AnalyticWithinAt.congr_of_eventuallyEq
-- 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 g : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
hs : EqOn g f s
⊢ AnalyticOn 𝕜 g s

Tactic:
fun x m ↦ (hf x m).congr hs (hs m)

Premises used: AnalyticOn, AnalyticWithinAt.congr
-- 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 g : E → F
s : Set E
hs : EqOn f g s
⊢ AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s

Tactic:
⟨fun h ↦ h.congr hs.symm, fun h ↦ h.congr hs⟩

Premises used: AnalyticOn.congr, Iff.intro, Set.EqOn.symm
-- 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 g : E → F
x : E
hf : AnalyticAt 𝕜 f x
hg : f =ᶠ[𝓝 x] g
⊢ AnalyticAt 𝕜 g x

Tactic:
let ⟨_, hpf⟩ := hf
  (hpf.congr hg).analyticAt

Premises used: HasFPowerSeriesAt.congr, AnalyticAt, _private.0.AnalyticAt.congr.match_1, 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 g : E → F
x : E
h : f =ᶠ[𝓝 x] g
⊢ AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x

Tactic:
⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

Premises used: Iff.intro, AnalyticAt.congr, Filter.EventuallyEq.symm
-- 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 t : Set E
hf : AnalyticOnNhd 𝕜 f t
hst : s ⊆ t
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
fun z hz => hf z (hst hz)

Premises used: AnalyticOnNhd
-- 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 g : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : f =ᶠ[𝓝ˢ s] g
⊢ AnalyticOnNhd 𝕜 g s

Tactic:
fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)

Premises used: AnalyticOnNhd, mem_nhdsSet_iff_forall, Iff.mp, AnalyticAt.congr
-- 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 g : E → F
s : Set E
h : f =ᶠ[𝓝ˢ s] g
⊢ AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s

Tactic:
⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩

Premises used: Iff.intro, Filter.EventuallyEq.symm, AnalyticOnNhd.congr'
-- 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 g : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOnNhd 𝕜 f s
hg : EqOn f g s
⊢ AnalyticOnNhd 𝕜 g s

Tactic:
hf.congr' <| mem_nhdsSet_iff_forall.mpr
    (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)

Premises used: Iff.mpr, mem_nhdsSet_iff_forall, And.intro, IsOpen.mem_nhds, Exists.intro, Filter.eventuallyEq_iff_exists_mem, AnalyticOnNhd.congr'
-- 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 g : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : EqOn f g s
⊢ AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s

Tactic:
⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩

Premises used: AnalyticOnNhd.congr, Iff.intro, Set.EqOn.symm
-- 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 t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s ∈ 𝓝[t] x
rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s x), AnalyticWithinAt 𝕜 f t x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
rcases h with ⟨p, hp⟩
-- 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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
⟨p, hp.mono_of_mem_nhdsWithin hst⟩

Premises used: AnalyticWithinAt, HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin, 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
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
exact ⟨p, hp.mono_of_mem_nhdsWithin hst⟩
-- 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 t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
h.mono_of_mem_nhdsWithin ?_

Premises used: AnalyticWithinAt.mono_of_mem_nhdsWithin
-- 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 t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
refine : s ∈ 𝓝[t] x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
refine h.mono_of_mem_nhdsWithin ?_

Premises used: AnalyticWithinAt.mono_of_mem_nhdsWithin
-- 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 t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ s ∈ 𝓝[t] x

Tactic:
simp [← nhdsWithin_eq_iff_eventuallyEq.mpr hst, self_mem_nhdsWithin]

Premises used: Iff.mpr, nhdsWithin_eq_iff_eventuallyEq, self_mem_nhdsWithin
-- 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 t : Set E
h : AnalyticOn 𝕜 f t
hs : s ⊆ t
⊢ AnalyticOn 𝕜 f s

Tactic:
fun _ m ↦ (h _ (hs m)).mono hs

Premises used: AnalyticOn, AnalyticWithinAt.mono
-- 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
x y : E
⊢ AnalyticWithinAt 𝕜 f (insert y s) x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
simp [AnalyticWithinAt]

Premises used: AnalyticWithinAt
-- 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
z : E
s : Set E
hU : s ∈ 𝓝 z
h : AnalyticOn 𝕜 f s
obtain : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s z), AnalyticAt 𝕜 f z
⊢ AnalyticAt 𝕜 f z

Tactic:
obtain ⟨p, hp⟩ := h z (mem_of_mem_nhds hU)

Premises used: mem_of_mem_nhds
-- 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
z : E
s : Set E
hU : s ∈ 𝓝 z
h : AnalyticOn 𝕜 f s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s z
⊢ AnalyticAt 𝕜 f z

Tactic:
⟨p, hasFPowerSeriesWithinAt_iff_of_nhds f p hU |>.mp hp⟩

Premises used: hasFPowerSeriesWithinAt_iff_of_nhds, AnalyticAt, Exists.intro, Iff.mp
-- 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
z : E
s : Set E
hU : s ∈ 𝓝 z
h : AnalyticOn 𝕜 f s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s z
⊢ AnalyticAt 𝕜 f z

Tactic:
exact ⟨p, hasFPowerSeriesWithinAt_iff_of_nhds f p hU |>.mp hp⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := G)
    (fun (n : ℕ) ↦ (g.compFormalMultilinearSeries p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y)
    (((⇑g : (a : F) → G) ∘ f) (x + y))

Tactic:
simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using
      g.hasSum (h.hasSum hy h'y)

Premises used: ContinuousLinearMap.hasSum, ContinuousLinearMap.compFormalMultilinearSeries_apply, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesOnBall f p x r
rw :
  ∀ (h : HasFPowerSeriesWithinOnBall f p univ x r),
    HasFPowerSeriesWithinOnBall ((⇑g : (a : F) → G) ∘ f) (g.compFormalMultilinearSeries p) univ x r
⊢ HasFPowerSeriesOnBall ((⇑g : (a : F) → G) ∘ f) (g.compFormalMultilinearSeries p) x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall ((⇑g : (a : F) → G) ∘ f) (g.compFormalMultilinearSeries p) univ x r

Tactic:
g.comp_hasFPowerSeriesWithinOnBall h

Premises used: ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall ((⇑g : (a : F) → G) ∘ f) (g.compFormalMultilinearSeries p) univ x r

Tactic:
exact g.comp_hasFPowerSeriesWithinOnBall h

Premises used: ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall