awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
h :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g
t₁ : (support (M := 𝕜 → ℝ) fun (u x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) u) : ℝ) * log ‖x - u‖) = D.support (U := U)
h₃f : D.support (U := U).Finite
z : 𝕜
hz :
  f z =
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) g z
h₂z : Eq (α := ℤ) ((D : (a : 𝕜) → ℤ) z : ℤ) (0 : ℤ)
h₃z : z ∈ U
this : ∀ x ∈ h₃f.toFinset (s := D.support (U := U)), HPow.hPow (β := ℤ) ‖z - x‖ ((D : (a : 𝕜) → ℤ) x : ℤ) ≠ 0
⊢ ∑ i ∈ h₃f.toFinset (s := D.support (U := U)), log (HPow.hPow (β := ℤ) ‖z - i‖ ((D : (a : 𝕜) → ℤ) i : ℤ)) + log ‖g z‖ =
    HAdd.hAdd (α := 𝕜 → ℝ) (β := 𝕜 → ℝ)
      (∑ i ∈ h₃f.toFinset (s := D.support (U := U)), fun (x : 𝕜) ↦ (↑((D : (a : 𝕜) → ℤ) i) : ℝ) * log ‖x - i‖)
      (fun (x : 𝕜) ↦ log ‖g x‖) z

Tactic:
simp [log_zpow]

Premises used: Real.log_zpow
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x

Tactic:
have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x :=
    (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
t₀ : MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x
⊢ MeromorphicAt (HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
t₀ : MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x
rw :
  HSMul.hSMul (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x)
      (g x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)
⊢ meromorphicTrailingCoeffAt f x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)

Tactic:
rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (by fun_prop) h₁x h₂x h),
    t₀.meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g]

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero, meromorphicTrailingCoeffAt_congr_nhdsNE, MeromorphicAt.meromorphicTrailingCoeffAt_smul, MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
t₀ : MeromorphicAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x
⊢ HSMul.hSMul (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x)
      (g x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) D x 0 u) (g x)

Tactic:
simp [meromorphicTrailingCoeffAt_factorizedRational hD]

Premises used: Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
hx :
  Norm.norm (E := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) ≠ 0
hy : ‖g x‖ ≠ 0
⊢ log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ (u : 𝕜), (↑(D u) : ℝ) * log ‖x - u‖ + log ‖g x‖

Tactic:
rw [meromorphicTrailingCoeffAt_congr_nhdsNE
      (hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
        (((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt)
          h₁x h₂x h),
    ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).meromorphicTrailingCoeffAt_smul
      h₁g.meromorphicAt, h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g,
    norm_smul, log_mul, log_norm_meromorphicTrailingCoeffAt hD]

Premises used: norm_smul, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero, meromorphicTrailingCoeffAt_congr_nhdsNE, MeromorphicAt.meromorphicTrailingCoeffAt_smul, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, MeromorphicNFOn.meromorphicOn, MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin, MeromorphicAt.smul, Real.log_mul, AnalyticAt.meromorphicAt, Function.FactorizedRational.meromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
hx : ¬Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) 0
⊢ Norm.norm (E := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) ≠ 0

Tactic:
simp only [ne_eq, norm_eq_zero]

Premises used: norm_eq_zero, ne_eq
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
hx : meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x ≠ ⊤
⊢ ¬Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x) 0

Tactic:
apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero
      ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x)

Premises used: MeromorphicNFOn.meromorphicOn, MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero, Function.FactorizedRational.meromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) x ≠ ⊤

Tactic:
apply FactorizedRational.meromorphicOrderAt_ne_top

Premises used: Function.FactorizedRational.meromorphicOrderAt_ne_top
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] HSMul.hSMul (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (D u)) g
⊢ ‖g x‖ ≠ 0

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

Tactic:
⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right, fun h ↦ h.frequently⟩

Premises used: MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero, Iff.intro, Filter.Eventually.frequently, Or.resolve_right
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
rw : ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ f =ᶠ[𝓝[≠] x] 0

Tactic:
rw [← hf.frequently_zero_iff_eventuallyEq_zero]

Premises used: MeromorphicAt.frequently_zero_iff_eventuallyEq_zero
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
apply : ∀ (x : 𝕜), x ∈ U ∧ x ∈ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = 0 x) x} ∪ Uᶜ → f x = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
apply ((accPt_iff_frequently_nhdsNE.1 h₂x).and_eventually <| eventually_mem_set.2
    (mem_codiscreteWithin_iff_forall_mem_nhdsNE.1 h x h₁x)).mono

