awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
simp_all :
  (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z,
      (t ∩
          Function.support (M := ℤ) fun (z : 𝕜) ↦
            if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0).Finite

Tactic:
simp_all only [Function.support_subset_iff, ne_eq, ite_eq_right_iff, WithTop.untop₀_eq_zero,
      and_imp, Classical.not_imp, not_or, implies_true,
      ← supportDiscreteWithin_iff_locallyFiniteWithin]

Premises used: and_imp, ne_eq, not_or, Function.support_subset_iff, supportDiscreteWithin_iff_locallyFiniteWithin, ite_eq_right_iff, Classical.not_imp, implies_true, WithTop.untop₀_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
pos :
  ∀ (hf : MeromorphicOn f U),
    (codiscreteWithin U).EventuallyEq (β := ℤ)
      (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
neg :
  ∀ (hf : ¬MeromorphicOn f U),
    (codiscreteWithin U).EventuallyEq (β := ℤ)
      (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
⊢ (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0

Tactic:
by_cases hf : MeromorphicOn f U

Premises used: MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
        (Set.image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})
        a →
      (if MeromorphicOn f U ∧ a ∈ U then (meromorphicOrderAt f a).untop₀ else 0) = 0 a
⊢ (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0

Tactic:
filter_upwards [mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
        hf.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top]

Premises used: MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, Iff.mp, mem_codiscrete_subtype_iff_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h :
  ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
⊢ ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
        (Set.image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})
        a →
      (if MeromorphicOn f U ∧ a ∈ U then (meromorphicOrderAt f a).untop₀ else 0) = 0 a

Tactic:
simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_left, exists_prop,
        exists_eq_right_right, Pi.ofNat_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero, and_imp]

Premises used: exists_eq_right_right, and_imp, Set.mem_image, Subtype.exists, exists_and_left, Pi.ofNat_apply, Set.mem_setOf_eq, exists_prop, ite_eq_right_iff, WithTop.untop₀_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h h₁ h₂ :
  ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₃ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₄ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₅ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₆ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₇ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₈ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₉ h₁₀ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₁₁ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
h₁₂ h₁₃ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
h₁₄ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
h₁₅ :
  ∀ a ∈ U,
    meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
⊢ ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U_1 : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0

Tactic:
simp [hf, Pi.zero_def]

Premises used: Pi.zero_def
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ (divisor f U : (a : 𝕜) → ℤ) z = if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : MeromorphicOn f U
hz : z ∈ U
⊢ (divisor f U : (a : 𝕜) → ℤ) z = (meromorphicOrderAt f z).untop₀

Tactic:
simp_all [MeromorphicOn.divisor_def]

Premises used: MeromorphicOn.divisor_def
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z : 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hz : z ∈ U
rw : (meromorphicOrderAt f z).untop₀ = WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z))
rw₁ rw₂ :
  Eq (α := ℤ) (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)))
    (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)))
⊢ Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ) (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)) : ℤ)

