Delete 884838fd-52e4-4608-80c9-73a896264eae-output.lean

884838fd-52e4-4608-80c9-73a896264eae-output.lean

@@ -1,92 +0,0 @@
-/-
-This file was edited by Aristotle.
-
-Lean version: leanprover/lean4:v4.24.0
-Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
-
-The following was proved by Aristotle:
-
-- lemma meromorphic_measurable {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) :
-    Measurable f
--/
-
-import Mathlib
-
-
-open MeromorphicOn Real Set Classical Topology
-
-noncomputable section AristotleLemmas
-
-#check MeromorphicAt
-
-#check MeromorphicAt.eventually_analyticAt
-#check AnalyticAt.continuousAt
-#check Set.Countable.measurableSet
-#check Measurable.piecewise
-
-lemma measurable_of_continuousOn_open_of_countable_closed {f : ℂ → ℂ} {U : Set ℂ}
-    (hU : IsOpen U) (h_count : Uᶜ.Countable) (h_cont : ContinuousOn f U) : Measurable f := by
-  -- Assume the contrary, that $f$ is not measurable.
-  by_contra h_not_measurable;
-  -- Since $f$ is not measurable, there exists an open set $V$ such that $f^{-1}(V)$ is not measurable.
-  obtain ⟨V, hV_open, hV_not_meas⟩ : ∃ V : Set ℂ, IsOpen V ∧ ¬ MeasurableSet (f ⁻¹' V) := by
-    -- By definition of measurability, if $f$ is not measurable, then there exists an open set $V$ such that $f^{-1}(V)$ is not measurable.
-    have h_not_measurable_def : ¬(∀ V : Set ℂ, IsOpen V → MeasurableSet (f ⁻¹' V)) := by
-      exact fun h => h_not_measurable <| measurable_of_isOpen h;
-    aesop;
-  -- Since $f$ is continuous on $U$, the preimage of any open set under $f|_U$ is open in $U$, hence measurable.
-  have h_preimage_U_meas : MeasurableSet (f ⁻¹' V ∩ U) := by
-    -- The preimage of an open set under a continuous function is open.
-    have h_preimage_open : IsOpen (f ⁻¹' V ∩ U) := by
-      rw [ isOpen_iff_mem_nhds ] at * ; aesop;
-      exact h_cont.continuousAt ( hU x right ) |> fun h => h.tendsto.eventually ( hV_open _ left );
-    exact h_preimage_open.measurableSet;
-  -- Since $U^c$ is countable, the preimage $f^{-1}(V)$ can be written as the union of $f^{-1}(V) \cap U$ and $f^{-1}(V) \cap U^c$.
-  have h_preimage_union : f ⁻¹' V = (f ⁻¹' V ∩ U) ∪ (f ⁻¹' V ∩ Uᶜ) := by
-    rw [ ← Set.inter_union_distrib_left, Set.union_compl_self, Set.inter_univ ];
-  -- Since $U^c$ is countable, the preimage $f^{-1}(V) \cap U^c$ is also countable.
-  have h_preimage_Uc_countable : Set.Countable (f ⁻¹' V ∩ Uᶜ) := by
-    exact h_count.mono fun x hx => hx.2;
-  exact hV_not_meas <| h_preimage_union.symm ▸ MeasurableSet.union h_preimage_U_meas ( h_preimage_Uc_countable.measurableSet )
-
-end AristotleLemmas
-
-lemma meromorphic_measurable {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) :
-    Measurable f := by
-  -- The set of singularities of a meromorphic function is countable.
-  have h_countable : Set.Countable {z : ℂ | ¬AnalyticAt ℂ f z} := by
-    -- Let $S$ be the set of points where $f$ is not analytic. For each $z \in S$, there exists a neighborhood around $z$ where $f$ is analytic except at $z$.
-    set S := {z : ℂ | ¬AnalyticAt ℂ f z}
-    have h_discrete : ∀ z ∈ S, ∃ ε > 0, ∀ w ∈ Metric.ball z ε, w ≠ z → AnalyticAt ℂ f w := by
-      -- Since $f$ is meromorphic on the entire complex plane, for any $z \in S$, there exists an $\epsilon > 0$ such that $f$ is analytic on the punctured disk around $z$ (excluding $z$ itself).
-      have h_meromorphic : ∀ z ∈ S, ∃ ε > 0, ∀ w ∈ Metric.ball z ε, w ≠ z → AnalyticAt ℂ f w := by
-        intro z hz
-        have h_meromorphic_at_z : MeromorphicAt f z := by
-          exact?
-        -- By definition of MeromorphicAt, there exists a neighborhood around z where f is analytic except at z itself.
-        have h_neighborhood : ∀ᶠ w in 𝓝[≠] z, AnalyticAt ℂ f w := by
-          exact?;
-        rw [ eventually_nhdsWithin_iff ] at h_neighborhood;
-        rw [ Metric.eventually_nhds_iff ] at h_neighborhood; aesop;
-      assumption;
-    -- Since $S$ is discrete, it is countable.
-    have h_countable : DiscreteTopology S := by
-      -- To show that S is discrete, we use the fact that for each z in S, there exists an ε > 0 such that the ball around z with radius ε contains no other points of S except z itself.
-      have h_discrete : ∀ z ∈ S, ∃ ε > 0, Metric.ball z ε ∩ S = {z} := by
-        exact fun z hz => by obtain ⟨ ε, ε_pos, hε ⟩ := h_discrete z hz; exact ⟨ ε, ε_pos, Set.eq_singleton_iff_unique_mem.mpr ⟨ ⟨ Metric.mem_ball_self ε_pos, hz ⟩, fun w hw => Classical.not_not.1 fun hw' => hw.2 <| hε w hw.1 hw' ⟩ ⟩ ;
-      refine' singletons_open_iff_discrete.mp _;
-      intro z; specialize h_discrete z z.2; aesop;
-      rw [ Set.eq_singleton_iff_unique_mem ] at right ; aesop;
-      exact ⟨ Metric.ball val w, Metric.isOpen_ball, by ext ⟨ x, hx ⟩ ; specialize right x; aesop ⟩;
-    exact Set.countable_coe_iff.mp ( by exact? );
-  -- Since $U$ is open and $f$ is continuous on $U$, and the complement of $U$ is countable, we can apply the lemma to conclude that $f$ is measurable.
-  have h_measurable : Measurable f := by
-    have hU : IsOpen {z : ℂ | AnalyticAt ℂ f z} := by
-      exact?
-    have h_cont : ContinuousOn f {z : ℂ | AnalyticAt ℂ f z} := by
-      exact fun x hx => hx.continuousAt.continuousWithinAt
-    have h_count : {z : ℂ | ¬AnalyticAt ℂ f z}.Countable := by
-      -- Apply the fact that the set of points where f is not analytic is countable.
-      exact h_countable
-    exact measurable_of_continuousOn_open_of_countable_closed hU h_count h_cont;
-  exact h_measurable