diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index b0bba43..e9a0b0b 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -36,11 +36,15 @@ theorem MeromorphicOn.decompose
     ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) U) := by
 
   let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
-  have h₁g₁ : MeromorphicOn g₁ U := by sorry
+  have h₁g₁ : MeromorphicOn g₁ U := by
+    sorry
   let g := h₁g₁.makeStronglyMeromorphicOn
-  have h₁g : MeromorphicOn g U := by sorry
-  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by sorry
-  have h₃g : StronglyMeromorphicOn g U := by sorry
+  have h₁g : MeromorphicOn g U := by
+    sorry
+  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
+    sorry
+  have h₃g : StronglyMeromorphicOn g U := by
+    sorry
   have h₄g : AnalyticOnNhd ℂ g U := by
     intro z hz
     apply StronglyMeromorphicAt.analytic (h₃g z hz)
@@ -51,10 +55,8 @@ theorem MeromorphicOn.decompose
   · constructor
     · intro z hz
       rw [← (h₄g z hz).order_eq_zero_iff]
-
       have A := (h₄g z hz).meromorphicAt_order
       rw [h₂g ⟨z, hz⟩] at A
-
       have t₀ : (h₄g z hz).order ≠ ⊤ := by
         by_contra hC
         rw [hC] at A