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 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
exact (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt.2 (h x hx)

Premises used: Iff.mpr, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt
-- 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₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∉ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp [hx]
-- 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₁f : AnalyticOnNhd 𝕜 f U
⊢ MeromorphicNFOn f U

Tactic:
fun z hz ↦ (h₁f z hz).meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt, 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 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h :
  ∀ (u : 𝕜),
    u ∈ U ∩ f ⁻¹' {0} ↔
      Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
⊢ U ∩ f ⁻¹' {0} = Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)

Tactic:
ext 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
h :
  u ∈ U ∩ f ⁻¹' {0} →
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
h₁ :
  Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u →
    u ∈ U ∩ f ⁻¹' {0}
⊢ u ∈ U ∩ f ⁻¹' {0} ↔
    Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : u ∈ U ∩ f ⁻¹' {0}
⊢ Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u

Tactic:
simp_all only [ne_eq, Subtype.forall, Set.mem_inter_iff, Set.mem_preimage,
      Set.mem_singleton_iff, Function.mem_support, h₁f.meromorphicOn, MeromorphicOn.divisor_apply,
      WithTop.untop₀_eq_zero, (h₁f hu.1).meromorphicOrderAt_eq_zero_iff, not_true_eq_false, or_self,
      not_false_eq_true]

Premises used: Set.mem_inter_iff, not_true_eq_false, Subtype.forall, MeromorphicOn.divisor_apply, ne_eq, Set.mem_singleton_iff, And.left, MeromorphicNFOn.meromorphicOn, or_self, Function.mem_support, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, WithTop.untop₀_eq_zero, not_false_eq_true, Set.mem_preimage
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : Membership.mem (γ := Set 𝕜) (Function.support (M := ℤ) (⇑(MeromorphicOn.divisor f U) : (a : 𝕜) → ℤ)) u
⊢ ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)

Tactic:
simp only [Function.mem_support, ne_eq] at hu

Premises used: ne_eq, Function.mem_support
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
h : u ∈ U
h₁ : u ∈ f ⁻¹' {0}
⊢ u ∈ U ∩ f ⁻¹' {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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ u ∈ U

Tactic:
(MeromorphicOn.divisor f U).supportWithinDomain hu

Premises used: MeromorphicOn.divisor, Function.locallyFinsuppWithin.supportWithinDomain
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ u ∈ U

Tactic:
exact (MeromorphicOn.divisor f U).supportWithinDomain hu

Premises used: MeromorphicOn.divisor, Function.locallyFinsuppWithin.supportWithinDomain
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
⊢ ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0

Tactic:
have := h₁f ((MeromorphicOn.divisor f U).supportWithinDomain hu)
        |>.meromorphicOrderAt_eq_zero_iff.not
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
hu : ¬Eq (α := ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) u : ℤ) (0 : ℤ)
this : ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0
⊢ ¬meromorphicOrderAt f u = 0 ∧ ¬meromorphicOrderAt f u = ⊤

Tactic:
simp only [h₁f.meromorphicOn, (MeromorphicOn.divisor f U).supportWithinDomain hu,
        MeromorphicOn.divisor_apply, WithTop.untop₀_eq_zero, not_or] at hu

Premises used: MeromorphicOn.divisor, MeromorphicOn.divisor_apply, not_or, Function.locallyFinsuppWithin.supportWithinDomain, MeromorphicNFOn.meromorphicOn, WithTop.untop₀_eq_zero
-- 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₁f : MeromorphicNFOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
u : 𝕜
this : ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0
hu : ¬meromorphicOrderAt f u = 0 ∧ ¬meromorphicOrderAt f u = ⊤
⊢ f u = 0

Tactic:
simp_all [hu.1]

Premises used: And.left
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
mp : MeromorphicNFOn (g • f) U → MeromorphicNFOn f U
mpr : MeromorphicNFOn f U → MeromorphicNFOn (g • f) U
⊢ MeromorphicNFOn (g • f) U ↔ 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
mp : MeromorphicNFAt (g • f) z
⊢ MeromorphicNFAt f z

Tactic:
rw [← meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g z hz) (h₂g z hz)]

Premises used: meromorphicNFAt_smul_iff_right_of_analyticAt
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (g • f) z

