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

---
 Nevanlinna/analyticAt.lean | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index 299b4e8..afbb8da 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -135,9 +135,22 @@ theorem AnalyticAt.order_congr
   (hf : f₁ =ᶠ[nhds z₀] f₂) :
   hf₁.order = (hf₁.congr hf).order := by
 
-
-
-  sorry
+  by_cases h₁f₁ : hf₁.order = ⊤
+  rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
+  rw [AnalyticAt.order_eq_top_iff] at h₁f₁
+  exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
+  --
+  let n := hf₁.order.toNat
+  have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
+  rw [hn, eq_comm, AnalyticAt.order_eq_nat_iff]
+  rw [AnalyticAt.order_eq_nat_iff] at hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
+  use g
+  constructor
+  · assumption
+  · constructor
+    · assumption
+    · exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
 
 
 theorem AnalyticAt.order_comp_CLE
@@ -154,7 +167,8 @@ theorem AnalyticAt.order_comp_CLE
     simp at A
     rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
 
-    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
+      apply analyticAt_const
     have : this.order = ⊤ := by
       rw [AnalyticAt.order_eq_top_iff]
       simp