awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Within
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
⊢ x ∈ insert x s

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Within
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
⊢ x ∈ u ∩ insert x s

Tactic:
have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
-- Module: Mathlib.Analysis.Analytic.Within
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
this : x ∈ u ∩ insert x s
⊢ f x = g' x

Tactic:
simpa [g', xu, this] using hu this
-- Module: Mathlib.Analysis.Analytic.Within
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
neg : ∀ (h'y : y ∉ u), f y = g' y
⊢ f y = g' y

Tactic:
by_cases h'y : y ∈ u
-- Module: Mathlib.Analysis.Analytic.Within
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
⊢ y ∈ u ∩ insert x s

Tactic:
have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
-- Module: Mathlib.Analysis.Analytic.Within
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
this : y ∈ u ∩ insert x s
⊢ f y = g' y

Tactic:
simpa [g', h'y, this] using hu this
-- Module: Mathlib.Analysis.Analytic.Within
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

Tactic:
simp [g', h'y]
-- Module: Mathlib.Analysis.Analytic.Within
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 : g =ᶠ[𝓝 x] g'
⊢ AnalyticAt 𝕜 g' x

Tactic:
apply hg.congr

Premises used: AnalyticAt.congr
-- Module: Mathlib.Analysis.Analytic.Within
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 ∈ u
⊢ g y = g' y

Tactic:
simp [g', hy]
-- Module: Mathlib.Analysis.Analytic.Within
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
h₁ h₂ : ∀ (y : E) (hy : y ∈ u), g y = g' y
⊢ g =ᶠ[𝓝 x] g'

Tactic:
filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Within
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
⊢ ∀ a ∈ insert x s, f a = g a

Tactic:
hf

Premises used: Set.EqOn
-- Module: Mathlib.Analysis.Analytic.Within
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
h₁ : ∀ a ∈ insert x s, f a = g a
⊢ f =ᶠ[𝓝[insert x s] x] g

Tactic:
filter_upwards [self_mem_nhdsWithin] using hf

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Analytic.Within
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
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
-- Module: Mathlib.Analysis.Analytic.Within
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
refine_2 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
⊢ AnalyticWithinAt 𝕜 f s 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⟩

Premises used: analyticWithinAt_iff_exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
h.exists_analyticAt

Premises used: AnalyticWithinAt.exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
obtain : ∀ (g : E → F) (h'g : EqOn f g (insert x s)) (hg : AnalyticAt 𝕜 g x), ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
obtain ⟨g, -, h'g, hg⟩ : ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x :=
    h.exists_analyticAt

Premises used: AnalyticWithinAt.exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
⟨u, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
refine_1 : u ∈ 𝓝[insert x s] x
refine_2 : AnalyticOn 𝕜 f u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
refine ⟨u, ?_, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
⊢ u ∈ 𝓝[insert x s] x

Tactic:
inter_mem_nhdsWithin _ ((isOpen_analyticAt 𝕜 g).mem_nhds hg)

Premises used: inter_mem_nhdsWithin, Set.Mem, setOf, IsOpen.mem_nhds, isOpen_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
⊢ u ∈ 𝓝[insert x s] x

Tactic:
exact inter_mem_nhdsWithin _ ((isOpen_analyticAt 𝕜 g).mem_nhds hg)

Premises used: inter_mem_nhdsWithin, IsOpen.mem_nhds, isOpen_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
⊢ AnalyticWithinAt 𝕜 g u y

Tactic:
have : AnalyticWithinAt 𝕜 g u y := hy.2.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
this : AnalyticWithinAt 𝕜 g u y
⊢ AnalyticWithinAt 𝕜 f u y

Tactic:
this.congr (h'g.mono (inter_subset_left)) (h'g (inter_subset_left hy))

Premises used: Set.inter_subset_left, AnalyticWithinAt.congr, Set.EqOn.mono
-- Module: Mathlib.Analysis.Analytic.Within
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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
this : AnalyticWithinAt 𝕜 g u y
⊢ AnalyticWithinAt 𝕜 f u y

Tactic:
exact this.congr (h'g.mono (inter_subset_left)) (h'g (inter_subset_left hy))

Premises used: Set.inter_subset_left, AnalyticWithinAt.congr, Set.EqOn.mono
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
obtain :
  ∀ (g : E → F) (hfg : f =ᶠ[𝓝[insert x s] x] g) (hga : AnalyticAt 𝕜 g x), ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y
⊢ ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y

Tactic:
obtain ⟨g, hfg, hga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf

Premises used: Iff.mp, analyticWithinAt_iff_exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hfg : f =ᶠ[𝓝[insert x s] x] g
hga : AnalyticAt 𝕜 g x
simp :
  ∀ (hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1), ∀ᶠ (x : E) in 𝓝 x, x ∈ s → AnalyticWithinAt 𝕜 f s x
⊢ ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y

Tactic:
simp only [Filter.EventuallyEq, eventually_nhdsWithin_iff] at hfg ⊢

Premises used: Filter.EventuallyEq, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
h :
  ∀ (z : E) (hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1) (hgaz : AnalyticAt 𝕜 g z) (hz : z ∈ s),
    AnalyticWithinAt 𝕜 f s z
⊢ ∀ᶠ (x : E) in 𝓝 x, x ∈ s → AnalyticWithinAt 𝕜 f s x

Tactic:
filter_upwards [hfg.eventually_nhds, hga.eventually_analyticAt] with z hfgz hgaz hz

Premises used: Filter.Eventually.eventually_nhds, AnalyticAt.eventually_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
z : E
hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1
hgaz : AnalyticAt 𝕜 g z
hz : z ∈ s
⊢ AnalyticWithinAt 𝕜 f s z

Tactic:
analyticWithinAt_iff_exists_analyticAt.mpr ⟨g, ?_, hgaz⟩

Premises used: Iff.mpr, And.intro, Exists.intro, analyticWithinAt_iff_exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
z : E
hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1
hgaz : AnalyticAt 𝕜 g z
hz : z ∈ s
h : f =ᶠ[𝓝[insert z s] z] g
⊢ AnalyticWithinAt 𝕜 f s z

Tactic:
refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨g, ?_, hgaz⟩

Premises used: Iff.mpr, And.intro, Exists.intro, analyticWithinAt_iff_exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
z : E
hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1
hgaz : AnalyticAt 𝕜 g z
hz : z ∈ s
⊢ insert z s ⊆ insert x s

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Analytic.Within
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
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
z : E
hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1
hgaz : AnalyticAt 𝕜 g z
hz : z ∈ s
⊢ f =ᶠ[𝓝[insert z s] z] g

Tactic:
exact (eventually_nhdsWithin_iff.mpr hfgz).filter_mono <| nhdsWithin_mono _ (by simp [hz])

Premises used: Iff.mpr, Filter.Eventually.filter_mono, eventually_nhdsWithin_iff, nhdsWithin_mono
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
⊢ x ∈ (↑D : Set X) ↔ x ∈ D

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
⊢ x ∈ D.carrier ↔ x ∈ D

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, Delone.DeloneSet.toSet
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : Nonempty X
D : DeloneSet X
⊢ (↑D : Set X).Nonempty

Tactic:
D.isCover_coveringRadius.nonempty Set.univ_nonempty

Premises used: Delone.DeloneSet.isCover_coveringRadius, Set.univ_nonempty, Delone.DeloneSet.toSet, Metric.IsCover.nonempty
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < packingRadius

Tactic:
simpa [h_packing] using D.packingRadius_pos

Premises used: Delone.DeloneSet.packingRadius_pos
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsSeparated (↑packingRadius : ENNReal) carrier

Tactic:
simpa [h_carrier, h_packing] using D.isSeparated_packingRadius

Premises used: Delone.DeloneSet.isSeparated_packingRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < coveringRadius

Tactic:
simpa [h_covering] using D.coveringRadius_pos

Premises used: Delone.DeloneSet.coveringRadius_pos
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsCover coveringRadius Set.univ carrier

Tactic:
simpa [h_carrier, h_covering] using D.isCover_coveringRadius

Premises used: Delone.DeloneSet.isCover_coveringRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ D.copy carrier packingRadius coveringRadius h_carrier h_packing h_covering = D

Tactic:
DeloneSet.ext h_carrier h_packing h_covering

Premises used: Delone.DeloneSet.ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ENNReal.ofReal (↑D.packingRadius : ℝ) < ENNReal.ofReal (dist x y)

Tactic:
simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne

Premises used: edist_dist, Delone.DeloneSet.isSeparated_packingRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ENNReal.ofReal (↑D.packingRadius : ℝ) < ENNReal.ofReal (dist x y)

Tactic:
have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
hsep : ENNReal.ofReal (↑D.packingRadius : ℝ) < ENNReal.ofReal (dist x y)
⊢ (↑D.packingRadius : ℝ) < dist x y

Tactic:
(ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep

Premises used: Iff.mpr, dist_pos, Iff.mp, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
hsep : ENNReal.ofReal (↑D.packingRadius : ℝ) < ENNReal.ofReal (dist x y)
⊢ (↑D.packingRadius : ℝ) < dist x y

Tactic:
exact (ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep

Premises used: Iff.mpr, dist_pos, Iff.mp, ENNReal.ofReal_lt_ofReal_iff