awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
have rw : (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ ∈ 𝓝[≠] x
Tactic: rw [disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ ∈ 𝓝[≠] x
have apply : {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y) x} ⊆ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
Tactic: apply Filter.mem_of_superset ((h x hx).eventually_analyticAt)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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}ᶜ ∩ U).Countable
have apply : {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜᶜ ∈ codiscreteWithin U
Tactic: apply (HereditarilyLindelofSpace.isLindelof _).countable_of_isDiscrete
    (isDiscrete_of_codiscreteWithin _)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ MeromorphicOn f univ ↔ Meromorphic f
have mp : MeromorphicOn f univ → Meromorphic f
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicOn f univ ↔ Meromorphic f
have mpr : Meromorphic f → MeromorphicOn f univ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicOn f univ ↔ Meromorphic f
have mp₃ : MeromorphicOn f univ → ∀ (x : 𝕜), MeromorphicAt f x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicOn f univ ↔ Meromorphic f
have mpr₃ : Meromorphic f → ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) univ x → MeromorphicAt f x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ Meromorphic g
have rw : ∀ (hf : MeromorphicOn f univ) (h₁ : f =ᶠ[codiscrete 𝕜] g), MeromorphicOn g univ
Tactic: rw [← meromorphicOn_univ] at *
Cleared hypotheses: hf, h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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}
⊢ Measurable f
have h₁ : sᶜ.Countable
Tactic: have h₁ : sᶜ.Countable := by simpa using h.countable_compl_analyticAt
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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
⊢ Measurable f
have h₁' : Countable.{u_1 + 1} (↑sᶜ : Type u_1)
Tactic: have h₁' := h₁.to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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)
⊢ Measurable f
have h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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
⊢ Measurable f
have h₃ : ContinuousOn f s
Tactic: have h₃ : ContinuousOn f s := fun z hz ↦ hz.continuousAt.continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ z ∈ U
have by_contra : ∀ (h₂z : z ∉ U), False
Tactic: by_contra h₂z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 𝕜
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z,
      (t ∩
          Function.support (M := ℤ) fun (z : 𝕜) ↦
            if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0).Finite
have simp_all : (codiscreteWithin U).EventuallyEq (β := ℤ)
  (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 𝕜
⊢ (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
have pos : ∀ (hf : MeromorphicOn f U),
  (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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ (codiscreteWithin U).EventuallyEq (β := ℤ)
    (fun (z : 𝕜) ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) 0
have neg : ∀ (hf : ¬MeromorphicOn f U),
  (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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
have 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
Tactic: filter_upwards [mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
        hf.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ ∀ (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
have h : ∀ (a : 𝕜),
  meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
    a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f 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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 = ⊤
⊢ ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
have h₃ : ∀ a ∈ U,
  meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 = ⊤
⊢ ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
have h₄ : ∀ a ∈ U,
  meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 = ⊤
⊢ ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
have h₁₁ : ∀ a ∈ U,
  meromorphicOrderAt f a = 0 → MeromorphicOn f U → a ∈ U → ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 = ⊤
⊢ ∀ (a : 𝕜),
    meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤ →
      a ∈ U → MeromorphicOn f U → a ∈ U → meromorphicOrderAt f a = 0 ∨ meromorphicOrderAt f a = ⊤
have h₁₄ : ∀ a ∈ U,
  meromorphicOrderAt f a = ⊤ → MeromorphicOn f U → a ∈ U → ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ) (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)) : ℤ)
have rw : (meromorphicOrderAt f z).untop₀ = WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z))
Tactic: rw [hf.meromorphicOn.divisor_apply hz, (hf z hz).meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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))
⊢ Eq (α := ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ) (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)) : ℤ)
have rw₁ : Eq (α := ℤ) (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)))
  (WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f z)))
Tactic: rw [hf.meromorphicOn.divisor_apply hz, (hf z hz).meromorphicOrderAt_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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ᶜ
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have h : ∀ (x : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 : 𝕜
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) x : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 : ℤ)
have pos : (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
Tactic: simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin_of_eqOn_compl h₁ h₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ (meromorphicOrderAt f₁ x).untop₀ = (meromorphicOrderAt f₂ x).untop₀
have pos : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have pos : f₁ =ᶠ[𝓝[≠] x] f₂
Tactic: apply meromorphicOrderAt_congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
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
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
have h₃ : ∀ x ∈ U, (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
have h : ∀ (a : 𝕜) (ha : a ∈ (U \ {x : 𝕜 | f₁ x = f₂ x})ᶜ), f₁ a = f₂ a
Tactic: filter_upwards [h₁ x hx] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
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})ᶜ
⊢ f₁ a = f₂ a
have ha₁ : a ∈ U → f₁ a = f₂ a
Tactic: simp at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ f₁ a = f₂ a
have h : ∀ (ha : a ∉ U), f₁ a = f₂ a
Tactic: tauto
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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
⊢ f₁ a = f₂ a
have h₃ : ∀ (ha : f₁ a = f₂ a), f₁ a = f₂ a
Tactic: tauto
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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₂
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have h₁ : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 : 𝕜
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∉ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : ¬z ∉ U), Eq (α := ℤ) ((divisor f₁ U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f₂ U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∉ U