awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
ι : Type u_4
s : Finset ι
f : ι → 𝕜 → E
h : ∀ σ ∈ s, MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_3} (E := E) (∑ n ∈ s, f n) U

Tactic:
fun z hz ↦ MeromorphicAt.sum (h · · z hz)

Premises used: MeromorphicAt.sum, MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
ι : Type u_4
s : Finset ι
f : ι → 𝕜 → E
h : ∀ (σ : ι), MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ∑ n ∈ s, f n z) U

Tactic:
fun z hz ↦ MeromorphicAt.fun_sum (fun σ _ ↦ h σ z hz)

Premises used: MeromorphicOn, MeromorphicAt.fun_sum
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_4
f : ι → 𝕜 → 𝕜'
h : ∀ (σ : ι), MeromorphicOn (f σ) U
⊢ MeromorphicOn.{u_1, u_2} (E := 𝕜') (∑ᶠ (n : ι), f n) U

Tactic:
fun z hz ↦ MeromorphicAt.finsum (h · z hz)

Premises used: MeromorphicAt.finsum, MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
hs : MeromorphicOn s U
⊢ MeromorphicOn s⁻¹ U

Tactic:
fun x hx ↦ (hs x hx).inv

Premises used: MeromorphicOn, MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
h : MeromorphicOn s⁻¹ U
⊢ MeromorphicOn s U

Tactic:
simpa only [inv_inv] using h.inv

Premises used: MeromorphicOn.inv, inv_inv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s t : 𝕜 → 𝕜'
U : Set 𝕜
hs : MeromorphicOn s U
ht : MeromorphicOn t U
⊢ MeromorphicOn (s / t) U

Tactic:
fun x hx ↦ (hs x hx).div (ht x hx)

Premises used: MeromorphicOn, MeromorphicAt.div
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
hs : MeromorphicOn s U
n : ℕ
⊢ MeromorphicOn (s ^ n) U

Tactic:
fun x hx ↦ (hs x hx).pow _

Premises used: MeromorphicOn, MeromorphicAt.pow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
hs : MeromorphicOn s U
n : ℤ
⊢ MeromorphicOn (s ^ n) U

Tactic:
fun x hx ↦ (hs x hx).zpow _

Premises used: MeromorphicOn, MeromorphicAt.zpow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
inst_3 : CompleteSpace E
⊢ MeromorphicOn (deriv f) U

Tactic:
fun z hz ↦ (hf z hz).deriv

Premises used: MeromorphicOn, MeromorphicAt.deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
inst_3 : CompleteSpace E
⊢ MeromorphicOn.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ deriv f z) U

Tactic:
hf.deriv

Premises used: MeromorphicOn.deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
inst_3 : CompleteSpace E
n : ℕ
⊢ MeromorphicOn (deriv^[n] f) U

Tactic:
fun z hz ↦ (hf z hz).iterated_deriv

Premises used: MeromorphicAt.iterated_deriv, MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
inst_3 : CompleteSpace E
n : ℕ
⊢ MeromorphicOn.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ deriv^[n] f z) U

Tactic:
hf.iterated_deriv

Premises used: MeromorphicOn.iterated_deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : EqOn f g U
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ MeromorphicOn g U

Tactic:
fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, MeromorphicOn, nhdsWithin_le_nhds, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : EqOn f g U
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
refine : ∀ (x : 𝕜) (hx : x ∈ U), f =ᶠ[𝓝 x] g
⊢ MeromorphicOn g U

Tactic:
refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : EqOn f g U
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝 x] g

Tactic:
eventually_of_mem (hu.mem_nhds hx) h_eq

Premises used: Filter.EventuallyEq, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : EqOn f g U
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝 x] g

Tactic:
exact eventually_of_mem (hu.mem_nhds hx) h_eq

Premises used: Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
rw : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
⊢ ∀ᶠ (y : 𝕜) in codiscreteWithin U, AnalyticAt 𝕜 f y

Tactic:
rw [eventually_iff, mem_codiscreteWithin]

