From dbea68061b9658d2b64131cf2c5e77fce2958eec Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 12 Sep 2024 07:04:00 +0200
Subject: [PATCH] Update analyticAt.lean

---
 Nevanlinna/analyticAt.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index 1d564bc..299b4e8 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -123,7 +123,7 @@ theorem eventually_nhds_comp_composition
     exact h₁t (ℓ y) hy
   · constructor
     · apply IsOpen.preimage
-      exact ContinuousLinearEquiv.continuous ℓ
+      exact hℓ
       exact h₂t
     · exact h₃t
 
@@ -132,9 +132,10 @@ theorem AnalyticAt.order_congr
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
   (hf₁ : AnalyticAt ℂ f₁ z₀)
-  (hf₂ : AnalyticAt ℂ f₂ z₀)
-  (hf : ∀ᶠ (z : ℂ) in nhds z₀, f₁ z = f₂ z) :
-  hf₁.order = hf₂.order := by
+  (hf : f₁ =ᶠ[nhds z₀] f₂) :
+  hf₁.order = (hf₁.congr hf).order := by
+
+
 
   sorry
 
@@ -151,9 +152,9 @@ theorem AnalyticAt.order_comp_CLE
     rw [AnalyticAt.order_eq_top_iff] at h₁f
     let A := eventually_nhds_comp_composition h₁f ℓ.continuous
     simp at A
-    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
 
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
     have : this.order = ⊤ := by
       rw [AnalyticAt.order_eq_top_iff]
       simp
@@ -176,7 +177,7 @@ theorem AnalyticAt.order_comp_CLE
       exact t₀
       apply AnalyticAt.comp h₁g
       exact ContinuousLinearEquiv.analyticAt ℓ z₀
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
     simp
 
     rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]