Tactic:
h hz
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn (g • f) U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (g • f) z

Tactic:
exact h hz
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn f U
z : 𝕜
hz : z ∈ U
mpr : g z ≠ 0
⊢ MeromorphicNFAt (g • f) z

Tactic:
apply (h hz).smul_analytic (h₁g z hz)

Premises used: MeromorphicNFAt.smul_analytic
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn f U
z : 𝕜
hz : z ∈ U
⊢ g z ≠ 0

Tactic:
h₂g z hz
-- 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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
h : MeromorphicNFOn f U
z : 𝕜
hz : z ∈ U
⊢ g z ≠ 0

Tactic:
exact h₂g z hz
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
rw : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
⊢ MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U

Tactic:
rw [← smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

Tactic:
meromorphicNFOn_smul_iff_right_of_analyticOnNhd h₁g h₂g

Premises used: meromorphicNFOn_smul_iff_right_of_analyticOnNhd
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

Tactic:
exact meromorphicNFOn_smul_iff_right_of_analyticOnNhd h₁g h₂g

Premises used: meromorphicNFOn_smul_iff_right_of_analyticOnNhd
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
rw : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U
⊢ MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U

Tactic:
rw [mul_comm, ← smul_eq_mul]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

Tactic:
meromorphicNFOn_mul_iff_right_of_analyticOnNhd h₁g h₂g

Premises used: meromorphicNFOn_mul_iff_right_of_analyticOnNhd
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

Tactic:
exact meromorphicNFOn_mul_iff_right_of_analyticOnNhd h₁g h₂g

Premises used: meromorphicNFOn_mul_iff_right_of_analyticOnNhd
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
⊢ MeromorphicNFOn (E := 𝕜) (∏ i ∈ s, f i) U

Tactic:
fun x hx ↦ meromorphicNFAt_prod (h₁f · · hx) (h₂f x hx)

Premises used: meromorphicNFAt_prod, MeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
⊢ MeromorphicNFOn (E := 𝕜) (∏ i ∈ s, f i) U

Tactic:
meromorphicNFOn_prod h₁f h₂f

Premises used: meromorphicNFOn_prod
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
⊢ MeromorphicNFOn (E := 𝕜) (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) U

Tactic:
convert! meromorphicNFOn_prod h₁f h₂f

Premises used: meromorphicNFOn_prod
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)

Tactic:
(Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | σ ∈ s ∧ f σ x = 0}
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)

Tactic:
exact (Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFOn (f i) U
h₂f : ∀ x ∈ U, Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
⊢ MeromorphicNFOn (E := 𝕜) (∏ᶠ (i : ι), f i) U

Tactic:
fun x hx ↦ meromorphicNFAt_finprod (h₁f · hx) (h₂f x hx)

Premises used: meromorphicNFAt_finprod, MeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
U : Set 𝕜
hf : MeromorphicNFOn f U
⊢ MeromorphicNFOn (f ^ n) U

Tactic:
fun _ hz ↦ (hf hz).zpow

Premises used: MeromorphicNFAt.zpow, MeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
⊢ MeromorphicNFOn (E := 𝕜) (fun (x : 𝕜) ↦ (f x)⁻¹) U ↔ MeromorphicNFOn f U

Tactic:
meromorphicNFOn_inv

Premises used: meromorphicNFOn_inv
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
pos : (h₁f : MeromorphicOn f U) → 𝕜 → E
neg : (h₁f : ¬MeromorphicOn f U) → 𝕜 → E
⊢ 𝕜 → E

Tactic:
by_cases h₁f : MeromorphicOn f U

Premises used: 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
pos : (hz : z ∈ U) → E
neg : (hz : z ∉ U) → E
⊢ E

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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ E

Tactic:
exact toMeromorphicNFAt f z z

Premises used: 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : MeromorphicOn f U
z : 𝕜
hz : z ∉ U
⊢ E

Tactic:
exact f 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
h₁f : ¬MeromorphicOn f U
⊢ 𝕜 → E

Tactic:
exact 0
-- 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
⊢ toMeromorphicNFOn f U = 0

Tactic:
simp [toMeromorphicNFOn, hf]

Premises used: 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 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ Uᶜ
⊢ toMeromorphicNFOn f U x = f x

Tactic:
simp_all [toMeromorphicNFOn]

Premises used: 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 𝕜
hf : MeromorphicOn f U
⊢ U ∈ Filter.codiscreteWithin U

Tactic:
simp
-- 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
⊢ U ∈ Filter.codiscreteWithin U

Tactic:
have : U ∈ Filter.codiscreteWithin U := by simp
-- 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
this : U ∈ Filter.codiscreteWithin U
h : ∀ (a : 𝕜) (h₁a : AnalyticAt 𝕜 f a) (h₂a : a ∈ U), f a = toMeromorphicNFOn f U a
⊢ f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U

Tactic:
filter_upwards [hf.analyticAt_mem_codiscreteWithin, this] with a h₁a h₂a

Premises used: MeromorphicOn.analyticAt_mem_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
U : Set 𝕜
hf : MeromorphicOn f U
this : U ∈ Filter.codiscreteWithin U
a : 𝕜
h₁a : AnalyticAt 𝕜 f a
h₂a : a ∈ U
⊢ f a = toMeromorphicNFOn f U a

Tactic:
simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 h₁a.meromorphicNFAt).symm]