Premises used: Filter.eventually_iff, mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
rw : (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ ∈ 𝓝[≠] x
⊢ Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))

Tactic:
rw [disjoint_principal_right]

Premises used: Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
apply : {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y) x} ⊆ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
⊢ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ ∈ 𝓝[≠] x

Tactic:
apply Filter.mem_of_superset ((h x hx).eventually_analyticAt)

Premises used: MeromorphicAt.eventually_analyticAt, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x_1 : 𝕜
hx_1 : x_1 ∈ U
x : 𝕜
hx : Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y) x} x
⊢ x ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
inst_3 : SecondCountableTopology 𝕜
inst_4 : CompleteSpace E
h : MeromorphicOn f U
apply : {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜᶜ ∈ codiscreteWithin U
⊢ ({z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ ∩ U).Countable

Tactic:
apply (HereditarilyLindelofSpace.isLindelof _).countable_of_isDiscrete
    (isDiscrete_of_codiscreteWithin _)

Premises used: IsLindelof.countable_of_isDiscrete, HereditarilyLindelofSpace.isLindelof, isDiscrete_of_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
inst_3 : SecondCountableTopology 𝕜
inst_4 : CompleteSpace E
h : MeromorphicOn f U
⊢ {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜᶜ ∈ codiscreteWithin U

Tactic:
simpa using eventually_codiscreteWithin_analyticAt f h

Premises used: MeromorphicOn.eventually_codiscreteWithin_analyticAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
mp : MeromorphicOn f univ → Meromorphic f
mpr : Meromorphic f → MeromorphicOn f univ
mp₁ mp₂ : MeromorphicOn f univ → Meromorphic f
mp₃ : MeromorphicOn f univ → ∀ (x : 𝕜), MeromorphicAt f x
mpr₁ mpr₂ : Meromorphic f → MeromorphicOn f univ
mpr₃ : Meromorphic f → ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) univ x → MeromorphicAt f x
mp₄ mp₅ mp₆ : MeromorphicOn f univ → ∀ (x : 𝕜), MeromorphicAt f x
mpr₄ mpr₅ mpr₆ : Meromorphic f → ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) univ x → MeromorphicAt f x
mp₇ mp₈ mp₉ : MeromorphicOn f univ → ∀ (x : 𝕜), MeromorphicAt f x
mpr₇ mpr₈ mpr₉ : Meromorphic f → ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) univ x → MeromorphicAt f x
mp₁₀ mp₁₁ : MeromorphicOn f univ → ∀ (x : 𝕜), MeromorphicAt f x
mpr₁₀ mpr₁₁ : Meromorphic f → ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) univ x → MeromorphicAt f x
⊢ MeromorphicOn f univ ↔ Meromorphic f

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : Meromorphic f
⊢ MeromorphicAt f x

Tactic:
hf x
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
s : Set 𝕜
hf : Meromorphic f
⊢ MeromorphicOn f s

Tactic:
fun x _ ↦ hf x

Premises used: MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ Meromorphic.{u_1, u_3} (E := E) fun (x_1 : 𝕜) ↦ x

Tactic:
fun _ ↦ .const _ _

Premises used: Meromorphic, MeromorphicAt.const
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : Meromorphic f
⊢ Meromorphic (-f)

Tactic:
fun x ↦ (hf x).neg

Premises used: Meromorphic, MeromorphicAt.neg
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
hg : Meromorphic g
⊢ Meromorphic (f + g)

Tactic:
fun x ↦ (hf x).add (hg x)

Premises used: Meromorphic, MeromorphicAt.add
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_4
s : Finset ι
G : ι → 𝕜 → E
h : ∀ σ ∈ s, Meromorphic (G σ)
⊢ Meromorphic.{u_1, u_3} (𝕜 := 𝕜) (E := E) (∑ n ∈ s, G n)

Tactic:
fun x ↦ MeromorphicAt.sum (h · · x)

Premises used: Meromorphic, MeromorphicAt.sum
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
h : ∀ (σ : ι), Meromorphic (F σ)
⊢ Meromorphic.{u_1, u_2} (𝕜 := 𝕜) (E := 𝕜') (∑ᶠ (σ : ι), F σ)

Tactic:
fun x ↦ MeromorphicAt.finsum (h · x)

Premises used: MeromorphicAt.finsum, Meromorphic
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
hg : Meromorphic g
⊢ Meromorphic (f - g)

Tactic:
fun x ↦ (hf x).sub (hg x)

Premises used: Meromorphic, MeromorphicAt.sub
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
hf : Meromorphic f
hg : Meromorphic g
⊢ Meromorphic (f • g)

Tactic:
fun x ↦ (hf x).smul (hg x)

Premises used: Meromorphic, MeromorphicAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
hf : Meromorphic f
hg : Meromorphic g
⊢ Meromorphic (f * g)

Tactic:
fun x ↦ (hf x).mul (hg x)

Premises used: MeromorphicAt.mul, Meromorphic
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
hf : Meromorphic f
⊢ Meromorphic f⁻¹

Tactic:
fun x ↦ (hf x).inv

Premises used: Meromorphic, MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ σ ∈ s, Meromorphic (F σ)
⊢ Meromorphic.{u_1, u_2} (𝕜 := 𝕜) (E := 𝕜') (∏ n ∈ s, F n)

Tactic:
fun x ↦ MeromorphicAt.prod (h · · x)

Premises used: Meromorphic, MeromorphicAt.prod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_4
F : ι → 𝕜 → 𝕜'
h : ∀ (σ : ι), Meromorphic (F σ)
⊢ Meromorphic.{u_1, u_2} (𝕜 := 𝕜) (E := 𝕜') (∏ᶠ (σ : ι), F σ)

Tactic:
fun x ↦ MeromorphicAt.finprod (h · x)

Premises used: Meromorphic, MeromorphicAt.finprod
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
hf : Meromorphic f
hg : Meromorphic g
⊢ Meromorphic (f / g)

Tactic:
fun x ↦ (hf x).div (hg x)

Premises used: Meromorphic, MeromorphicAt.div
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
n : ℕ
hf : Meromorphic f
⊢ Meromorphic (f ^ n)

Tactic:
fun x ↦ (hf x).pow n

Premises used: Meromorphic, MeromorphicAt.pow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
n : ℤ
hf : Meromorphic f
⊢ Meromorphic (f ^ n)

Tactic:
fun x ↦ (hf x).zpow n

Premises used: Meromorphic, MeromorphicAt.zpow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : CompleteSpace E
hf : Meromorphic f
⊢ Meromorphic (deriv f)

Tactic:
fun x ↦ (hf x).deriv

Premises used: Meromorphic, MeromorphicAt.deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : CompleteSpace E
n : ℕ
hf : Meromorphic f
⊢ Meromorphic (deriv^[n] f)

Tactic:
fun x ↦ (hf x).iterated_deriv

Premises used: Meromorphic, MeromorphicAt.iterated_deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : Meromorphic f
h₁ : f =ᶠ[codiscrete 𝕜] g
rw : ∀ (hf : MeromorphicOn f univ) (h₁ : f =ᶠ[codiscrete 𝕜] g), MeromorphicOn g univ
⊢ Meromorphic g

Tactic:
rw [← meromorphicOn_univ] at *

Premises used: meromorphicOn_univ
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : MeromorphicOn f univ
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ MeromorphicOn g univ

Tactic:
hf.congr_codiscreteWithin (eventuallyEq_of_mem h₁ fun ⦃x⦄ a ↦ a) isOpen_univ

Premises used: Filter.eventuallyEq_of_mem, MeromorphicOn.congr_codiscreteWithin, isOpen_univ
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : MeromorphicOn f univ
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ MeromorphicOn g univ

Tactic:
exact hf.congr_codiscreteWithin (eventuallyEq_of_mem h₁ fun ⦃x⦄ a ↦ a) isOpen_univ

Premises used: Filter.eventuallyEq_of_mem, MeromorphicOn.congr_codiscreteWithin, isOpen_univ
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ Meromorphic f ↔ Meromorphic g

Tactic:
⟨(·.congr_codiscrete h₁), (·.congr_codiscrete h₁.symm)⟩

Premises used: Meromorphic.congr_codiscrete, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : SecondCountableTopology 𝕜
inst_4 : CompleteSpace E
h : Meromorphic f
⊢ Set.Countable.{u_1} (α := 𝕜) {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ

Tactic:
simpa using (h.meromorphicOn (s := univ)).countable_compl_analyticAt_inter

Premises used: Meromorphic.meromorphicOn, MeromorphicOn.countable_compl_analyticAt_inter
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
⊢ sᶜ.Countable

Tactic:
simpa using h.countable_compl_analyticAt

Premises used: Meromorphic.countable_compl_analyticAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
⊢ sᶜ.Countable

Tactic:
have h₁ : sᶜ.Countable := by simpa using h.countable_compl_analyticAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
⊢ Countable.{u_1 + 1} (↑sᶜ : Type u_1)

Tactic:
have h₁' := h₁.to_subtype
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable.{u_1 + 1} (↑sᶜ : Type u_1)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable.{u_1 + 1} (↑sᶜ : Type u_1)
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousOn f s

Tactic:
have h₃ : ContinuousOn f s := fun z hz ↦ hz.continuousAt.continuousWithinAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable.{u_1 + 1} (↑sᶜ : Type u_1)
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h₃ : ContinuousOn f s
⊢ Subset.{u_1} (α := Set 𝕜) univ
    (range (ι := { x : 𝕜 // x ∈ s }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ s)) ∪
      range (ι := { x : 𝕜 // x ∈ sᶜ }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ sᶜ)))

Tactic:
simp [-mem_compl_iff]

Premises used: Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
inst_3 : MeasurableSpace 𝕜
inst_4 : SecondCountableTopology 𝕜
inst_5 : BorelSpace 𝕜
inst_6 : MeasurableSpace E
inst_7 : CompleteSpace E
inst_8 : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z : 𝕜 | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable.{u_1 + 1} (↑sᶜ : Type u_1)
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h₃ : ContinuousOn f s
⊢ Measurable f

Tactic:
exact .of_union_range_cover (.subtype_coe h₂.measurableSet) (.subtype_coe h₁.measurableSet)
    (by simp [-mem_compl_iff]) h₃.restrict.measurable (measurable_of_countable _)
-- Module: Mathlib.Analysis.Meromorphic.Complex
Goal:
⊢ MeromorphicNFOn Complex.Gamma univ

Tactic:
meromorphicNFOn_inv.mp <| AnalyticOnNhd.meromorphicNFOn <|
    analyticOnNhd_univ_iff_differentiable.mpr differentiable_one_div_Gamma

Premises used: Iff.mpr, Complex.analyticOnNhd_univ_iff_differentiable, meromorphicNFOn_inv, AnalyticOnNhd.meromorphicNFOn, Complex.differentiable_one_div_Gamma, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Complex
Goal:
⊢ Meromorphic Complex.Gamma

Tactic:
meromorphicOn_univ.mp MeromorphicNFOn.Gamma.meromorphicOn

Premises used: meromorphicOn_univ, MeromorphicNFOn.Gamma, Iff.mp, MeromorphicNFOn.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Complex
Goal:
s : Set ℂ
⊢ MeromorphicOn Complex.Gamma s

Tactic:
Meromorphic.Gamma.meromorphicOn

Premises used: Meromorphic.meromorphicOn, Meromorphic.Gamma
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z_1 : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
z : 𝕜
hz :
  Membership.mem (γ := Set 𝕜)
    (Function.support (M := ℤ) fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) z
by_contra : ∀ (h₂z : z ∉ U), False
⊢ z ∈ U

Tactic:
by_contra h₂z
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z_1 : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
z : 𝕜
hz :
  Membership.mem (γ := Set 𝕜)
    (Function.support (M := ℤ) fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) z
h₂z : z ∉ U
⊢ False

Tactic:
simp [h₂z] at hz