diff --git a/DividedPowers/DPAlgebra/BaseChange.lean b/DividedPowers/DPAlgebra/BaseChange.lean
index 200508b..3330b92 100644
--- a/DividedPowers/DPAlgebra/BaseChange.lean
+++ b/DividedPowers/DPAlgebra/BaseChange.lean
@@ -1,11 +1,5 @@
---import DividedPowers.DPAlgebra.Init
 import DividedPowers.DPAlgebra.Exponential
 import DividedPowers.DPAlgebra.Graded.Basic
-import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
-import DividedPowers.PolynomialMap.Homogeneous
---import DividedPowers.DPAlgebra.Misc
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.TensorProduct.Basic
 
 -- import DividedPowers.ForMathlib.RingTheory.TensorProduct
diff --git a/DividedPowers/DPAlgebra/Envelope.lean b/DividedPowers/DPAlgebra/Envelope.lean
index 8571a54..aa7fa82 100644
--- a/DividedPowers/DPAlgebra/Envelope.lean
+++ b/DividedPowers/DPAlgebra/Envelope.lean
@@ -1,4 +1,5 @@
 import DividedPowers.DPAlgebra.Compatible
+import Mathlib.Data.Rel
 
 universe u v w
 
@@ -357,6 +358,7 @@ lemma isCompatibleWith [Nontrivial B] [DecidableEq B]
     true_and]
     sorry -/
 
+
 #exit
 
 -- End of case 1
@@ -589,5 +591,3 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
   simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
     MonoidHom.coe_coe]
   rw [← hφ_unique β hβ]