Premises used: Iff.mpr, toMeromorphicNFAt_eq_self, AnalyticAt.meromorphicNFAt, toMeromorphicNFOn, 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
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
h : ∀ (a : 𝕜) (ha : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ), toMeromorphicNFOn f U a = f a
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha

Premises used: MeromorphicOn.eventually_analyticAt_or_mem_compl
-- 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
a : 𝕜
ha : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h : ∀ (ha : AnalyticAt 𝕜 f a), toMeromorphicNFOn f U a = f a
h₁ : ∀ (ha : a ∈ Uᶜ), toMeromorphicNFOn f U a = f a
⊢ toMeromorphicNFOn f U a = f a

Tactic:
rcases ha with ha | ha
-- 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
a : 𝕜
ha : AnalyticAt 𝕜 f a
⊢ toMeromorphicNFOn f U a = f a

Tactic:
simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]

Premises used: Iff.mpr, toMeromorphicNFAt_eq_self, AnalyticAt.meromorphicNFAt, toMeromorphicNFOn, 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
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : a ∈ Uᶜ
⊢ a ∉ U

Tactic:
simp only [Set.mem_compl_iff] at ha

Premises used: Set.mem_compl_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 : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : a ∉ U
⊢ toMeromorphicNFOn f U a = f a

Tactic:
simp [toMeromorphicNFOn, ha, hf]

Premises used: 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
h₁ : toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x
h₂ : toMeromorphicNFOn f U x = toMeromorphicNFAt f x x
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE

Premises used: eventuallyEq_nhds_of_eventuallyEq_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] toMeromorphicNFAt f x

Tactic:
(hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx).trans (hf x hx).eq_nhdsNE_toMeromorphicNFAt

Premises used: MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE, Filter.EventuallyEq.trans, MeromorphicAt.eq_nhdsNE_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
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x

Tactic:
exact (hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx).trans (hf x hx).eq_nhdsNE_toMeromorphicNFAt

Premises used: MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE, Filter.EventuallyEq.trans, MeromorphicAt.eq_nhdsNE_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
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U x = toMeromorphicNFAt f x x

Tactic:
simp [toMeromorphicNFOn, hf, hx]

Premises used: 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
apply : toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x
⊢ toMeromorphicNFOn f U x = toMeromorphicNFAt f x x

Tactic:
apply Filter.EventuallyEq.eq_of_nhds (g := toMeromorphicNFAt f x)

Premises used: Filter.EventuallyEq.eq_of_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 : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x

Tactic:
simp [(toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hx).trans]

Premises used: Filter.EventuallyEq.trans, toMeromorphicNFOn_eq_toMeromorphicNFAt_on_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
U : Set 𝕜
pos : ∀ (hf : MeromorphicOn f U), MeromorphicNFOn (toMeromorphicNFOn f U) U
neg : ∀ (hf : ¬MeromorphicOn f U), MeromorphicNFOn (toMeromorphicNFOn f U) U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

Tactic:
by_cases hf : MeromorphicOn f U

Premises used: MeromorphicOn