Premises used: Iff.mpr, mem_codiscreteWithin_iff_forall_mem_nhdsNE, accPt_iff_frequently_nhdsNE, Filter.Frequently.mono, Filter.Frequently.and_eventually, Iff.mp, Filter.eventually_mem_set
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] 0
⊢ ∀ (x : 𝕜), x ∈ U ∧ x ∈ {x : 𝕜 | (fun (x : 𝕜) ↦ f x = 0 x) x} ∪ Uᶜ → f x = 0

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
h :
  ∀ (x : 𝕜) (h₁x : AnalyticAt 𝕜 f x) (h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)), f x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
filter_upwards [h₁f.analyticAt_mem_codiscreteWithin,
    h₁f.codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top h₂f] with x h₁x h₂x

Premises used: MeromorphicOn.analyticAt_mem_codiscreteWithin, MeromorphicOn.codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
x : 𝕜
h₁x : AnalyticAt 𝕜 f x
h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)
⊢ meromorphicOrderAt f x ≠ ⊤

Tactic:
have := h₂f x h₂x.1
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
x : 𝕜
h₁x : AnalyticAt 𝕜 f x
h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)
this : meromorphicOrderAt f x ≠ ⊤
⊢ f x ≠ 0

Tactic:
simp_all [← h₁x.analyticOrderAt_eq_zero, h₁x.meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
rw : (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, (f - g) z = 0
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ f =ᶠ[𝓝[≠] x] g

Tactic:
rw [eventuallyEq_iff_sub, ← (hf.sub hg).frequently_zero_iff_eventuallyEq_zero]

Premises used: MeromorphicAt.sub, Filter.eventuallyEq_iff_sub, MeromorphicAt.frequently_zero_iff_eventuallyEq_zero
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
simp_rw : (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z - g z = 0
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, (f - g) z = 0

Tactic:
simp_rw [Pi.sub_apply, sub_eq_zero]

Premises used: sub_eq_zero, Pi.sub_apply
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f =ᶠ[codiscreteWithin U] g
rw : ∀ (h : f - g =ᶠ[codiscreteWithin U] 0), f - g =ᶠ[𝓝[≠] x] 0
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
rw [eventuallyEq_iff_sub] at *

Premises used: Filter.eventuallyEq_iff_sub
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
h : f - g =ᶠ[codiscreteWithin U] 0
⊢ f - g =ᶠ[𝓝[≠] x] 0

Tactic:
apply (hf.sub hg).eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin h₁x h₂x h

Premises used: MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin, MeromorphicAt.sub
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
hx : x ∈ U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin hg hx (hU x hx) h

Premises used: MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
rw : ∃ (t : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g
⊢ ∀ᶠ (x : 𝕜) in 𝓝ˢ U, f =ᶠ[𝓝[≠] x] g

Tactic:
rw [eventually_nhdsSet_iff_exists]

Premises used: eventually_nhdsSet_iff_exists
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
h₁ :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧
    U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} x → f =ᶠ[𝓝[≠] x] g
⊢ ∃ (t : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g

Tactic:
use {x | f =ᶠ[𝓝[≠] x] g}
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧
    U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} x → f =ᶠ[𝓝[≠] x] g

Tactic:
simp only [Set.mem_setOf_eq, imp_self, implies_true, and_true]

Premises used: and_true, Set.mem_setOf_eq, imp_self, implies_true
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
h₂ : U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : 𝕜 | f =ᶠ[𝓝[≠] x] g}

Tactic:
apply isOpen_setOf_eventually_nhdsWithin

Premises used: isOpen_setOf_eventually_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf x hx) (hg x hx) hx (hU x hx) h

Premises used: MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
exact eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf x hx) (hg x hx) hx (hU x hx) h

Premises used: MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
-- 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 : 𝕜
mp : MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
mpr : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0 → MeromorphicNFAt f x
⊢ MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

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
x : 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
simp [(analyticAt_congr h).2 analyticAt_const]

Premises used: Iff.mpr, analyticAt_const, analyticAt_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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
apply : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
⊢ MeromorphicAt f x

Tactic:
apply MeromorphicAt.congr _ (h₃g.filter_mono nhdsWithin_le_nhds).symm

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds, MeromorphicAt.congr, Filter.EventuallyEq.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
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x

Tactic:
fun_prop
-- 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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicAt f x

Tactic:
have hf : MeromorphicAt f x := by
        apply MeromorphicAt.congr _ (h₃g.filter_mono nhdsWithin_le_nhds).symm
        fun_prop
-- 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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hf : MeromorphicAt f x
rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff hf]

Premises used: meromorphicOrderAt_eq_int_iff
-- 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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hf : MeromorphicAt f x
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
use g, h₁g, h₂g
-- 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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hf : MeromorphicAt f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
eventually_nhdsWithin_of_eventually_nhds h₃g

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- 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 : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hf : MeromorphicAt f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact eventually_nhdsWithin_of_eventually_nhds h₃g

Premises used: eventually_nhdsWithin_of_eventually_nhds