awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F) (0 : F)
have psum_eq : p.partialSum (k + 1) = fun (y : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y
Tactic: have psum_eq : p.partialSum (k + 1) = fun y => p k fun _ => y := by
    funext z
    refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_
    · have := Finset.mem_range_succ_iff.mp hb
      simp only [hk b (this.lt_of_ne hnb)]
    · exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
psum_eq : p.partialSum (k + 1) = fun (y : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F) (0 : F)
have h₁ : Asymptotics.IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ 0 (x + y) - p.partialSum k.succ y) fun (y : E) ↦
  ‖y‖ ^ k.succ
Tactic: replace h := h.isBigO_sub_partialSum_pow k.succ
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
psum_eq : p.partialSum (k + 1) = fun (y : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y
h :
  Asymptotics.IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ 0 (x + y) - p.partialSum k.succ y)
    fun (y : E) ↦ ‖y‖ ^ k.succ
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F) (0 : F)
have h₁ : Asymptotics.IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0)
  (fun (x : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ x) fun (y : E) ↦ ‖y‖ ^ k.succ
Tactic: simp only [psum_eq, zero_sub, Pi.zero_apply, Asymptotics.isBigO_neg_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt.{u_1, u_1, u_2} (𝕜 := 𝕜) (F := E) 0 p x
⊢ p = 0
have h₁ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := E) ((p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1 : E)
    ((0 n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1 : E)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt.{u_1, u_1, u_2} (𝕜 := 𝕜) (F := E) 0 p x
n : ℕ
⊢ Eq.{u_2 + 1} (α := E) ((p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1 : E)
    ((0 n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1 : E)
have h₁ : Eq.{u_2 + 1} (α := E)
  (((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1) :
          ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) E) :
        (a : (i : Fin n) → 𝕜) → E)
      fun (x : Fin n) ↦ 1 :
    E)
  ((0 n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ 1 : E)
Tactic: rw [← mkPiRing_apply_one_eq_self (p n)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
main : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
⊢ EqOn f 0 U
have Uu : U ⊆ u
Tactic: have Uu : U ⊆ u :=
      hU.subset_of_closure_inter_subset isOpen_setOf_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
⊢ EqOn f 0 U
have suffices : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
Tactic: suffices main : closure u ∩ U ⊆ u by
    have Uu : U ⊆ u :=
      hU.subset_of_closure_inter_subset isOpen_setOf_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
    intro z hz
    simpa using mem_of_mem_nhds (Uu hz)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
⊢ x ∈ u
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r), x ∈ u
Tactic: rcases hf x xU with ⟨p, r, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ x ∈ u
have obtain : ∀ (y : E) (yu : y ∈ u) (hxy : edist x y < r / 2), x ∈ u
Tactic: obtain ⟨y, yu, hxy⟩ : ∃ y ∈ u, edist x y < r / 2 :=
    EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
have rwa : ∀ (hxy : edist y x < r / 2), (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
Tactic: rwa [edist_comm, edist_eq_enorm_sub] at hxy
Cleared hypotheses: hxy, q
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
rwa : ∀ (hxy : edist y x < r / 2), (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
have rwa₁ : ∀ (hxy : ‖y - x‖ₑ < r / 2), (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
Tactic: rwa [edist_comm, edist_eq_enorm_sub] at hxy
Cleared hypotheses: hxy, q
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
⊢ HasFPowerSeriesOnBall f q y (r / 2)
have A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
Tactic: have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
⊢ HasFPowerSeriesOnBall f q y (r / 2)
have this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) (r - (↑‖y - x‖₊ : ℝ≥0∞))
Tactic: have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ HasFPowerSeriesOnBall f q y (r / 2)
have this₁ : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
Tactic: simp only [add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ HasFPowerSeriesOnBall f q y (r / 2)
have apply : r / 2 ≤ r - (↑‖y - x‖₊ : ℝ≥0∞)
Tactic: apply this.mono (ENNReal.half_pos hp.r_pos.ne')
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ r / 2 ≤ r - (↑‖y - x‖₊ : ℝ≥0∞)
have apply : (↑‖y - x‖₊ : ℝ≥0∞) + r / 2 ≤ r
Tactic: apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
A : (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ (↑‖y - x‖₊ : ℝ≥0∞) + r / 2 ≤ r
have apply : r / 2 + r / 2 = r
Tactic: apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
⊢ x ∈ u
have has_series : HasFPowerSeriesOnBall f q y (r / 2)
Tactic: have has_series : HasFPowerSeriesOnBall f q y (r / 2) := by
    have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
    have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
    simp only [add_sub_cancel] at this
    apply this.mono (ENNReal.half_pos hp.r_pos.ne')
    apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top
    apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)
    exact ENNReal.add_halves _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
⊢ x ∈ u
have M : Metric.eball y (r / 2) ∈ 𝓝 x
Tactic: have M : Metric.eball y (r / 2) ∈ 𝓝 x := Metric.isOpen_eball.mem_nhds hxy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
⊢ x ∈ u
have h : ∀ (z : E) (hz : z ∈ Metric.eball y (r / 2)), f z = 0 z
Tactic: filter_upwards [M] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
⊢ f z = 0 z
have A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
Tactic: have A : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) (f z) := has_series.hasSum_sub hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
⊢ HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0
have this : HasFPowerSeriesAt 0 q y
Tactic: have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0
have h : Eq.{u_3 + 1} (α := ℕ → F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) fun (x : ℕ) ↦ 0
Tactic: convert! hasSum_zero (α := F) using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ Eq.{u_3 + 1} (α := ℕ → F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) fun (x : ℕ) ↦ 0
have h : ∀ (n : ℕ), Eq.{u_3 + 1} (α := F) ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y : F) (0 : F)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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
inst_5 : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x : E | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) (f z)
⊢ f z = 0 z
have B : HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z - y) 0
Tactic: have B : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) 0 := by
    have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
    convert! hasSum_zero (α := F) using 1
    ext n
    exact this.apply_eq_zero n _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (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 : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
⊢ EqOn f 0 U
have this : AnalyticOnNhd 𝕜 (F := F') ((⇑e : (a : F) → F') ∘ f) U
Tactic: have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)