-
-#min_imports
diff --git a/DividedPowers/DPAlgebra/Exponential.lean b/DividedPowers/DPAlgebra/Exponential.lean
index 98c3d58..00dc0bd 100644
--- a/DividedPowers/DPAlgebra/Exponential.lean
+++ b/DividedPowers/DPAlgebra/Exponential.lean
@@ -136,3 +136,6 @@ theorem dividedPowerAlgebra_exponentialModule_equiv_symm_apply
       = coeff S n (β m) := by
   unfold dividedPowerAlgebra_exponentialModule_equiv
   simp only [Equiv.coe_fn_symm_mk, lift'AlgHom_apply_dp]
+
+
+#min_imports
diff --git a/DividedPowers/DPAlgebra/Graded/Basic.lean b/DividedPowers/DPAlgebra/Graded/Basic.lean
index 83a4c98..23aab8f 100644
--- a/DividedPowers/DPAlgebra/Graded/Basic.lean
+++ b/DividedPowers/DPAlgebra/Graded/Basic.lean
@@ -1,5 +1,7 @@
 import DividedPowers.DPAlgebra.Init
 import DividedPowers.ForMathlib.GradedRingQuot
+import Mathlib.Algebra.MvPolynomial.CommRing
+
 
 noncomputable section
 
diff --git a/DividedPowers/DPAlgebra/Init.lean b/DividedPowers/DPAlgebra/Init.lean
index ba399be..5fa1458 100644
--- a/DividedPowers/DPAlgebra/Init.lean
+++ b/DividedPowers/DPAlgebra/Init.lean
@@ -5,11 +5,6 @@
 import DividedPowers.Basic
 import DividedPowers.DPAlgebra.Misc
 
-import Mathlib.Algebra.RingQuot
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.Data.Rel
-import Mathlib.RingTheory.Ideal.Quotient
-
 noncomputable section
 
 open Finset MvPolynomial Ideal.Quotient
@@ -544,5 +539,3 @@ end Functoriality
 end DividedPowerAlgebra
 
 end
-
---#lint
diff --git a/DividedPowers/DPAlgebra/Misc.lean b/DividedPowers/DPAlgebra/Misc.lean
index 870281d..831de9c 100644
--- a/DividedPowers/DPAlgebra/Misc.lean
+++ b/DividedPowers/DPAlgebra/Misc.lean
@@ -2,13 +2,11 @@
 ! This file was ported from Lean 3 source module divided_powers.dp_algebra.misc
 -/
 
-import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
+import Mathlib.Algebra.MvPolynomial.Supported
 import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.TrivSqZeroExt
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.Algebra.MvPolynomial.Supported
-import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 
 noncomputable section
 
diff --git a/DividedPowers/DPAlgebra/PolynomialMap.lean b/DividedPowers/DPAlgebra/PolynomialMap.lean
index 0cda909..5cad0b4 100644
--- a/DividedPowers/DPAlgebra/PolynomialMap.lean
+++ b/DividedPowers/DPAlgebra/PolynomialMap.lean
@@ -1,6 +1,5 @@
-import DividedPowers.PolynomialMap.Homogeneous
-import DividedPowers.DPAlgebra.Graded.Basic
 import DividedPowers.DPAlgebra.BaseChange
+import DividedPowers.PolynomialMap.Homogeneous
 
 /-
 
@@ -83,7 +82,6 @@ theorem gamma_mem_grade (n : ℕ) (S : Type*) [CommRing S] [Algebra R S] (m : S
     simp only [LinearMap.mem_range]
     -- we need the graded structure on the base change of a graded algebra
     rw [← hx', ← hy']
-
     sorry
 
 /- to do this, it seems that we have to understand polynomial maps
diff --git a/DividedPowers/DPAlgebra/RobyLemma9.lean b/DividedPowers/DPAlgebra/RobyLemma9.lean
index 9862fcb..490fc76 100644
--- a/DividedPowers/DPAlgebra/RobyLemma9.lean
+++ b/DividedPowers/DPAlgebra/RobyLemma9.lean
@@ -1,7 +1,5 @@
-import Mathlib.RingTheory.TensorProduct.Basic
-import Mathlib.LinearAlgebra.TensorProduct.Tower
 import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.RingTheory.TensorProduct.Basic
 
 open scoped TensorProduct
 
diff --git a/DividedPowers/ForMathlib/Bell.lean b/DividedPowers/ForMathlib/Bell.lean
index a28a4a9..5b93e19 100644
--- a/DividedPowers/ForMathlib/Bell.lean
+++ b/DividedPowers/ForMathlib/Bell.lean
@@ -1,24 +1,24 @@
+import Mathlib.Algebra.Ring.Regular
 import Mathlib.Data.Nat.Choose.Multinomial
-import Mathlib.Data.Nat.Choose.Vandermonde
 
-/-! # Bell numbers for multisets 
+/-! # Bell numbers for multisets
 
-For `n : ℕ`, the `n`th Bell number is the number of partitions of a set of cardinality `n`. 
+For `n : ℕ`, the `n`th Bell number is the number of partitions of a set of cardinality `n`.
 Here, we define a refinement of these numbers, that count, for any `m : Multiset ℕ`,
 the number of partitions of a set of cardinality `m.sum` whose parts have cardinalities given by `m`.
 The definition presents it as an integer.
 
-* `Multiset.bell`: number of partitions of a set whose parts have cardinalities a given multiset 
+* `Multiset.bell`: number of partitions of a set whose parts have cardinalities a given multiset
 
-* `Multiset.bell_zero`: `Multiset.bell 0 = 1` 
+* `Multiset.bell_zero`: `Multiset.bell 0 = 1`
 
 * `Nat.uniformBell m n` : short name for `Multiset.bell (replicate m n)`
 
 * `Multiset.bell_mul_eq` shows that
-    `m.bell * (m.map (fun j ↦ j !)).prod * 
+    `m.bell * (m.map (fun j ↦ j !)).prod *
       Finset.prod (m.toFinset.erase 0) (fun j ↦ (m.count j)!) = m.sum !`
 
-* `Nat.uniformBell_mul_eq`  shows that 
+* `Nat.uniformBell_mul_eq`  shows that
     `uniformBell m n * n.factorial ^ m * m.factorial = (m * n).factorial`
 
 * `Nat.uniformBell_zero`, `Nat.uniformBell_zero'`, `Nat.uniformBell_one`, `Nat.uniformBell_one':
@@ -31,13 +31,13 @@ compute `Nat.uniformBell` when one of the parameters is `0` or `1`
 open Multiset Nat
 
 theorem Nat.choose_mul_add (m) {n : ℕ} (hn : n ≠ 0) :
-    (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1) := by 
+    (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1) := by
   rw [← mul_left_inj' (mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]
-  set p := n - 1 
+  set p := n - 1
   have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
   simp only [hp, add_succ_sub_one]
-  calc 
-    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p+1))! * (p+1)!) 
+  calc
+    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p+1))! * (p+1)!)
       = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p+1))! * (p+1)! := by ring
     _ = (m * (p+ 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
     _ = ((m * (p+ 1) + p) + 1)! := by ring_nf
@@ -47,10 +47,10 @@ theorem Nat.choose_mul_add (m) {n : ℕ} (hn : n ≠ 0) :
     _ = (m * (p + 1) + p).choose p * (m * (p+1))! * (((p + 1) * (p)!) * (m + 1)) := by ring
     _ = (m * (p + 1) + p).choose p * (m * (p+1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
     _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by ring
-  
+
 theorem Nat.choose_mul_right (m) {n : ℕ} (hn : n ≠ 0) :
-    (m * n).choose n = m * (m * n - 1).choose (n - 1) := by 
-  by_cases hm : m = 0 
+    (m * n).choose n = m * (m * n - 1).choose (n - 1) := by
+  by_cases hm : m = 0
   · simp only [hm, zero_mul, choose_eq_zero_iff]
     exact Nat.pos_of_ne_zero hn
   · set p := m - 1; have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
@@ -58,29 +58,29 @@ theorem Nat.choose_mul_right (m) {n : ℕ} (hn : n ≠ 0) :
     rw [add_mul, one_mul, choose_mul_add _ hn]
 
 
-@[simp] lemma Multiset.replicate_toFinset {α : Type*} [DecidableEq α] (n : ℕ) (a : α) : 
-    (replicate n a).toFinset = if n = 0 then ∅ else {a} := by 
+@[simp] lemma Multiset.replicate_toFinset {α : Type*} [DecidableEq α] (n : ℕ) (a : α) :
+    (replicate n a).toFinset = if n = 0 then ∅ else {a} := by
   ext x
   simp only [mem_toFinset, Finset.mem_singleton, mem_replicate]
   split_ifs with hn <;> simp [hn]
 
-def Multiset.bell (m : Multiset ℕ) : ℕ := 
-  Nat.multinomial m.toFinset (fun k ↦ k * m.count k) * 
-    (m.toFinset.erase 0).prod 
+def Multiset.bell (m : Multiset ℕ) : ℕ :=
+  Nat.multinomial m.toFinset (fun k ↦ k * m.count k) *
+    (m.toFinset.erase 0).prod
       (fun k ↦ Finset.prod (Finset.range (m.count k)) fun j ↦ (j * k + k - 1).choose (k-1))
 
 @[simp]
 theorem Multiset.bell_zero : bell 0 = 1 := by unfold bell; simp
 
 @[to_additive]
-theorem Multiset.map_prod_pow_count {ι α : Type*} [DecidableEq ι] (m : Multiset ι) [CommMonoid α] 
+theorem Multiset.map_prod_pow_count {ι α : Type*} [DecidableEq ι] (m : Multiset ι) [CommMonoid α]
     (f : ι → α) :
-     m.toFinset.prod (fun a ↦ f a ^ count a m) = (m.map f).prod := by 
+     m.toFinset.prod (fun a ↦ f a ^ count a m) = (m.map f).prod := by
   induction m using Multiset.induction_on with
   | empty => simp
-  | cons n m h => 
+  | cons n m h =>
     simp only [toFinset_cons, prod_cons, map_cons]
-    by_cases hn : n ∈ m 
+    by_cases hn : n ∈ m
     · have hn' : n ∈ m.toFinset := by exact mem_toFinset.mpr hn
       rw [Finset.insert_eq_of_mem hn']
       rw [← Finset.prod_erase_mul _ _ hn'] at h ⊢
@@ -89,9 +89,9 @@ theorem Multiset.map_prod_pow_count {ι α : Type*} [DecidableEq ι] (m : Multis
       apply congr_arg₂ _ rfl
       apply congr_arg₂ _ _ rfl
       apply Finset.prod_congr rfl
-      intro x hx 
+      intro x hx
       apply congr_arg₂ _ rfl
-      rw [count_cons, if_neg (Finset.ne_of_mem_erase hx), add_zero] 
+      rw [count_cons, if_neg (Finset.ne_of_mem_erase hx), add_zero]
     · have hn' : n ∉ m.toFinset := by simp [hn]
       rw [Finset.prod_insert hn']
       apply congr_arg₂
@@ -103,7 +103,7 @@ theorem Multiset.map_prod_pow_count {ι α : Type*} [DecidableEq ι] (m : Multis
 
  @[to_additive]
 theorem Multiset.prod_pow_count {α : Type*} [DecidableEq α] (m : Multiset α) [CommMonoid α] :
-     m.toFinset.prod (fun i ↦ i ^ count i m) = m.prod := by 
+     m.toFinset.prod (fun i ↦ i ^ count i m) = m.prod := by
   rw [← map_id m, ← m.map_prod_pow_count, map_id]
   simp only [id_eq]
 
@@ -111,8 +111,8 @@ theorem Nat.bell_mul_eq_lemma {x : ℕ} (hx : x ≠ 0) (c : ℕ) :
     x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1) = (x * c)! := by
   induction c with
   | zero => simp
-  | succ c hrec => 
-    suffices  x ! ^ (c + 1) * (c + 1) ! = x ! * (c + 1) * (x ! ^ c * c !) by 
+  | succ c hrec =>
+    suffices  x ! ^ (c + 1) * (c + 1) ! = x ! * (c + 1) * (x ! ^ c * c !) by
       rw [this]
       rw [← mul_assoc]
       simp only [Finset.range_succ, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
@@ -123,7 +123,7 @@ theorem Nat.bell_mul_eq_lemma {x : ℕ} (hx : x ≠ 0) (c : ℕ) :
       rw [mul_comm]
       simp only [← mul_assoc]
       rw [hrec]
-      have : (x * c)! * ((c * x + x - 1).choose (x - 1)) * x ! * (c + 1)  
+      have : (x * c)! * ((c * x + x - 1).choose (x - 1)) * x ! * (c + 1)
         = ((c + 1) * ((c * x + x - 1).choose (x - 1))) * (x * c)! *  x ! := by
         ring_nf
       rw [this]
@@ -134,8 +134,8 @@ theorem Nat.bell_mul_eq_lemma {x : ℕ} (hx : x ≠ 0) (c : ℕ) :
     rw [factorial_succ, pow_succ]
     ring_nf
 
-theorem Multiset.bell_mul_eq (m : Multiset ℕ) : 
-    m.bell * (m.map (fun j ↦ j !)).prod * 
+theorem Multiset.bell_mul_eq (m : Multiset ℕ) :
+    m.bell * (m.map (fun j ↦ j !)).prod *
       Finset.prod (m.toFinset.erase 0) (fun j ↦ (m.count j)!) = m.sum ! := by
   unfold bell
   rw [← Nat.mul_right_inj]
@@ -146,7 +146,7 @@ theorem Multiset.bell_mul_eq (m : Multiset ℕ) :
     apply congr_arg₂
     · rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib]
       rw [← Multiset.map_prod_pow_count]
-      suffices this : _ by 
+      suffices this : _ by
         by_cases hm : 0 ∈ m.toFinset
         · rw [← Finset.prod_erase_mul _ _ hm]
           rw [← Finset.prod_erase_mul _ _ hm]
@@ -168,8 +168,8 @@ theorem Multiset.bell_mul_eq (m : Multiset ℕ) :
     apply Finset.prod_pos
     exact fun _ _ ↦ Nat.factorial_pos _
 
-theorem Multiset.bell_eq (m : Multiset ℕ) : 
-    m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * 
+theorem Multiset.bell_eq (m : Multiset ℕ) :
+    m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod *
       Finset.prod (m.toFinset.erase 0) (fun j ↦ (m.count j)!)) := by
   rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]
   · rw [← mul_assoc]
@@ -186,24 +186,24 @@ theorem Multiset.bell_eq (m : Multiset ℕ) :
 
 def Nat.uniformBell (m n : ℕ) : ℕ := bell (replicate m n)
 
-theorem Nat.uniformBell_eq (m n : ℕ) : m.uniformBell n =  
-    Finset.prod (Finset.range m) fun p => Nat.choose (p * n + n - 1) (n - 1) := by 
+theorem Nat.uniformBell_eq (m n : ℕ) : m.uniformBell n =
+    Finset.prod (Finset.range m) fun p => Nat.choose (p * n + n - 1) (n - 1) := by
   unfold uniformBell bell
   rw [replicate_toFinset]
   split_ifs with hm
   · simp  [hm]
-  · by_cases hn : n = 0 
+  · by_cases hn : n = 0
     · simp [hn]
     · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
       simp [count_replicate]
 
-theorem Nat.uniformBell_zero (n : ℕ) : uniformBell 0 n = 1 := by 
+theorem Nat.uniformBell_zero (n : ℕ) : uniformBell 0 n = 1 := by
   simp [uniformBell_eq]
 
 theorem Nat.uniformBell_zero' (m : ℕ) : uniformBell m 0 = 1 := by
   simp [uniformBell_eq]
 
-theorem Nat.uniformBell_succ (m n : ℕ) : 
+theorem Nat.uniformBell_succ (m n : ℕ) :
     uniformBell (m+1) n = choose (m * n + n - 1) (n - 1) * uniformBell m n := by
   simp only [uniformBell_eq, Finset.prod_range_succ, mul_comm]
 
@@ -215,7 +215,7 @@ theorem uniformBell_one' (m : ℕ) : uniformBell m 1 = 1 := by
   simp only [uniformBell_eq, mul_one, add_tsub_cancel_right, ge_iff_le, le_refl,
     tsub_eq_zero_of_le, choose_zero_right, Finset.prod_const_one]
 
-theorem uniformBell_mul_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) : 
+theorem uniformBell_mul_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
     uniformBell m n * n.factorial ^ m * m.factorial = (m * n).factorial := by
   convert bell_mul_eq (replicate m n)
   · simp only [map_replicate, prod_replicate]
@@ -231,10 +231,10 @@ theorem uniformBell_eq_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
     uniformBell m n = (m * n).factorial / (n.factorial ^ m * m.factorial) := by
   rw [eq_comm]
   apply Nat.div_eq_of_eq_mul_left
-  · exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos 
+  · exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos
   · rw [← mul_assoc, ← uniformBell_mul_eq _ hn]
-    
-  
+
+
 namespace Nat
 
 #exit
@@ -266,21 +266,21 @@ theorem mchoose_lemma (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
   rw [← zero_lt_iff] at hn
   induction m with -- m ih
   | zero => rw [mchoose_zero, mul_one, MulZeroClass.zero_mul, factorial_zero, pow_zero, mul_one]
-  | succ m ih => 
-    calc (m+1)! * (n)! ^ (m+1) * mchoose (m + 1) n 
+  | succ m ih =>
+    calc (m+1)! * (n)! ^ (m+1) * mchoose (m + 1) n
         = (m + 1)! *(n)! ^(m + 1) * ((m * n + n - 1).choose (n-1) * mchoose m n) := by rw [mchoose_succ]
       _ = ((m + 1) * (m * n + n - 1).choose (n-1)) * (m)! * (n)!  ^(m +1) * (mchoose m n) := by
-        rw [factorial_succ]; ring 
-      _ = ((m*n+n).choose n) * (m)! * (n)! ^ (m+1) * (mchoose m n) := by 
+        rw [factorial_succ]; ring
+      _ = ((m*n+n).choose n) * (m)! * (n)! ^ (m+1) * (mchoose m n) := by
         rw [← choose_mul_add _ (not_eq_zero_of_lt hn)]
-      _ = ((m*n+n).choose n) * (n)! * ((m)! * (n)! ^ m * (mchoose m n)) := by 
+      _ = ((m*n+n).choose n) * (n)! * ((m)! * (n)! ^ m * (mchoose m n)) := by
         rw [pow_succ]; ring_nf
       _ = (m  * n + n).choose n * (m * n)! * (n)! := by rw [ih]; ring
       _ = (m * n + n)! := by rw [add_choose_mul_factorial_mul_factorial]
       _ = ((m + 1)* n)! := by ring_nf
 
 
-theorem mchoose_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) : 
+theorem mchoose_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
     mchoose m n = (m * n).factorial / (m.factorial * n.factorial ^ m) := by
   rw [eq_comm]
   apply Nat.div_eq_of_eq_mul_left
@@ -289,37 +289,37 @@ theorem mchoose_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
 
 open Multiset Finset
 
-/- Can one define restricted Bell numbers ? 
+/- Can one define restricted Bell numbers ?
 
 For `m : Multiset ℕ`, `rBell m` counts the number of unordered partitions
-of a set with `m.sum` elements. 
+of a set with `m.sum` elements.
 It is equal to `(m.sum)! / ((m.map fun i ↦ i !).prod * Π n ∈ m.toFinset.erase 0, (m.count n)!)
 -/
 
 /-- The number of partitions of a set of cardinality `m.sum` with parts of cardinalities given by `m` -/
 def rBell (m : Multiset ℕ) : ℕ :=
-  (m.sum)! / ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!)) 
+  (m.sum)! / ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!))
 
 theorem rBell_dvd (m : Multiset ℕ) :
-    ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!)) ∣ (m.sum)! := by 
-  suffices ∀ s : Finset ℕ, ∀ m : Multiset ℕ, m.toFinset = s → 
-    ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!)) ∣ (m.sum)! by 
-    exact this m.toFinset m rfl 
+    ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!)) ∣ (m.sum)! := by
+  suffices ∀ s : Finset ℕ, ∀ m : Multiset ℕ, m.toFinset = s →
+    ((m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!)) ∣ (m.sum)! by
+    exact this m.toFinset m rfl
   intro s
-  induction s using Finset.induction_on with 
-  | empty => 
-    intro m hs 
-    rw [toFinset_eq_empty] at hs 
+  induction s using Finset.induction_on with
+  | empty =>
+    intro m hs
+    rw [toFinset_eq_empty] at hs
     simp [hs, prod_empty, mul_one]
-  | @insert a s has hrec => 
+  | @insert a s has hrec =>
     intro m hs
-    let m' := m - replicate (m.count a) a 
+    let m' := m - replicate (m.count a) a
     have hm' : count a m' = 0 := by simp [m']
-    have hm : m = m' + replicate (m.count a) a := by 
+    have hm : m = m' + replicate (m.count a) a := by
       simp only [m']
-      ext b 
+      ext b
       simp only [count_add, count_replicate, count_sub, m']
-      split_ifs with hb 
+      split_ifs with hb
       · simp [hb]
       · simp [hb]
     have hs' :m'.toFinset = s := by
@@ -337,23 +337,23 @@ theorem rBell_dvd (m : Multiset ℕ) :
     simp only [hs'] at hk
     by_cases ha0 : a = 0
     · simp [ha0]
-      have : m.toFinset.erase 0 = s.erase 0 := by 
+      have : m.toFinset.erase 0 = s.erase 0 := by
         ext x
-        simp only [hs, ha0, erase_insert_eq_erase, mem_erase, ne_eq] 
+        simp only [hs, ha0, erase_insert_eq_erase, mem_erase, ne_eq]
       rw [this]
-      conv_rhs => 
+      conv_rhs =>
         rw [hm, Multiset.sum_add, Multiset.sum_replicate, ha0, smul_eq_mul, mul_zero, add_zero]
       rw [hk]
-      rw [Finset.prod_congr rfl 
-        (show ∀ x ∈ s.erase 0, (count x m)! = (count x m')! by 
+      rw [Finset.prod_congr rfl
+        (show ∀ x ∈ s.erase 0, (count x m)! = (count x m')! by
           intro x hx
           apply congr_arg
           rw [hm, count_add, count_replicate, if_neg, add_zero]
-          intro hx' 
+          intro hx'
           rw [← hx'] at hx
           exact has (Finset.mem_of_mem_erase hx))]
       apply Nat.dvd_mul_right
-    · have this : (insert a s).erase 0 = insert a (s.erase 0) := by 
+    · have this : (insert a s).erase 0 = insert a (s.erase 0) := by
         ext x
         simp only [mem_erase, ne_eq, mem_insert]
         constructor
@@ -372,14 +372,14 @@ theorem rBell_dvd (m : Multiset ℕ) :
       rw [hm]
       simp only [count_add, count_replicate_self, sum_add, sum_replicate, smul_eq_mul, hm', zero_add]
       rw [Finset.prod_congr rfl
-        (show ∀ x ∈ s.erase 0, (count x m' + count x (replicate (count a m) a))! = (count x m')! by 
-          intro x hx 
+        (show ∀ x ∈ s.erase 0, (count x m' + count x (replicate (count a m) a))! = (count x m')! by
+          intro x hx
           apply congr_arg
           rw [count_replicate, if_neg, add_zero]
           intro hx'; rw [hx'] at this'; exact this' hx)]
       rw [← add_choose_mul_factorial_mul_factorial m'.sum, hk]
       simp only [mul_assoc]
-      conv_rhs => 
+      conv_rhs =>
         rw [mul_comm]
         simp only [mul_assoc]
       apply mul_dvd_mul dvd_rfl
@@ -392,14 +392,14 @@ theorem rBell_dvd (m : Multiset ℕ) :
       simp only [mul_assoc]
       apply mul_dvd_mul dvd_rfl
       apply Nat.dvd_mul_right
-      
-theorem rBell_mul_eq_factorial_sum (m : Multiset ℕ) : 
-    rBell m * (m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!) = (m.sum)! := by 
+
+theorem rBell_mul_eq_factorial_sum (m : Multiset ℕ) :
+    rBell m * (m.map fun n ↦ n !).prod * (∏ n in m.toFinset.erase 0, (m.count n)!) = (m.sum)! := by
   rw [mul_assoc]
   exact Nat.div_mul_cancel (rBell_dvd m)
 
 
-theorem rBell_replicate (m n : ℕ) : rBell (replicate m n) = mchoose m n := by 
+theorem rBell_replicate (m n : ℕ) : rBell (replicate m n) = mchoose m n := by
   by_cases hn : n = 0
   · rw [hn, mchoose_zero']
     unfold rBell
@@ -410,8 +410,8 @@ theorem rBell_replicate (m n : ℕ) : rBell (replicate m n) = mchoose m n := by
     simp only [replicate_toFinset, mem_erase, ne_eq] at hx
     simp only [count_replicate, if_neg (Ne.symm hx.1), factorial_zero]
   · rw [mchoose_eq m hn]
-    unfold rBell 
-    apply congr_arg₂ 
+    unfold rBell
+    apply congr_arg₂
     · rw [sum_replicate]
       simp only [smul_eq_mul]
     · simp only [map_replicate, prod_replicate]
@@ -424,5 +424,3 @@ theorem rBell_replicate (m n : ℕ) : rBell (replicate m n) = mchoose m n := by
         simp only [mem_erase, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
         intro hx
         simp [hx, hn]
-
-
diff --git a/DividedPowers/ForMathlib/DirectLimit.lean b/DividedPowers/ForMathlib/DirectLimit.lean
index e3f0656..d1f16ec 100644
--- a/DividedPowers/ForMathlib/DirectLimit.lean
+++ b/DividedPowers/ForMathlib/DirectLimit.lean
@@ -1,11 +1,6 @@
-import Mathlib.RingTheory.FiniteType
-import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.Algebra.Algebra.Subalgebra.Basic
-import Mathlib.RingTheory.TensorProduct.Basic
-import Mathlib.Algebra.DirectLimit
 import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
--- import DividedPowers.ForMathlib.LinearAlgebra.DirectSum.Finsupp
-import DividedPowers.ForMathlib.RingTheory.TensorProduct.LinearEquiv
+import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.RingTheory.Adjoin.FG
 
 /- # Tensor products and finitely generated submodules
 
diff --git a/DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean b/DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean
index 939810d..9e6e7ce 100644
--- a/DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean
+++ b/DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean
@@ -5,9 +5,9 @@ Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
 -/
 
 import DividedPowers.ForMathlib.MvPowerSeries.PiTopology
+import DividedPowers.ForMathlib.MvPowerSeries.Trunc
 import DividedPowers.ForMathlib.Topology.Algebra.TopologicallyNilpotent
 import Mathlib.Algebra.MvPolynomial.CommRing
-import DividedPowers.ForMathlib.MvPowerSeries.Trunc
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.UniformRing
 
@@ -405,3 +405,5 @@ theorem comp_aeval (ha : EvalDomain a)
 end Evaluation
 
 end MvPowerSeries
+
+#min_imports
diff --git a/DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean b/DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean
index fae3eb0..932d160 100644
--- a/DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean
+++ b/DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean
@@ -3,9 +3,9 @@ Copyright (c) 2024 Antoine Chambert-Loir, María Inés de Frutos-Fernández. All
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
 -/
-import Mathlib.Data.Finsupp.Interval
 import DividedPowers.ForMathlib.MvPowerSeries.PiTopology
 import DividedPowers.ForMathlib.Topology.Algebra.LinearTopology
+import Mathlib.Data.Finsupp.Interval
 
 /-! # Linear topology on the ring of multivariate power series
 
diff --git a/DividedPowers/ForMathlib/MvPowerSeries/Substitution.lean b/DividedPowers/ForMathlib/MvPowerSeries/Substitution.lean
index a64c8e4..6e0ec60 100644
--- a/DividedPowers/ForMathlib/MvPowerSeries/Substitution.lean
+++ b/DividedPowers/ForMathlib/MvPowerSeries/Substitution.lean
@@ -4,14 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos Fernández
 -/
 
-import Mathlib.Algebra.MvPolynomial.CommRing
-import Mathlib.Data.Set.Finite
 import DividedPowers.ForMathlib.MvPowerSeries.Evaluation
 import DividedPowers.ForMathlib.MvPowerSeries.LinearTopology
-import Mathlib.RingTheory.MvPowerSeries.Trunc
-import Mathlib.RingTheory.PowerSeries.Basic
 import Mathlib.RingTheory.Nilpotent.Basic
-import Mathlib.Topology.Algebra.Algebra
+import Mathlib.RingTheory.PowerSeries.Basic
 
 /-! # Substitutions in power series
 
diff --git a/DividedPowers/ForMathlib/MvPowerSeries/Trunc.lean b/DividedPowers/ForMathlib/MvPowerSeries/Trunc.lean
index d997d5c..3f4f999 100644
--- a/DividedPowers/ForMathlib/MvPowerSeries/Trunc.lean
+++ b/DividedPowers/ForMathlib/MvPowerSeries/Trunc.lean
@@ -1,5 +1,5 @@
-import Mathlib.RingTheory.MvPowerSeries.Trunc
-
+import Mathlib.Data.Finsupp.Interval
+import Mathlib.RingTheory.MvPowerSeries.Basic
 
 -- In #15019
 
diff --git a/DividedPowers/IdealAdd.lean b/DividedPowers/IdealAdd.lean
index 2f9f68a..3b56593 100644
--- a/DividedPowers/IdealAdd.lean
+++ b/DividedPowers/IdealAdd.lean
@@ -6,6 +6,8 @@ Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
 import DividedPowers.BasicLemmas
 import DividedPowers.DPMorphism
 import DividedPowers.RatAlgebra
+import Mathlib.Data.Nat.Choose.Vandermonde
+
 
 section Polynomial
 
diff --git a/DividedPowers/PolynomialMap/Basic.lean b/DividedPowers/PolynomialMap/Basic.lean
index 015aec8..033262e 100644
--- a/DividedPowers/PolynomialMap/Basic.lean
+++ b/DividedPowers/PolynomialMap/Basic.lean
@@ -1,8 +1,10 @@
 /- Copyright ACL @ MIdFF 2024 -/
 
 import DividedPowers.ForMathlib.DirectLimit
-import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
+import Mathlib.RingTheory.FiniteType
+import Mathlib.RingTheory.Ideal.QuotientOperations
+
 
 /-! # Polynomial laws on modules
 
diff --git a/DividedPowers/PolynomialMap/Coeff.lean b/DividedPowers/PolynomialMap/Coeff.lean
index 9819b66..0132329 100644
--- a/DividedPowers/PolynomialMap/Coeff.lean
+++ b/DividedPowers/PolynomialMap/Coeff.lean
@@ -1,6 +1,6 @@
 import DividedPowers.ForMathlib.RingTheory.SubmoduleMem
+import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
 import DividedPowers.PolynomialMap.Basic
-import Mathlib.RingTheory.TensorProduct.Basic
 
 universe u v w uM uN uι