diff --git a/PersistentDecomp.lean b/PersistentDecomp.lean
index e808a5e..00f1107 100644
--- a/PersistentDecomp.lean
+++ b/PersistentDecomp.lean
@@ -1,8 +1,8 @@
 import PersistentDecomp.BumpFunctor
-import PersistentDecomp.DirectSumDecomposition
+import PersistentDecomp.DirectSumDecompositionDual
 import PersistentDecomp.Mathlib.Algebra.DirectSum.Basic
 import PersistentDecomp.Mathlib.Algebra.Module.Submodule.Map
-import PersistentDecomp.Mathlib.Data.DFinsupp.Basic
+import PersistentDecomp.Mathlib.Data.DFinsupp.BigOperators
 import PersistentDecomp.Mathlib.Order.Disjoint
 import PersistentDecomp.Mathlib.Order.Interval.Basic
 import PersistentDecomp.Mathlib.Order.SupIndep
diff --git a/PersistentDecomp/DirectSumDecomposition.lean b/PersistentDecomp/DirectSumDecomposition.lean
index c0dbcfd..8118c46 100644
--- a/PersistentDecomp/DirectSumDecomposition.lean
+++ b/PersistentDecomp/DirectSumDecomposition.lean
@@ -14,7 +14,7 @@ variable (M) in
 @[ext]
 structure DirectSumDecomposition where
   carrier : Set (PersistenceSubmodule M)
-  setIndependent' : SetIndependent carrier
+  sSupIndep' : sSupIndep carrier
   sSup_eq_top' : sSup carrier = ⊤
   --(h : ∀ (x : C), DirectSum.IsInternal (M := M.obj x) (S := Submodule K (M.obj x))
     --(fun (p : PersistenceSubmodule M) (hp : p ∈ S) => p  x))
@@ -24,12 +24,12 @@ namespace DirectSumDecomposition
 
 instance : SetLike (DirectSumDecomposition M) (PersistenceSubmodule M) where
   coe := carrier
-  coe_injective' D₁ D₂ := by cases D₁; cases D₂; sorry
+  coe_injective' D₁ := by cases D₁; congr!
 
 attribute [-instance] SetLike.instPartialOrder
 
-lemma setIndependent (D : DirectSumDecomposition M) : SetIndependent (SetLike.coe D) :=
-  D.setIndependent'
+protected lemma sSupIndep (D : DirectSumDecomposition M) : sSupIndep (SetLike.coe D) :=
+  D.sSupIndep'
 
 lemma sSup_eq_top (D : DirectSumDecomposition M) : sSup (SetLike.coe D) = ⊤ := D.sSup_eq_top'
 lemma not_bot_mem (D : DirectSumDecomposition M) : ⊥ ∉ D := D.not_bot_mem'
@@ -40,7 +40,7 @@ lemma pointwise_sSup_eq_top (D : DirectSumDecomposition M) (x : C) : ⨆ p ∈ D
 
 lemma isInternal (I : DirectSumDecomposition M) (c : C) :
     IsInternal (M := M.obj c) (S := Submodule K (M.obj c)) fun p : I ↦ p.val c := by
-  rw [DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top]
+  rw [DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]
   constructor
   sorry
   sorry
@@ -108,7 +108,7 @@ lemma RefinementMapSurj' (I : DirectSumDecomposition M) (J : DirectSumDecomposit
     rcases h_contra with ⟨A, h₁, h₂⟩
     exact (h_not_le (⟨A, h₁⟩) h₂)
   have h_disj : Disjoint N₀.val (sSup B) := by
-    exact (SetIndependent.disjoint_sSup J.setIndependent' N₀.prop h_sub h_aux')
+    exact (sSupIndep.disjoint_sSup J.sSupIndep' N₀.prop h_sub h_aux')
   have h_not_bot : N₀.val ≠ ⊥ := by
     intro h_contra
     exact J.not_bot_mem (h_contra ▸ N₀.prop)
@@ -184,7 +184,7 @@ instance DirectSumDecompLE : PartialOrder (DirectSumDecomposition M) where
       have h_mem : A.val ∈ B := by
         by_contra h_A_not_mem
         have h_aux : Disjoint A.val (sSup B) := by
-          exact (I.setIndependent.disjoint_sSup A.prop h_B₂ h_A_not_mem)
+          exact (I.sSupIndep.disjoint_sSup A.prop h_B₂ h_A_not_mem)
         have h_aux' : sSup B ≤ A.val := h_B₁ ▸ h_N_le_A
         have h_last : sSup B = (⊥ : PersistenceSubmodule M) := by
           rw [disjoint_comm] at h_aux
@@ -212,10 +212,10 @@ If `D` is a direct sum decomposition of `M` and for each `N` appearing in `S` we
 sum decomposition of `N`, we can construct a refinement of `D`.
 -/
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
-    (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where
   carrier := ⋃ N, ⋃ hN, B N hN
-  setIndependent' x hx a ha ha' := by
+  sSupIndep' x hx a ha ha' := by
     sorry
   sSup_eq_top' := by
     sorry
@@ -223,13 +223,13 @@ def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
 
 lemma refinement_le (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN))
-    (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) :
     refinement B hB hB' hB'' ≤ D := sorry
 
 lemma refinement_lt_of_exists_ne_singleton (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN))
-    (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN)
     (H : ∃ (N : PersistenceSubmodule M) (hN : N ∈ D), B N hN ≠ {N}) :
     refinement B hB hB' hB'' < D := sorry
diff --git a/PersistentDecomp/DirectSumDecompositionDual.lean b/PersistentDecomp/DirectSumDecompositionDual.lean
index b58a5f3..f7ef97b 100644
--- a/PersistentDecomp/DirectSumDecompositionDual.lean
+++ b/PersistentDecomp/DirectSumDecompositionDual.lean
@@ -14,7 +14,7 @@ variable (M) in
 @[ext]
 structure DirectSumDecomposition where
   carrier : Set (PersistenceSubmodule M)
-  setIndependent' : SetIndependent carrier
+  sSupIndep' : sSupIndep carrier
   sSup_eq_top' : sSup carrier = ⊤
   --(h : ∀ (x : C), DirectSum.IsInternal (M := M.obj x) (S := Submodule K (M.obj x))
     --(fun (p : PersistenceSubmodule M) (hp : p ∈ S) => p  x))
@@ -24,12 +24,11 @@ namespace DirectSumDecomposition
 
 instance : SetLike (DirectSumDecomposition M) (PersistenceSubmodule M) where
   coe := carrier
-  coe_injective' D₁ D₂ := by cases D₁; cases D₂; sorry
+  coe_injective' D₁ D₂ := by cases D₁; congr!
 
 attribute [-instance] SetLike.instPartialOrder
 
-lemma setIndependent (D : DirectSumDecomposition M) : SetIndependent (SetLike.coe D) :=
-  D.setIndependent'
+protected lemma sSupIndep (D : DirectSumDecomposition M) : sSupIndep (SetLike.coe D) := D.sSupIndep'
 
 lemma sSup_eq_top (D : DirectSumDecomposition M) : sSup (SetLike.coe D) = ⊤ := D.sSup_eq_top'
 lemma not_bot_mem (D : DirectSumDecomposition M) : ⊥ ∉ D := D.not_bot_mem'
@@ -40,7 +39,7 @@ lemma pointwise_sSup_eq_top (D : DirectSumDecomposition M) (x : C) : ⨆ p ∈ D
 
 lemma isInternal (I : DirectSumDecomposition M) (c : C) :
     IsInternal (M := M.obj c) (S := Submodule K (M.obj c)) fun p : I ↦ p.val c := by
-  rw [DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top]
+  rw [DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]
   constructor
   sorry
   sorry
@@ -108,7 +107,7 @@ lemma RefinementMapSurj' (I : DirectSumDecomposition M) (J : DirectSumDecomposit
     rcases h_contra with ⟨A, h₁, h₂⟩
     exact (h_not_le (⟨A, h₁⟩) h₂)
   have h_disj : Disjoint N₀.val (sSup B) := by
-    exact (SetIndependent.disjoint_sSup J.setIndependent' N₀.prop h_sub h_aux')
+    exact (sSupIndep.disjoint_sSup J.sSupIndep' N₀.prop h_sub h_aux')
   have h_not_bot : N₀.val ≠ ⊥ := by
     intro h_contra
     exact J.not_bot_mem (h_contra ▸ N₀.prop)
@@ -156,7 +155,7 @@ lemma UniqueGE (I : DirectSumDecomposition M) (J : DirectSumDecomposition M)
       exact (h_mem ▸ A.prop)
       subst X
       exact B.prop
-    exact (CompleteLattice.setIndependent_pair h_neq').mp (CompleteLattice.SetIndependent.mono I.setIndependent' h_sub)
+    exact (sSupIndep_pair h_neq').mp (sSupIndep.mono I.sSupIndep' h_sub)
   have h_le' : N.val ≤ A.val ⊓ B.val := by
     apply le_inf
     exact h_le.1
@@ -270,7 +269,7 @@ instance DirectSumDecompLE : PartialOrder (DirectSumDecomposition M) where
       have h_mem : A.val ∈ B := by
         by_contra h_A_not_mem
         have h_aux : Disjoint A.val (sSup B) := by
-          exact (I.setIndependent.disjoint_sSup A.prop h_B₂ h_A_not_mem)
+          exact (I.sSupIndep.disjoint_sSup A.prop h_B₂ h_A_not_mem)
         have h_aux' : sSup B ≤ A.val := h_B₁ ▸ h_N_le_A
         have h_last : sSup B = (⊥ : PersistenceSubmodule M) := by
           rw [disjoint_comm] at h_aux
@@ -298,10 +297,10 @@ If `D` is a direct sum decomposition of `M` and for each `N` appearing in `S` we
 sum decomposition of `N`, we can construct a refinement of `D`.
 -/
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
-    (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where
   carrier := ⋃ N, ⋃ hN, B N hN
-  setIndependent' x hx a ha ha' := by
+  sSupIndep' x hx a ha ha' := by
     sorry
   sSup_eq_top' := by
     sorry
@@ -309,13 +308,13 @@ def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
 
 lemma refinement_le (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN))
-    (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) :
     refinement B hB hB' hB'' ≤ D := sorry
 
 lemma refinement_lt_of_exists_ne_singleton (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN))
-    (hB' : ∀ N hN, SetIndependent (B N hN))
+    (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN)
     (H : ∃ (N : PersistenceSubmodule M) (hN : N ∈ D), B N hN ≠ {N}) :
     refinement B hB hB' hB'' < D := sorry
diff --git a/PersistentDecomp/Mathlib/Data/DFinsupp/Basic.lean b/PersistentDecomp/Mathlib/Data/DFinsupp/BigOperators.lean
similarity index 90%
rename from PersistentDecomp/Mathlib/Data/DFinsupp/Basic.lean
rename to PersistentDecomp/Mathlib/Data/DFinsupp/BigOperators.lean
index 05829aa..47a111c 100644
--- a/PersistentDecomp/Mathlib/Data/DFinsupp/Basic.lean
+++ b/PersistentDecomp/Mathlib/Data/DFinsupp/BigOperators.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.DFinsupp.Basic
+import Mathlib.Data.DFinsupp.BigOperators
 
 @[to_additive (attr := simp)]
 lemma SubmonoidClass.coe_dfinsuppProd {B ι N : Type*} {M : ι → Type*} [DecidableEq ι]
diff --git a/PersistentDecomp/Mathlib/Order/SupIndep.lean b/PersistentDecomp/Mathlib/Order/SupIndep.lean
index 8e49748..a597703 100644
--- a/PersistentDecomp/Mathlib/Order/SupIndep.lean
+++ b/PersistentDecomp/Mathlib/Order/SupIndep.lean
@@ -4,5 +4,5 @@ open CompleteLattice
 
 variable {ι κ α : Type*} [CompleteLattice α] {f : ι → κ → α}
 
-lemma Pi.iSupIndepIndep_iff : Independent f ↔ ∀ k, Independent (f · k) := by
-  simpa [Independent, Pi.disjoint_iff] using forall_swap
+lemma Pi.iSupIndep_iff : iSupIndep f ↔ ∀ k, iSupIndep (f · k) := by
+  simpa [iSupIndep, Pi.disjoint_iff] using forall_swap
diff --git a/PersistentDecomp/step_2.lean b/PersistentDecomp/step_2.lean
index aa50d13..1c2ce09 100644
--- a/PersistentDecomp/step_2.lean
+++ b/PersistentDecomp/step_2.lean
@@ -94,7 +94,7 @@ lemma isInternal_chainBound (hT : IsChain LE.le T) (c : C) : IsInternal fun l :
 
 /-- The `M[λ]` are linearly independent -/
 lemma lambdas_indep (hT : IsChain LE.le T) :
-    CompleteLattice.SetIndependent {M[l] | (l : L T) (_ : ¬ IsBot M[l])} := by
+    sSupIndep {M[l] | (l : L T) (_ : ¬ IsBot M[l])} := by
   intro a b ha hb hab
   sorry
 
@@ -107,7 +107,7 @@ lemma sSup_lambdas_eq_top (hT : IsChain LE.le T) :
 def DirectSumDecomposition_of_chain (hT : IsChain LE.le T) : DirectSumDecomposition M where
   carrier := {M[l] | (l : L T) (_ : ¬ IsBot M[l])}
   sSup_eq_top' := sSup_lambdas_eq_top hT
-  setIndependent' := lambdas_indep hT
+  sSupIndep' := lambdas_indep hT
   not_bot_mem' := sorry
 
 /-- The set `𝓤` is an upper bound for the chain `T` -/
diff --git a/lake-manifest.json b/lake-manifest.json
index 139be4b..3421e93 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "af731107d531b39cd7278c73f91c573f40340612",
+   "rev": "44e2d2e643fd2618b01f9a0592d7dcbd3ffa22de",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ac7b989cbf99169509433124ae484318e953d201",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,11 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "594b4bcc3cc06910b4838114317b1153f497be17",
+   "rev": "c4f307606793b52847c977499c58d745bc2186d3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
- "name": "PH_formalisation",
+ "name": "PersistentDecomp",
  "lakeDir": ".lake"}