From 46740a0f17fc1c2064016592ab54a9e5185bb3dc Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 26 Nov 2024 14:14:03 +0100 Subject: [PATCH] Update stronglyMeromorphicOn_eliminate.lean --- Nevanlinna/stronglyMeromorphicOn_eliminate.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index a67a66d..33fef88 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -304,11 +304,8 @@ theorem MeromorphicOn.decompose₃ ∧ (∀ u : U, g u ≠ 0) ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by - have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by - apply MeromorphicOn.order_ne_top h₂U h₁f h₂f - - have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by - exact h₁f.meromorphicOn.divisor.finiteSupport h₁U + have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f + have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset