awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
pos : MeromorphicNFAt (toMeromorphicNFAt f z) z
⊢ MeromorphicNFAt (toMeromorphicNFOn f U) z

Tactic:
rw [meromorphicNFAt_congr (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hz)]

Premises used: toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds, meromorphicNFAt_congr
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (toMeromorphicNFAt f z) z

Tactic:
meromorphicNFAt_toMeromorphicNFAt

Premises used: meromorphicNFAt_toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (toMeromorphicNFAt f z) z

Tactic:
exact meromorphicNFAt_toMeromorphicNFAt

Premises used: meromorphicNFAt_toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

Tactic:
simpa [hf] using analyticOnNhd_const.meromorphicNFOn

Premises used: analyticOnNhd_const, AnalyticOnNhd.meromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
mp : toMeromorphicNFOn f U = f → MeromorphicNFOn f U
mpr : MeromorphicNFOn f U → toMeromorphicNFOn f U = f
⊢ toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : toMeromorphicNFOn f U = f
mp : MeromorphicNFOn (toMeromorphicNFOn f U) U
⊢ MeromorphicNFOn f U

Tactic:
rw [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : toMeromorphicNFOn f U = f
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

Tactic:
apply meromorphicNFOn_toMeromorphicNFOn

Premises used: meromorphicNFOn_toMeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
mpr : ∀ (x : 𝕜), toMeromorphicNFOn f U x = f x
⊢ toMeromorphicNFOn f U = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
pos : ∀ (hx : x ∈ U), toMeromorphicNFOn f U x = f x
neg : ∀ (hx : x ∉ U), toMeromorphicNFOn f U x = f x
⊢ toMeromorphicNFOn f U x = f x

Tactic:
by_cases hx : x ∈ U
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
pos : toMeromorphicNFAt f x x = f x
⊢ toMeromorphicNFOn f U x = f x

Tactic:
simp only [toMeromorphicNFOn, h.meromorphicOn, ↓reduceDIte, hx]

Premises used: reduceDIte, MeromorphicNFOn.meromorphicOn, toMeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
pos pos₁ : f x = f x
⊢ toMeromorphicNFAt f x x = f x

Tactic:
rw [toMeromorphicNFAt_eq_self.2 (h hx)]

Premises used: Iff.mpr, toMeromorphicNFAt_eq_self
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∉ U
⊢ toMeromorphicNFOn f U x = f x

Tactic:
simp [toMeromorphicNFOn, h.meromorphicOn, hx]

Premises used: MeromorphicNFOn.meromorphicOn, toMeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
hf₁₂ : toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f
⊢ meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x

Tactic:
apply meromorphicOrderAt_congr

Premises used: meromorphicOrderAt_congr
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f

Tactic:
hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx

Premises used: MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f

Tactic:
exact hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx

Premises used: MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (toMeromorphicNFOn f U) U) (divisor f U)

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
neg :
  ∀ (hz : z ∉ U),
    Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
by_cases hz : z ∈ U
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]

Premises used: meromorphicNFOn_toMeromorphicNFOn, MeromorphicNFOn.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∉ U
⊢ Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]

Premises used: meromorphicNFOn_toMeromorphicNFOn, MeromorphicNFOn.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = 0

Tactic:
dif_neg hf

Premises used: meromorphicOrderAt, dif_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : meromorphicOrderAt f x ≠ 0
contrapose : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f x = 0
⊢ MeromorphicAt f x

Tactic:
contrapose hf
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = 0

Tactic:
simp [hf]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
by_cases hf : MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ¬MeromorphicAt f x
neg : ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [hf, not_false_eq_true, meromorphicOrderAt_of_not_meromorphicAt, WithTop.zero_ne_top,
      false_iff]

Premises used: false_iff, WithTop.zero_ne_top, meromorphicOrderAt_of_not_meromorphicAt, not_false_eq_true
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ¬MeromorphicAt f x
neg : ∀ (hf : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), MeromorphicAt f x
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
contrapose hf
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ MeromorphicAt f x

Tactic:
(MeromorphicAt.const 0 x).congr (EventuallyEq.symm hf)

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ MeromorphicAt f x

Tactic:
exact (MeromorphicAt.const 0 x).congr (EventuallyEq.symm hf)

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
pos :
  analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
            f z)
        x =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [meromorphicOrderAt, hf, ↓reduceDIte, sub_eq_top_iff, ENat.map_eq_top_iff,
    WithTop.natCast_ne_top, or_false]

Premises used: ENat.map_eq_top_iff, WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff, reduceDIte, meromorphicOrderAt, WithTop.natCast_ne_top, or_false
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
pos :
  ∀
    (h :
      analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
              f z)
          x =
        ⊤),
    analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
              f z)
          x =
        ⊤ ↔
      ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
neg :
  ∀
    (h :
      ¬analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
                f z)
            x =
          ⊤),
    analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
              f z)
          x =
        ⊤ ↔
      ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
            f z)
        x =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤

Premises used: HSub.hSub, HPow.hPow, analyticOrderAt, HSMul.hSMul, Exists.choose
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x =
    ⊤
pos : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
⊢ analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
            f z)
        x =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [h, eventually_nhdsWithin_iff, mem_compl_iff, mem_singleton_iff, true_iff]

Premises used: true_iff, Set.mem_singleton_iff, eventually_nhdsWithin_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x =
    ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0

Tactic:
rw [analyticOrderAt_eq_top] at h

Premises used: analyticOrderAt_eq_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h₁ :
  ∀ (z : 𝕜)
    (hf :
      (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z =
        0)
    (hz : ¬z = x), f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0

Tactic:
filter_upwards [h] with z hf hz
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf_1 : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf_1 •
        f z =
      0
z : 𝕜
hf :
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf_1 •
      f z =
    0
hz : ¬z = x
h₁ h₂ h₃ h₄ : ∀ (hf : f z = 0) (hz : ¬z = x), f z = 0
⊢ f z = 0

Tactic:
rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf

Premises used: Iff.mpr, sub_ne_zero, pow_ne_zero, smul_eq_zero_iff_right
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
neg :
  ∀ (m : ℕ)
    (hm :
      (↑m : ℕ∞) =
        analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
              f z)
          x),
    analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
              f z)
          x =
        ⊤ ↔
      ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
            f z)
        x =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp h

Premises used: ENat.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
neg : ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
            f z)
        x =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [← hm, ENat.coe_ne_top, false_iff]

Premises used: false_iff, ENat.coe_ne_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
neg :
  ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0),
    analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
contrapose h
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
neg :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
⊢ analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x =
    ⊤

Tactic:
rw [analyticOrderAt_eq_top]

Premises used: analyticOrderAt_eq_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
neg :
  ∃ᶠ (z : 𝕜) in 𝓝[≠] x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0

Tactic:
rw [← hf.choose_spec.frequently_eq_iff_eventually_eq analyticAt_const]

Premises used: Exists.choose_spec, analyticAt_const, AnalyticAt.frequently_eq_iff_eventually_eq
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
neg :
  ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
    (x_1 - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f x_1 =
      0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0

Tactic:
apply Eventually.frequently

Premises used: Filter.Eventually.frequently