awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
refine : ∃ᶠ (x : 𝕜) in 𝓝 0, x ≠ 0
⊢ False

Tactic:
refine isLittleO_irrefl (.mono ?_ fun _ ↦ pow_ne_zero n) this

Premises used: Asymptotics.isLittleO_irrefl, Filter.Frequently.mono
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
⊢ ∃ᶠ (x : 𝕜) in 𝓝 0, x ≠ 0

Tactic:
Filter.frequently_iff_neBot.2 <| inferInstanceAs (𝓝[≠] (0 : 𝕜)).NeBot

Premises used: Iff.mpr, _private.0.Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero._proof_1, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
⊢ ∃ᶠ (x : 𝕜) in 𝓝 0, x ≠ 0

Tactic:
exact Filter.frequently_iff_neBot.2 <| inferInstanceAs (𝓝[≠] (0 : 𝕜)).NeBot

Premises used: Iff.mpr, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 : ℕ
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)

Tactic:
Nat.strong_induction_on n fun k hk => ?_

Premises used: Nat.strong_induction_on
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 : ℕ
refine :
  ∀ (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)
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)

Tactic:
refine Nat.strong_induction_on n fun k hk => ?_
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
h₁ : ∀ (z : E), p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z
⊢ p.partialSum (k + 1) = fun (y : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y

Tactic:
funext z
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
⊢ p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z

Tactic:
Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_

Premises used: FormalMultilinearSeries.partialSum, Finset.sum_eq_single
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
h₁ :
  ∀ (b : ℕ) (hb : b ∈ Finset.range (k + 1)) (hnb : b ≠ k),
    Eq.{u_3 + 1} (α := F) ((p b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ z : F) (0 : F)
h₂ :
  ∀ (hn : k ∉ Finset.range (k + 1)),
    Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z : F) (0 : F)
⊢ p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z

Tactic:
refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ b ≤ k

Tactic:
have := Finset.mem_range_succ_iff.mp hb
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
this : b ≤ k
⊢ Eq.{u_3 + 1} (α := F) ((p b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ z : F) (0 : F)

Tactic:
simp only [hk b (this.lt_of_ne hnb)]

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
hn : k ∉ Finset.range (k + 1)
⊢ Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z : F) (0 : F)

Tactic:
False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))

Premises used: Iff.mpr, lt_add_one, False.elim, Finset.mem_range
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
z : E
hn : k ∉ Finset.range (k + 1)
⊢ Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z : F) (0 : F)

Tactic:
exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))

Premises used: Iff.mpr, lt_add_one, False.elim, Finset.mem_range
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
⊢ 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)))
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
⊢ 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
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
⊢ 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

Premises used: Asymptotics.isBigO_neg_left, Pi.zero_apply, zero_sub
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 (x : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ x) 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)

Tactic:
h.continuousMultilinearMap_apply_eq_zero

Premises used: Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 (x : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ x) 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)

Tactic:
exact h.continuousMultilinearMap_apply_eq_zero

Premises used: Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
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)
⊢ p = 0

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 : ℕ
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)
⊢ 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:
rw [← mkPiRing_apply_one_eq_self (p n)]