Tactic:
rw [hf.meromorphicOn.divisor_apply hz, (hf z hz).meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq, MeromorphicOn.divisor_apply, 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
h : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
pos : ∀ (hx : x ∈ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
neg : ∀ (hx : x ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((divisor 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
pos : (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin_of_eqOn_compl h₁ h₂]

Premises used: MeromorphicOn.congr_codiscreteWithin_of_eqOn_compl, MeromorphicOn.divisor_apply
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
pos : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀

Tactic:
congr 1
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
pos : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
apply meromorphicOrderAt_congr

Premises used: meromorphicOrderAt_congr
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x

Tactic:
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁

Premises used: Filter.Eventually, Filter.EventuallyEq, mem_codiscreteWithin, Filter.disjoint_principal_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₁ : MeromorphicOn f₁ U
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
h : ∀ (a : 𝕜) (ha : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ), f₁ a = f₂ a
⊢ f₁ =ᶠ[𝓝[≠] x] f₂

Tactic:
filter_upwards [h₁ x hx] with a ha
-- 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
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ
⊢ a ∈ U → f₁ a = f₂ a

Tactic:
simp at ha
-- 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
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ U → f₁ a = f₂ a
h : ∀ (ha : a ∉ U), f₁ a = f₂ a
h₃ : ∀ (ha : f₁ a = f₂ a), f₁ a = f₂ a
h₄ : ∀ (ha : a ∉ U), f₁ a = f₂ a
h₅ : ∀ (ha : f₁ a = f₂ a), f₁ a = f₂ a
h₆ : ∀ (ha : a ∉ U), f₁ a = f₂ a
h₇ : ∀ (ha : f₁ a = f₂ a), f₁ a = f₂ a
h₈ h₉ h₁₀ h₁₁ h₁₂ : ∀ (ha : a ∉ U), f₁ a = f₂ a
⊢ f₁ a = f₂ a

Tactic:
tauto
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∉ U
⊢ Eq (α := ℤ) ((divisor 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₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
h₁ : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)

Tactic:
ext z
-- 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
pos : ∀ (hz : z ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
neg : ∀ (hz : ¬z ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
by_cases hz : z ∉ 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∉ U
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)

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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : ¬z ∉ U
⊢ z ∈ U

Tactic:
rw [not_not] at hz

Premises used: Classical.not_not
-- 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
neg : (meromorphicOrderAt f₁ z).untop₀ = (meromorphicOrderAt f₂ z).untop₀
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz]

Premises used: MeromorphicOn.divisor_apply
-- 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
neg : meromorphicOrderAt f₁ z = meromorphicOrderAt f₂ z
⊢ (meromorphicOrderAt f₁ z).untop₀ = (meromorphicOrderAt f₂ z).untop₀

Tactic:
congr 1
-- 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
neg : f₁ =ᶠ[𝓝[≠] z] f₂
⊢ meromorphicOrderAt f₁ z = meromorphicOrderAt f₂ z

Tactic:
apply meromorphicOrderAt_congr

Premises used: meromorphicOrderAt_congr
-- 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₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ f₁ =ᶠ[𝓝[≠] z] f₂

Tactic:
apply (hf₁ z hz).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
    (hf₂ z hz) hz hU h

Premises used: MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
pos : ∀ (hf₁ : MeromorphicOn f₁ U), Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
neg : ∀ (hf₁ : ¬MeromorphicOn f₁ U), Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)

Tactic:
by_cases hf₁ : MeromorphicOn f₁ U

Premises used: 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
pos : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
pos : ∀ (hx : x ∈ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
neg : ∀ (hx : x ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((divisor 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
pos : (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]

Premises used: MeromorphicOn.congr_codiscreteWithin, MeromorphicOn.divisor_apply
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
pos : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀

Tactic:
congr 1
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
pos : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
apply meromorphicOrderAt_congr

Premises used: meromorphicOrderAt_congr
-- 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
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x

Tactic:
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
        disjoint_principal_right] at h₁

Premises used: Filter.Eventually, Filter.EventuallyEq, mem_codiscreteWithin, Filter.disjoint_principal_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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
apply : ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
⊢ U ∈ 𝓝[≠] x

Tactic:
apply mem_nhdsWithin.mpr

Premises used: Iff.mpr, mem_nhdsWithin
-- 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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
w : Set 𝕜
left : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
left₁ : x ∈ U
right : U ∩ {x}ᶜ ⊆ U
⊢ ∃ (u : Set 𝕜), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U

Tactic:
use U, h₂, hx, Set.inter_subset_left

Premises used: Set.inter_subset_left
-- 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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
⊢ U ∈ 𝓝[≠] x

Tactic:
have : U ∈ 𝓝[≠] x := by
        apply mem_nhdsWithin.mpr
        use U, h₂, hx, Set.inter_subset_left
-- 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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
h : ∀ (a : 𝕜) (h₁a : a ∈ U) (h₂a : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ), f₁ a = f₂ a
⊢ f₁ =ᶠ[𝓝[≠] x] f₂

Tactic:
filter_upwards [this, h₁ x hx] with a h₁a h₂a
-- 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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ
⊢ a ∈ U → ¬¬f₁ a = f₂ a

Tactic:
simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a

Premises used: Set.mem_setOf_eq, Set.mem_diff, not_and, Set.mem_compl_iff
-- 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
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
h₂a : a ∈ U → ¬¬f₁ a = f₂ a
h : ∀ (h₂a : a ∉ U), f₁ a = f₂ a
h₃ h₄ h₅ : ∀ (h₂a : ¬¬f₁ a = f₂ a), f₁ a = f₂ a
h₆ h₇ h₈ : ∀ (h₂a : f₁ a = f₂ a), f₁ a = f₂ a
⊢ f₁ a = f₂ a

Tactic:
tauto