diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index bfbef39..40f66e7 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -139,12 +139,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
   rcases hh with ⟨N,ss⟩
   sorry
 
-
-
-
-
--- set_option pp.all true in
--- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), 
     (N ≤ n → f n = c) ∧ c ≠ 0) := by
   constructor
@@ -172,28 +166,16 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
       => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) 
       (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩
 
-
-
-
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
 
-
-
 -- Δ of 1 times decreaes the polynomial type by one
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by
   sorry
 
-
-
-
 lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
   sorry
 
-
-
-
-
 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
 lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
   induction' d with d hd
@@ -214,19 +196,7 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
       tauto
     tauto
 
-
-
-lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
-  intro h
-  have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by 
-    exact foofoo
-  specialize this d f
-  tauto
-
-
-
-
-
+lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
@@ -248,8 +218,6 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n
   -- Induction step
   · sorry
 
-
-
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0
 lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), ((N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0)) := by
@@ -263,41 +231,14 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃
   exact this1
 end
 
-
-
-
-
-
-
-
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section
--- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
---   (f : M →[R] N)
 open LinearMap
--- variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
--- noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
-
 
 -- Definitiion of the length of a module
 noncomputable def length (R M : Type _) [CommRing R] [AddCommGroup M] [Module R M] := Set.chainHeight {M' : Submodule R M | M' < ⊤}
 #check length ℤ ℤ
--- #eval length ℤ ℤ
-
-
--- @[ext]
--- structure SES (R : Type _) [CommRing R] where
---   A : Type _
---   B : Type _
---   C : Type _
---   f : A →ₗ[R] B
---   g : B →ₗ[R] C
--- left_exact : LinearMap.ker f = 0
--- middle_exact : LinearMap.range f = LinearMap.ker g
--- right_exact : LinearMap.range g = C
-
-
 
 -- Definition of a SES (Short Exact Sequence)
 -- @[ext]
@@ -309,10 +250,6 @@ structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B]
   middle_exact : LinearMap.range f = LinearMap.ker g
   right_exact : LinearMap.range g = ⊤
 
-#check SES.right_exact
-#check SES
-
-
 -- Additive lemma
 lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] 
   (f : A →ₗ[R] B) (g : B →ₗ[R] C)
@@ -321,11 +258,4 @@ lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommG
   rcases h with ⟨left_exact, middle_exact, right_exact⟩
   sorry
 
-end section
-
-
-
-
-
-
-
+end section
\ No newline at end of file