Premises used: ContinuousMultilinearMap.mkPiRing_apply_one_eq_self
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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)
    (((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:
simp [h.apply_eq_zero n 1]

Premises used: HasFPowerSeriesAt.apply_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : HasFPowerSeriesAt (𝕜 := 𝕜) f p₁ x
h₂ : HasFPowerSeriesAt (𝕜 := 𝕜) f p₂ x
⊢ HasFPowerSeriesAt.{u_1, u_1, u_2} (𝕜 := 𝕜) (F := E) 0 (p₁ - p₂) x

Tactic:
simpa only [sub_self] using h₁.sub h₂

Premises used: sub_self, HasFPowerSeriesAt.sub
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
x : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p x
hq : HasFPowerSeriesAt (𝕜 := 𝕜) g q x
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = g z
⊢ p = q

Tactic:
(hp.congr heq).eq_formalMultilinearSeries hq

Premises used: HasFPowerSeriesAt.congr, HasFPowerSeriesAt.eq_formalMultilinearSeries
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
x : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p x
hf : f =ᶠ[𝓝 x] 0
⊢ p = 0

Tactic:
(hp.congr hf).eq_zero

Premises used: HasFPowerSeriesAt.congr, HasFPowerSeriesAt.eq_zero
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
r₁ r₂ : ℝ≥0∞
x : 𝕜
h₁ : HasFPowerSeriesOnBall (𝕜 := 𝕜) f p₁ x r₁
h₂ : HasFPowerSeriesOnBall (𝕜 := 𝕜) f p₂ x r₂
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p₁ x r₂

Tactic:
h₂.hasFPowerSeriesAt.eq_formalMultilinearSeries h₁.hasFPowerSeriesAt ▸ h₂

Premises used: Eq.rec, HasFPowerSeriesAt.eq_formalMultilinearSeries, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
r : ℝ≥0∞
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
h : HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x r
h' : ∀ (r' : ℝ≥0), 0 < r' → ∃ (p' : FormalMultilinearSeries 𝕜 𝕜 E), HasFPowerSeriesOnBall (𝕜 := 𝕜) f p' x (↑r' : ℝ≥0∞)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f p x ∞

Tactic:
{ r_le := ENNReal.le_of_forall_pos_nnreal_lt fun r hr _ =>
      let ⟨_, hp'⟩ := h' r hr
      (h.exchange_radius hp').r_le
    r_pos := ENNReal.coe_lt_top
    hasSum := fun {y} _ =>
      let ⟨r', hr'⟩ := exists_gt ‖y‖₊
      let ⟨_, hp'⟩ := h' r' hr'.ne_bot.bot_lt
      (h.exchange_radius hp').hasSum <| mem_eball_zero_iff.mpr (ENNReal.coe_lt_coe.2 hr') }

Premises used: ENNReal.le_of_forall_pos_nnreal_lt, Iff.mpr, ENNReal.ofNNReal, NNNorm.nnnorm, _private.0.HasFPowerSeriesOnBall.r_eq_top_of_exists.match_1, ENNReal.coe_lt_coe, HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.hasSum, NoMaxOrder.exists_gt, LE.le, FormalMultilinearSeries.radius, HAdd.hAdd, HasSum, HasFPowerSeriesOnBall.mk, Nat, mem_eball_zero_iff, DFunLike.coe, Ne.bot_lt, SummationFilter.unconditional, LT.lt.ne_bot, HasFPowerSeriesOnBall.exchange_radius, ENNReal.coe_lt_top, _private.0.HasFPowerSeriesOnBall.r_eq_top_of_exists.match_2
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
⊢ U ⊆ u

Tactic:
have Uu : U ⊆ u :=
      hU.subset_of_closure_inter_subset isOpen_setOf_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
Uu : U ⊆ u
z : E
hz : z ∈ U
⊢ f z = 0 z

Tactic:
simpa using mem_of_mem_nhds (Uu hz)

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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}
suffices : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
⊢ EqOn f 0 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)
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r), x ∈ u
⊢ x ∈ u

Tactic:
rcases hf x xU with ⟨p, r, hp⟩
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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 ∈ u, edist x y < r / 2

Tactic:
EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')

Premises used: HDiv.hDiv, LT.lt.ne', ENNReal.half_pos, Iff.mp, EMetric.mem_closure_iff, OfNat.ofNat, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
obtain : ∀ (y : E) (yu : y ∈ u) (hxy : edist x y < r / 2), x ∈ u
⊢ 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')

Premises used: HDiv.hDiv, LT.lt.ne', ENNReal.half_pos, Iff.mp, EMetric.mem_closure_iff, OfNat.ofNat, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hxy : ‖y - x‖ₑ < r / 2), (↑‖y - x‖₊ : ℝ≥0∞) < r / 2
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r / 2

Tactic:
rwa [edist_comm, edist_eq_enorm_sub] at hxy

Premises used: edist_eq_enorm_sub, PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Analysis.Analytic.Uniqueness
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

Tactic:
have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy