awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : ¬n = 0
hz : z ∉ U
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg neg₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg₂ neg₃ :
  ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∉ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)

Tactic:
classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]

Premises used: MeromorphicOn.divisor_apply, MeromorphicOn.zpow
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
⊢ divisor (E := 𝕜) (fun (z : 𝕜) ↦ f z ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)

Tactic:
divisor_zpow hf n

Premises used: MeromorphicOn.divisor_zpow
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
h :
  ∀ (x : 𝕜),
    Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
      ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin V ℤ)
    (Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV) (divisor f V)

Tactic:
ext x
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
pos :
  ∀ (hx : x ∈ V),
    Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
      ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
neg :
  ∀ (hx : x ∉ V),
    Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
      ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
by_cases hx : x ∈ V
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∈ V
⊢ Eq (α := ℤ) (if x ∈ V then (divisor f U : (a : 𝕜) → ℤ) x else 0 : ℤ) ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp [hf, hx, hf.mono_set hV, hV hx]

Premises used: MeromorphicOn.mono_set
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∉ V
⊢ Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
h : ∀ (x : 𝕜), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₁ + f₂) U)⁻ (divisor f₁ U)⁻

Tactic:
ext x
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
pos : ∀ (hx : x ∈ U), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
neg : ∀ (hx : x ∉ U), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
by_cases hx : x ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
this : max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]

Premises used: MeromorphicOn.add, negPart_def, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
pos : max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
      simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
pos :
  ∀ (h : 0 ≤ meromorphicOrderAt f₁ x),
    max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
neg :
  ∀ (h : ¬0 ≤ meromorphicOrderAt f₁ x),
    max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
by_cases h : 0 ≤ meromorphicOrderAt f₁ x

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
this : 0 ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
pos : 0 ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
⊢ 0 ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg

Premises used: AnalyticAt.meromorphicOrderAt_nonneg, le_inf
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt

Premises used: meromorphicOrderAt_add, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
⊢ 0 ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
calc 0
      _ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
        le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg
      _ ≤ meromorphicOrderAt (f₁ + f₂) x :=
        meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt

Premises used: meromorphicOrderAt_add, AnalyticAt.meromorphicOrderAt_nonneg, meromorphicOrderAt, le_inf, HAdd.hAdd, AnalyticAt.meromorphicAt, Min.min
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
this : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
rwa : max (-(meromorphicOrderAt f₁ x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
rwa₁ : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
rwa₂ : max (-(meromorphicOrderAt f₁ x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
rwa₃ rwa₄ rwa₅ : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]

Premises used: meromorphicOrderAt_add_eq_left_of_lt, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
neg : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0

Tactic:
suffices meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x by
        rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt f₁ x < 0

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ 0 ≤ meromorphicOrderAt f₂ x

Tactic:
(hf₂ x hx).meromorphicOrderAt_nonneg

Premises used: AnalyticAt.meromorphicOrderAt_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
calc : meromorphicOrderAt f₁ x < 0
⊢ meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x

Tactic:
calc meromorphicOrderAt f₁ x
      _ < 0 := by simpa using h
      _ ≤ meromorphicOrderAt f₂ x := (hf₂ x hx).meromorphicOrderAt_nonneg

Premises used: AnalyticAt.meromorphicOrderAt_nonneg, meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∉ U
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : AnalyticOnNhd 𝕜 f₁ U
hf₂ : MeromorphicOn f₂ U
rw : Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₂ + f₁) U)⁻ (divisor f₂ U)⁻
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₁ + f₂) U)⁻ (divisor f₂ U)⁻

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : AnalyticOnNhd 𝕜 f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₂ + f₁) U)⁻ (divisor f₂ U)⁻

Tactic:
negPart_divisor_add_of_analyticNhdOn_right hf₂ hf₁

Premises used: MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : AnalyticOnNhd 𝕜 f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₂ + f₁) U)⁻ (divisor f₂ U)⁻

Tactic:
exact negPart_divisor_add_of_analyticNhdOn_right hf₂ hf₁

Premises used: MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
pos : ∀ (hu : x ∈ U), Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
neg : ∀ (hu : x ∉ U), Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
by_cases hu : x ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
pos : (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x).untop₀ = untop₀ (↑0 : WithTop ℤ)
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) hu,
      ← untop₀_coe 0]

Premises used: MeromorphicOn.id, MeromorphicOn.const, MeromorphicOn.divisor_apply, WithTop.untop₀_coe, MeromorphicOn.fun_sub, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
pos : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x = (↑0 : WithTop ℤ)
⊢ (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x).untop₀ = untop₀ (↑0 : WithTop ℤ)

Tactic:
congr
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ MeromorphicAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ Ne.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x - z₀) x) 0 ∧
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, z - z₀ = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) ((fun (x : 𝕜) ↦ x - z₀) z)

Tactic:
simp [sub_ne_zero_of_ne hx]

Premises used: sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x = (↑0 : WithTop ℤ)

Tactic:
exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr
      ⟨(· - z₀), analyticAt_id.fun_sub analyticAt_const, by simp [sub_ne_zero_of_ne hx]⟩

Premises used: Iff.mpr, HSub.hSub, meromorphicOrderAt_eq_int_iff, analyticAt_const, analyticAt_id, And.intro, Exists.intro, AnalyticAt.fun_sub
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∉ U
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
Function.locallyFinsuppWithin.apply_eq_zero_of_notMem _ hu

Premises used: Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∉ U
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
exact Function.locallyFinsuppWithin.apply_eq_zero_of_notMem _ hu

Premises used: Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
rw : (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀).untop₀ = untop₀ (↑1 : WithTop ℤ)
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) z₀ : ℤ) (1 : ℤ)

Tactic:
rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) h, ← untop₀_coe 1]

Premises used: MeromorphicOn.id, MeromorphicOn.const, MeromorphicOn.divisor_apply, WithTop.untop₀_coe, MeromorphicOn.fun_sub, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
e_a : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀ = (↑1 : WithTop ℤ)
⊢ (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀).untop₀ = untop₀ (↑1 : WithTop ℤ)

Tactic:
congr
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ MeromorphicAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ Ne.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ (1 : 𝕜)) z₀) 0 ∧
    ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, z - z₀ = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - z₀) 1) ((fun (x : 𝕜) ↦ (1 : 𝕜)) z)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀ = (↑1 : WithTop ℤ)

Tactic:
exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr ⟨fun _ ↦ 1, analyticAt_const, by simp⟩

Premises used: Iff.mpr, meromorphicOrderAt_eq_int_iff, analyticAt_const, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h :
  ∀ (u : 𝕜),
    Membership.mem (γ := Set 𝕜)
        (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u ↔
      u ∈ support d
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) = support d

Tactic:
ext u
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h :
  Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u →
    u ∈ support d
h₁ :
  u ∈ support d →
    Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u
⊢ Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u ↔
    u ∈ support d

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h :
  Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u
⊢ ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) = 1

Tactic:
simp_all only [mem_mulSupport, ne_eq, mem_support]

Premises used: Function.mem_mulSupport, ne_eq, Function.mem_support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) = 1
h₁ : ∀ (hCon : d u = 0), False
⊢ ¬d u = 0

Tactic:
by_contra hCon
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) = 1
hCon : d u = 0
⊢ False

Tactic:
simp_all [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
h₁ : ∃ (a : 𝕜), ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) a = 1 a
⊢ Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u

Tactic:
simp_all only [mem_mulSupport, ne_eq, ne_iff]

Premises used: Function.mem_mulSupport, ne_eq, Function.ne_iff
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
h₁ : ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) u = 1 u
⊢ ∃ (a : 𝕜), ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) a = 1 a

Tactic:
use u
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) u = 1 u

Tactic:
simp_all [zero_zpow_eq_one₀]

Premises used: zero_zpow_eq_one₀
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
h₁ :
  ∀ (x : 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
      (∏ᶠ (u : 𝕜), (x - u) ^ d u)
⊢ Eq.{u_1 + 1} (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) fun (x : 𝕜) ↦
    ∏ᶠ (u : 𝕜), (x - u) ^ d u

Tactic:
ext x
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
h₁ :
  Eq (α := 𝕜) ((∏ i ∈ Finite.toFinset (s := support d) h, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - i) (d i)) x)
    (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ d i)
h₂ : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
h₃ :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) (∏ᶠ (u : 𝕜), (x - u) ^ d u)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset (s := h.toFinset),
    finprod_eq_prod_of_mulSupport_subset (s := h.toFinset)]

Premises used: finprod_eq_prod_of_mulSupport_subset