diff --git a/ClassificationOfSubgroups/Ch4_PGLIsoPSLOverAlgClosedField/ProjectiveGeneralLinearGroup.lean b/ClassificationOfSubgroups/Ch4_PGLIsoPSLOverAlgClosedField/ProjectiveGeneralLinearGroup.lean
index f59b43a..0403d7f 100644
--- a/ClassificationOfSubgroups/Ch4_PGLIsoPSLOverAlgClosedField/ProjectiveGeneralLinearGroup.lean
+++ b/ClassificationOfSubgroups/Ch4_PGLIsoPSLOverAlgClosedField/ProjectiveGeneralLinearGroup.lean
@@ -1,8 +1,6 @@
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 
-set_option linter.style.longLine true
-set_option autoImplicit false
 set_option maxHeartbeats 0
 
 universe u v w
diff --git a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S1_SpecialMatrices.lean b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S1_SpecialMatrices.lean
index a7ab058..c4165ee 100644
--- a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S1_SpecialMatrices.lean
+++ b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S1_SpecialMatrices.lean
@@ -182,5 +182,3 @@ lemma neg_d_mul_w (δ : Fˣ) : -(d δ * w) = d (-δ) * w := by rw [← neg_mul,
 end Interactions
 
 end SpecialMatrices
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S2_SpecialSubgroups.lean b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S2_SpecialSubgroups.lean
index e2db170..d8b5257 100644
--- a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S2_SpecialSubgroups.lean
+++ b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S2_SpecialSubgroups.lean
@@ -1,11 +1,8 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S1_SpecialMatrices
 import Mathlib.Algebra.Category.Grp.Images
 import Mathlib.Analysis.Normed.Field.Lemmas
+import Mathlib.GroupTheory.PGroup
 import Mathlib.Order.CompletePartialOrder
-import Mathlib.GroupTheory.Sylow
-
-set_option linter.style.longLine true
-set_option maxHeartbeats 0
 
 open Matrix MatrixGroups Subgroup Pointwise SpecialMatrices
 
@@ -20,6 +17,7 @@ variable
 namespace MatrixShapes
 
 def IsDiagonal (x : Matrix (Fin 2) (Fin 2) F) : Prop := x 0 1 = 0 ∧ x 1 0 = 0
+def IsAntiDiagonal (x : Matrix (Fin 2) (Fin 2) F) : Prop := x 0 0 = 0 ∧ x 1 1 = 0
 def IsLowerTriangular (x : Matrix (Fin 2) (Fin 2) F) : Prop := x 0 1 = 0
 def IsUpperTriangular (x : Matrix (Fin 2) (Fin 2) F) : Prop := x 1 0 = 0
 
@@ -345,12 +343,6 @@ lemma D_join_S_eq_L (F : Type*) [Field F]: D F ⊔ S F = L F := by
     rfl
 
 
-
-
-
--- second isomorphism theorem!!!!
-#check QuotientGroup.quotientInfEquivProdNormalQuotient
-
 def D_subgroupOf_L_mulEquiv_D : (D F).subgroupOf (L F) ≃* D F := by
   refine subgroupOfEquivOfLe ?_
   rintro d ⟨δ, rfl⟩
@@ -383,57 +375,6 @@ lemma left_subgroupOf_join_right_subgroupOf_join_eq_join_subgroupOf_join {G : Ty
   rw [comap_sup_eq_of_le_range f hH hK]
   simp [f]
 
-lemma simplify₁ : ((D F).subgroupOf (D F ⊔ S F) ⊔ (S F).subgroupOf (D F ⊔ S F)) = ⊤ :=
-  left_subgroupOf_join_right_subgroupOf_join_eq_join_subgroupOf_join (D F) (S F)
-
-/- D and S have trivial interesection, so the following holds -/
-lemma simplify₂ : ((S F).subgroupOf (D F ⊔ S F)).subgroupOf ((D F).subgroupOf (D F ⊔ S F)) = ⊥ := by
-  simp
-  rw [disjoint_iff, ← comap_subtype, ← comap_subtype, ← comap_inf, inf_comm, D_meet_S_eq_bot]
-  simp
-
-/- The second isomorphism theorem -/
-noncomputable def D_join_S_quot_S_subgroupOf_D_join_S_mulEquiv_D_subgroupOf_D_join_S
-  (F : Type*) [Field F] :=
-  (QuotientGroup.quotientInfEquivProdNormalQuotient
-    (H := (D F).subgroupOf (D F ⊔ S F:)) (N := (S F).subgroupOf (D F ⊔ S F :))).symm
-
-#check D_join_S_quot_S_subgroupOf_D_join_S_mulEquiv_D_subgroupOf_D_join_S
-
-def LHS (F : Type*) [Field F] :=
-  @QuotientGroup.equivQuotientSubgroupOfOfEq
-
-
-
-#check QuotientGroup.quotientBot
-
-#check MulEquiv.trans
-
-#check QuotientGroup.equivQuotientSubgroupOfOfEq
-
-#check QuotientGroup.quotientMulEquivOfEq
-
-def RHS (F : Type*) [Field F] :=
-  @QuotientGroup.equivQuotientSubgroupOfOfEq ((D F).subgroupOf (D F ⊔ S F) :) _
-    (A' := ((S F).subgroupOf (D F ⊔ S F)).subgroupOf ((D F).subgroupOf (D F ⊔ S F)))
-    -- below were ⊤ : (D F).subgroupOf (D F ⊔ S F)
-    (A := ⊤)--((D F).subgroupOf (D F ⊔ S F)).subgroupOf ((D F).subgroupOf (D F ⊔ S F)))
-    (B' := ⊥)
-    (B := ⊤)--((D F).subgroupOf (D F ⊔ S F)).subgroupOf ((D F).subgroupOf (D F ⊔ S F)))
-    (hAN := normal_subgroupOf)
-    (hBN := normal_subgroupOf)
-    (h' := simplify₂)
-    (h := Eq.refl _)
-
-#check RHS
-
-
--- def RHS' (F : Type*) [Field F] :
---   ↥(⊤ : Subgroup ↥((D F).subgroupOf (D F ⊔ S F))) ⧸ (⊥ : Subgroup ((D F).subgroupOf (D F ⊔ S F))).subgroupOf (⊤ : Subgroup ↥((D F).subgroupOf (D F ⊔ S F)))
---   ≃*
---   ↥(⊤ : Subgroup ↥((D F).subgroupOf (D F ⊔ S F))) :=
---   @QuotientGroup.quotientBot (((D F).subgroupOf (D F ⊔ S F)) :) _
-
 -- Conclusion to reach is
 instance : ((S F).subgroupOf (L F)).Normal := normal_S_subgroupOf_L
 
@@ -441,29 +382,11 @@ noncomputable def L_quot_S_subgroupOf_L_mulEquiv_D_subgroupOf_L :=
     QuotientGroup.quotientInfEquivProdNormalQuotient
       (H := (L F).subgroupOf (L F)) (N := (S F).subgroupOf (L F :))
 
-
-#check L_quot_S_subgroupOf_L_mulEquiv_D_subgroupOf_L
-
--- lemma foo : ((S F).subgroupOf (L F)).subgroupOf ((L F).subgroupOf (L F)) = (S F).subgroupOf (L F) := by sorry
-
-#check D_join_S_quot_S_subgroupOf_D_join_S_mulEquiv_D_subgroupOf_D_join_S
-
-#check L_quot_S_subgroupOf_L_mulEquiv_D_subgroupOf_L
-
-#check ((S F).subgroupOf (L F)).subgroupOf ((L F).subgroupOf (L F) ⊔ (S F).subgroupOf (L F))
-
-  --@QuotientGroup.Quotient.group (L F) _ ((S F).subgroupOf (L F)) (normal_S_subgroupOf_L)
-
 def D_join_S_monoidHom_D : (D F × S F :) →* D F where
   toFun d_s := d_s.1
   map_one' := by simp
   map_mul' := by simp
 
-
-
-#check  QuotientGroup.quotientKerEquivRange
-
-
 def DW (F : Type*) [Field F] : Subgroup SL(2,F) where
   carrier := { d δ | δ : Fˣ} ∪ { d δ * w | δ : Fˣ}
   mul_mem' := by
@@ -495,8 +418,7 @@ lemma D_leq_DW : D F ≤ DW F := by
   left
   apply exists_apply_eq_apply
 
-
-lemma Dw_leq_DW : (D F : Set SL(2,F)) * ({w} : Set SL(2,F)) ⊆ (DW F :  Set SL(2,F)) := by
+lemma Dw_leq_DW : (D F : Set SL(2,F)) * ({w} : Set SL(2,F)) ⊆ (DW F : Set SL(2,F)) := by
   rintro x ⟨d', hd', w, hw, rfl⟩
   obtain ⟨δ, rfl⟩ := hd'
   rw [DW, coe_set_mk]
@@ -504,7 +426,6 @@ lemma Dw_leq_DW : (D F : Set SL(2,F)) * ({w} : Set SL(2,F)) ⊆ (DW F :  Set SL(
   use δ
   rw [Set.mem_singleton_iff] at hw
   rw [hw]
-
 section Center
 
 def Z (R : Type*) [CommRing R] : Subgroup SL(2,R) := closure {(-1 : SL(2,R))}
@@ -519,13 +440,11 @@ lemma get_entries (x : SL(2,F)) : ∃ α β γ δ,
 
 lemma neg_one_mem_Z : (-1 : SL(2,F)) ∈ Z F := by simp [Z]
 
-
 lemma Odd.neg_one_zpow {α : Type*} [Group α] [HasDistribNeg α] {n : ℤ} (h : Odd n) :
   (-1 : α) ^ n = -1 := by
   rw [← neg_eq_iff_eq_neg, ← neg_one_mul, Commute.neg_one_left, mul_zpow_self]
   exact Even.neg_one_zpow <| Odd.add_one h
 
-
 lemma closure_neg_one_eq : (closure {(-1 : SL(2,R))} : Set SL(2,R)) = {1, -1} := by
   ext x
   constructor
@@ -548,7 +467,6 @@ lemma closure_neg_one_eq : (closure {(-1 : SL(2,R))} : Set SL(2,R)) = {1, -1} :=
     · rw [SetLike.mem_coe]
       exact mem_closure_singleton_self (-1)
 
-
 @[simp]
 lemma neg_one_neq_one_of_two_ne_zero [NeZero (2 : F)] : (1 : SL(2,F)) ≠ (-1 : SL(2,F)) := by
   intro h
@@ -566,14 +484,11 @@ lemma Field.one_eq_neg_one_of_two_eq_zero (two_eq_zero : (2 : F) = 0) : 1 = (-1
   rw [← one_add_one_eq_two, add_eq_zero_iff_neg_eq'] at two_eq_zero
   exact two_eq_zero.symm
 
-
 lemma SpecialLinearGroup.neg_one_eq_one_of_two_eq_zero (two_eq_zero : (2 : F) = 0) :
   1 = (-1 : SL(2,F)) := by
   ext
   <;> simpa using Field.one_eq_neg_one_of_two_eq_zero two_eq_zero
 
-
-
 @[simp]
 lemma set_Z_eq : (Z R : Set SL(2,R)) = {1, -1} := by
   dsimp [Z]
@@ -592,7 +507,7 @@ instance : Finite (Z F) := by
   simp only [mem_Z_iff]
   exact Finite.Set.finite_insert 1 {-1}
 
-lemma center_SL2_eq_Z (R : Type*)  [CommRing R] [NoZeroDivisors R]: center SL(2,R) = Z R := by
+lemma center_SL2_eq_Z (R : Type*) [CommRing R] [NoZeroDivisors R]: center SL(2,R) = Z R := by
   ext x
   constructor
   · intro hx
@@ -611,7 +526,6 @@ instance : Finite (center SL(2,F)) := by
   rw [center_SL2_eq_Z F]
   infer_instance
 
-
 lemma card_Z_eq_two_of_two_ne_zero [NeZero (2 : F)]: Nat.card (Z F) = 2 := by
   rw [Nat.card_eq_two_iff]
   use 1, ⟨-1, neg_one_mem_Z⟩
@@ -696,10 +610,8 @@ instance IsCyclic_Z : IsCyclic (Z F) := by
 
 instance IsCommutative_Z : IsMulCommutative (Z F) := inferInstance
 
-
 namespace IsPGroup
 
-
 /- Lemma 2.1. If G is a finite group of order pm where p is prime and m > 0,
 then p divides |Z(G)|.-/
 lemma p_dvd_card_center {H : Type*} {p : ℕ} (hp:  Nat.Prime p) [Group H] [Finite H] [Nontrivial H]
@@ -729,7 +641,6 @@ def SZ (F : Type*) [Field F] : Subgroup SL(2,F) where
     rintro x (⟨σ, rfl⟩ | ⟨σ, rfl⟩)
     repeat' simp
 
-
 def SZ' (F : Type*) [Field F] : Subgroup SL(2,F) where
   carrier := S F * Z F
   mul_mem' := by
@@ -801,7 +712,6 @@ lemma SZ_eq_SZ' {F : Type*} [Field F] : SZ' F = SZ F := by
       · simp
       · simp
 
-
 lemma S_mul_Z_subset_SZ :
   ((S F) : Set SL(2,F)) * ((Z F) : Set SL(2,F)) ⊆ ((SZ F) : Set SL(2,F)) := by
   rintro x ⟨t', ht', z, hz, hσ, h⟩
@@ -818,28 +728,15 @@ lemma S_mul_Z_subset_SZ :
   right
   use σ
   simp
-
--- ordering propositions so when proving it can be done more efficiently
-#check Set.mem_mul
-
-
 section CommutativeSubgroups
 
 lemma IsMulCommutative_iff {G : Type*} [Group G] {H : Subgroup G} :
   IsMulCommutative H ↔ ∀ x y : H, x * y = y * x := by
   constructor
-  · intro h x y
-    have := @mul_comm_of_mem_isMulCommutative G _ H h x y (by simp) (by simp)
-    exact SetLike.coe_eq_coe.mp this
-  · intro h
-    rw [← le_centralizer_iff_isMulCommutative]
-    intro y hy
-    rw [mem_centralizer_iff]
-    intro x hx
-    simp only [SetLike.mem_coe] at hx
-    specialize h ⟨x, hx⟩ ⟨y, hy⟩
-    simp only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] at h
-    exact h
+  . intro h x y
+    exact mul_comm x y
+  . intro h
+    exact {is_comm := { comm := h }}
 
 instance IsMulCommutative_D : IsMulCommutative (D F) := by
   rw [IsMulCommutative_iff]
@@ -866,7 +763,6 @@ end CommutativeSubgroups
 theorem val_eq_neg_one {a : Fˣ} : (a : F) = -1 ↔ a = (-1 : Fˣ) := by
   rw [Units.ext_iff, Units.coe_neg_one];
 
-
 lemma ex_of_card_D_gt_two {D₀ : Subgroup SL(2,F) }(hD₀ : 2 < Nat.card D₀) (D₀_leq_D : D₀ ≤ D F) :
   ∃ δ : Fˣ, (δ : F) ≠ 1 ∧ (δ : F) ≠ -1 ∧ d δ ∈ D₀ := by
   by_contra! h
@@ -890,10 +786,8 @@ lemma ex_of_card_D_gt_two {D₀ : Subgroup SL(2,F) }(hD₀ : 2 < Nat.card D₀)
     le_trans (Subgroup.card_le_of_le D₀_le_Z) card_Z_le_two
   linarith
 
-
 lemma mem_D_iff {x : SL(2,F)} : x ∈ D F ↔ ∃ δ : Fˣ, d δ = x := by rfl
 
-
 lemma mem_D_w_iff {x : SL(2,F)} : x ∈ (D F : Set SL(2,F)) * {w} ↔ ∃ δ : Fˣ, d δ * w = x := by
   constructor
   · rintro ⟨d', ⟨δ, rfl⟩, w, ⟨rfl⟩, rfl⟩
@@ -927,7 +821,4 @@ lemma S_join_Z_eq_SZ : S F ⊔ Z F = SZ F := by
         simp
       apply Subgroup.subset_closure mem_Z_mul_T
 
-
 end SpecialSubgroups
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S3_JordanNormalFormOfSL.lean b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S3_JordanNormalFormOfSL.lean
index 9e11c85..b34887f 100644
--- a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S3_JordanNormalFormOfSL.lean
+++ b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S3_JordanNormalFormOfSL.lean
@@ -1,8 +1,11 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S2_SpecialSubgroups
-import Mathlib
-
-set_option autoImplicit false
-set_option linter.style.longLine true
+import Mathlib.Algebra.GroupWithZero.Conj
+import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
+import Mathlib.RingTheory.Artinian.Instances
+import Mathlib.RingTheory.FiniteLength
+import Mathlib.RingTheory.PicardGroup
+import Mathlib.RingTheory.SimpleRing.Principal
 
 open Matrix MatrixGroups Subgroup Pointwise
 
@@ -69,7 +72,6 @@ lemma associated_of_dvd_mul_irreducibles {k : Type*} [Field k] {q p₁ p₂: k[X
       rw [q_eq, hk₁, hk₂, mul_assoc, ← mul_assoc k₁, mul_comm k₁, mul_assoc, ← mul_assoc,
       associated_mul_isUnit_right_iff (IsUnit.mul h₁ h₂)]
 
-
 lemma minpoly_eq_X_sub_C_implies_matrix_is_diagonal { n R : Type*} [Fintype n] [DecidableEq n]
      [ CommRing R ] [NoZeroDivisors R] {M : Matrix n n R} {a : R}
     (hM : minpoly R M = (X - C a)) : M = diagonal (fun _ ↦ a) := by
@@ -79,7 +81,6 @@ lemma minpoly_eq_X_sub_C_implies_matrix_is_diagonal { n R : Type*} [Fintype n] [
     -- This shows M is diagonal
     exact M_eq_diagonal
 
-
 /-
 The product of the top left entry and the bottom right entry equals one
 if the bottom left entry is zero.
@@ -107,7 +108,7 @@ A 2x2 matrix of the special linear group is diagonal, and can be written as `d 
 if and only if the bottom left and top right entries are zero.
 -/
 lemma SpecialLinearGroup.fin_two_diagonal_iff (x : SL(2,F)) :
-  x 0 1 = 0 ∧ x 1 0 = 0 ↔ ∃ δ : Fˣ, d δ = x := by
+  IsDiagonal x.val ↔ ∃ δ : Fˣ, d δ = x := by
   constructor
   · rintro ⟨hβ, hγ⟩
     rcases get_entries x with ⟨α, β, γ, δ, hα, -, -, hδ, -⟩
@@ -128,7 +129,7 @@ A 2x2 matrix of the special linear group is antidiagonal, and can be written as
 `d δ * w` for some `δ ∈ Fˣ` if and only if the top left and bottom right entries are zero.
 -/
 lemma SpecialLinearGroup.fin_two_antidiagonal_iff (x : SL(2,F)) :
-  x 0 0 = 0 ∧ x 1 1 = 0 ↔ ∃ δ : Fˣ, (d δ) * w = x := by
+  IsAntiDiagonal x.val ↔ ∃ δ : Fˣ, (d δ) * w = x := by
   constructor
   · rintro ⟨hα, hδ⟩
     have det_eq_one : det (x : Matrix (Fin 2) (Fin 2) F) = 1 := by rw [SpecialLinearGroup.det_coe]
@@ -267,7 +268,7 @@ lemma det_eq_det_IsConj {n : ℕ} {M N : Matrix (Fin n) (Fin n) R} (h : IsConj N
 If the underlying matrices are the same then the matrices
 as subtypes of the special linear group are also the same
 -/
-lemma SpecialLinearGroup.eq_of {S L : SL(2,F) } (h : (S : Matrix (Fin 2) (Fin 2) F) = L) :
+lemma SpecialLinearGroup.eq_of {S L : SL(2,F)} (h : (S : Matrix (Fin 2) (Fin 2) F) = L) :
   S = L := by ext <;> simp [h]
 
 lemma IsConj_coe {M N : Matrix (Fin 2) (Fin 2) F} (hM : det M = 1) (hN : det N = 1)
@@ -277,7 +278,6 @@ lemma IsConj_coe {M N : Matrix (Fin 2) (Fin 2) F} (hM : det M = 1) (hN : det N =
   apply SpecialLinearGroup.eq_of
   rw [SpecialLinearGroup.coe_mul, SpecialLinearGroup.coe_mul, hC]
 
-
 /-
 Lemma 1.5.
 Each element of SL(2,F) is conjugate to either
@@ -363,6 +363,3 @@ theorem SL2_IsConj_d_or_IsConj_s_or_IsConj_neg_s_of_AlgClosed [DecidableEq F] [I
     simp only [SpecialMatrices.d, IsUnit.unit_spec]
     -- conjugation is transitive
     apply IsConj.trans isConj₂.symm isConj₁.symm
-
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S4_PropertiesOfCentralizers.lean b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S4_PropertiesOfCentralizers.lean
index e142a70..099f84a 100644
--- a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S4_PropertiesOfCentralizers.lean
+++ b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S4_PropertiesOfCentralizers.lean
@@ -1,12 +1,8 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S3_JordanNormalFormOfSL
-import Mathlib
-
-set_option autoImplicit false
-set_option linter.style.longLine true
 
 open Matrix MatrixGroups Subgroup Pointwise
 
-open SpecialMatrices SpecialSubgroups
+open SpecialMatrices SpecialSubgroups MatrixShapes
 
 universe u
 
@@ -16,7 +12,7 @@ variable
   (R : Type u) [CommRing R]
   {G : Type u} [Group G]
 
-/- Proposition 1.6.ii C_L(± s σ) = T × Z where σ ≠ 0 -/
+/- Proposition 1.6.ii (positive part) C_L(s σ) = T × Z where σ ≠ 0 -/
 theorem centralizer_s_eq_SZ {σ : F} (hσ : σ ≠ 0) : centralizer { s σ } = SZ F := by
   ext x
   constructor
@@ -47,6 +43,13 @@ theorem centralizer_s_eq_SZ {σ : F} (hσ : σ ≠ 0) : centralizer { s σ } = S
     rw [hy]
     simp [add_comm]
 
+theorem centralizer_s_eq_neg_s {σ : F}:
+    centralizer { s σ } = centralizer { - s σ } := by
+  ext; constructor <;> simp [mem_centralizer_iff_commutator_eq_one]
+
+/-- Proposition 1.6.ii (negative part) C_L(- s σ) = T × Z where σ ≠ 0 -/
+theorem centralizer_s_eq_SZ_neg {σ : F} (hσ : σ ≠ 0) : centralizer { - s σ } = SZ F := by
+  rw [← centralizer_s_eq_neg_s, centralizer_s_eq_SZ hσ]
 
 lemma Field.self_eq_inv_iff (x : F) (x_ne_zero : x ≠ 0) : x = x⁻¹ ↔ x = 1 ∨ x = - 1 := by
   rw [← sq_eq_one_iff, sq, (mul_eq_one_iff_eq_inv₀ x_ne_zero)]
@@ -75,13 +78,12 @@ lemma centralizer_d_eq_D (δ : Fˣ) (δ_ne_one : δ ≠ 1) (δ_ne_neg_one : δ 
       refine Units.eq_or_eq_neg_of_sq_eq_sq δ 1 ?_
       rwa [one_pow, sq]
     rw [mul_comm, mul_eq_mul_left_iff] at hb hc
-    -- rw [ne_eq] at δ_ne_δ_inv
     have not_eq_inv : ¬ (δ : F)⁻¹ = (δ : F) := by
       norm_cast
       exact fun a ↦ δ_ne_δ_inv (congrArg Units.val (id (Eq.symm a)))
     replace hb : b = 0 := Or.resolve_left hb (Ne.symm not_eq_inv)
     replace hc : c = 0 := Or.resolve_left hc not_eq_inv
-    rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff]
+    rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff, IsDiagonal]
     simp [hb, hc, ← hb', ← hc']
   · rintro ⟨δ', rfl⟩
     simp [mem_centralizer_iff, mul_comm]
@@ -179,5 +181,3 @@ lemma IsMulCommutative_centralizer_of_not_mem_center [IsAlgClosed F] [DecidableE
       simp at hx
     rw [← centralizer_S_eq,  ← centralizer_neg_eq_centralizer, centralizer_s_eq_SZ σ_ne_zero]
     exact map_isMulCommutative _ _
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S5_PropertiesOfNormalizers.lean b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S5_PropertiesOfNormalizers.lean
index e3b6cbf..c5e4c63 100644
--- a/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S5_PropertiesOfNormalizers.lean
+++ b/ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S5_PropertiesOfNormalizers.lean
@@ -1,35 +1,17 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S3_JordanNormalFormOfSL
 
-
-
-set_option autoImplicit false
-set_option linter.style.longLine true
-
 open Matrix MatrixGroups Subgroup Pointwise
 
 open SpecialMatrices SpecialSubgroups MatrixShapes
 
 universe u
 
-
 variable
   {F : Type u} [Field F]
   (n : Type u) [Fintype n]
   (R : Type u) [CommRing R]
   {G : Type u} [Group G]
 
-
-
-/- Lemma 1.2.2.2 H ⧸ T = D -/
--- def quot_iso_subgroupGeneratedByD {F : Type* } [Field F] :
---   H F ⧸ T F ≃* D F := by sorry -- needs HasQuotient
-
-/- Lemma 1.3. Z(SL(2,F)) = ⟨ -I ⟩ .-/
--- def center_of_SL_2_F : center SL(2,F) ≃* rootsOfUnity 2 F  :=
---   Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' 2
-
-
-
 /-
 Proposition 1.6.i
 N_{SL(2,F)}(S₀) ⊆ L, where S₀ is any subgroup of S with order greater than 1.
@@ -123,11 +105,11 @@ lemma normalizer_subgroup_D_eq_DW { D₀ : Subgroup (SL(2,F)) }
       absurd zero_ne_one det_eq_one
       trivial
     · apply Dw_leq_DW
-      rw [mem_D_w_iff, ← SpecialLinearGroup.fin_two_antidiagonal_iff]
+      rw [mem_D_w_iff, ← SpecialLinearGroup.fin_two_antidiagonal_iff, IsAntiDiagonal]
       simp_rw [← hα, ← hδ, α_eq_zero, δ_eq_zero]
       trivial
     · apply D_leq_DW
-      rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff]
+      rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff, IsDiagonal]
       simp_rw [← hβ, ← hγ, β_eq_zero, γ_eq_zero]
       trivial
     · have det_eq_zero : det (x : Matrix (Fin 2) (Fin 2) F) = 0 := by
@@ -189,5 +171,3 @@ lemma normalizer_subgroup_D_eq_DW { D₀ : Subgroup (SL(2,F)) }
             d_mul_d_eq_d_mul, ← mul_assoc, mul_inv_cancel_comm] at conj_mem_D₀
         rw [← inv_d_eq_d_inv]
         exact Subgroup.inv_mem D₀ conj_mem_D₀
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S1_ElementaryAbelian.lean b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S1_ElementaryAbelian.lean
index f2b95e9..a9e705a 100644
--- a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S1_ElementaryAbelian.lean
+++ b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S1_ElementaryAbelian.lean
@@ -2,16 +2,11 @@ import Mathlib.Data.Nat.Factorization.PrimePow
 import Mathlib.GroupTheory.PGroup
 import Mathlib.Order.CompletePartialOrder
 
-
-set_option linter.style.longLine true
-set_option autoImplicit false
 set_option maxHeartbeats 0
 set_option synthInstance.maxHeartbeats 0
 
 open Subgroup
 
-
-
 structure ElementaryAbelian (p : ℕ) (G : Type*) [Group G] extends Subgroup G where
   is_comm : IsMulCommutative toSubgroup
   orderOf_eq : ∀ h : toSubgroup, h ≠ 1 → orderOf h = p
@@ -105,5 +100,3 @@ lemma subgroupOf {G : Type*} [Group G]
     simp [← order_of_eq_p']
 
 end IsElementaryAbelian
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S2_MaximalAbelianSubgroup.lean b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S2_MaximalAbelianSubgroup.lean
index 0873781..863b95e 100644
--- a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S2_MaximalAbelianSubgroup.lean
+++ b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S2_MaximalAbelianSubgroup.lean
@@ -1,10 +1,10 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S4_PropertiesOfCentralizers
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S5_PropertiesOfNormalizers
 import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S1_ElementaryAbelian
-import Mathlib
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Data.Int.Star
+import Mathlib.FieldTheory.Finite.Basic
 
-set_option linter.style.longLine true
-set_option autoImplicit false
 set_option maxHeartbeats 0
 set_option synthInstance.maxHeartbeats 0
 set_option linter.unusedTactic false
@@ -1813,5 +1813,3 @@ theorem K_mem_MaximalAbelianSubgroups_of_center_lt_card_K {F : Type*} [Field F]
   sorry
 
 end MaximalAbelianSubgroup
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S3_NoncenterClassEquation.lean b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S3_NoncenterClassEquation.lean
index 07e1397..8f8f8a3 100644
--- a/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S3_NoncenterClassEquation.lean
+++ b/ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S3_NoncenterClassEquation.lean
@@ -1,15 +1,8 @@
 import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S2_MaximalAbelianSubgroup
-import Mathlib
-
-set_option linter.style.longLine true
-set_option autoImplicit false
-set_option maxHeartbeats 0
-set_option synthInstance.maxHeartbeats 0
-
+import Mathlib.Data.Setoid.Partition
 
 universe u
 
-
 open Matrix MatrixGroups Subgroup MulAut MaximalAbelianSubgroup Pointwise SpecialSubgroups
 
 
@@ -80,8 +73,6 @@ def Partition_lift_noncenter_MaximalAbelianSubgroupsOf {F : Type*} [Field F] (G
 
 #check Setoid.IsPartition.sUnion_eq_univ
 
-#check sUnion_memPartition
-
 #check Set
 /-
 Define $C (A)^* = \bicup_{x \in G} x A^*  x^{-1}$
@@ -605,11 +596,6 @@ lemma card_noncenter_C_eq_noncenter_MaximalAbelianSubgroup_mul_noncenter_ConjCla
 
   sorry
 
-#check Group.nat_card_center_add_sum_card_noncenter_eq_card
-
-#check Group.card_center_add_sum_card_noncenter_eq_card
-
-
 -- lemma card_noncenter_C_eq_of_related {F : Type*} [Field F] (G : Subgroup SL(2,F)) [Finite G] :
 --   ∀ (A B : noncenter_MaximalAbelianSubgroupsOf G),
 --     A ≈ B → card_noncenter_C G A = card_noncenter_C G B := by
@@ -762,7 +748,3 @@ lemma normalizer_Sylow_join_center_eq_normalizer_Sylow {F : Type*} [Field F] {p
   normalizer (map G.subtype Q.toSubgroup ⊔ center SL(2,F)) =
     normalizer (map G.subtype Q.toSubgroup) := by
   sorry
-
-
-
-#min_imports
diff --git a/ClassificationOfSubgroups/Ch7_DicksonsClassificationTheorem.lean b/ClassificationOfSubgroups/Ch7_DicksonsClassificationTheorem.lean
index a7ee3c8..298afce 100644
--- a/ClassificationOfSubgroups/Ch7_DicksonsClassificationTheorem.lean
+++ b/ClassificationOfSubgroups/Ch7_DicksonsClassificationTheorem.lean
@@ -1,19 +1,19 @@
 import ClassificationOfSubgroups.Ch4_PGLIsoPSLOverAlgClosedField.ProjectiveGeneralLinearGroup
 import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S2_MaximalAbelianSubgroup
+import ClassificationOfSubgroups.Ch4_PGLIsoPSLOverAlgClosedField.ProjectiveGeneralLinearGroup
+import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S2_MaximalAbelianSubgroup
 import Mathlib.FieldTheory.Finite.GaloisField
-import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.GroupTheory.PresentedGroup
 import Mathlib.GroupTheory.SpecificGroups.Alternating
-import Mathlib.GroupTheory.QuotientGroup.Basic
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
+import Mathlib.GroupTheory.SpecificGroups.Dihedral
 
-set_option linter.style.longLine true
 set_option maxHeartbeats 0
 
 open Matrix Subgroup LinearMap
 
 open scoped MatrixGroups
 
+universe u v
 
 /- Lemma 3.1 -/
 lemma IsPGroup.not_le_normalizer {F : Type*} [Field F] {p : ℕ} [Fact (Nat.Prime p)]
@@ -39,12 +39,11 @@ def R (F : Type*) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p](k : ℕ+)
 instance field_R {F : Type*} [Field F] {p : ℕ} [Fact (Nat.Prime p)]
   [CharP F p] {k : ℕ+} : Field (R F p k) := by sorry
 
-/- Lemma 3.4 -/
-#check Matrix.card_GL_field
+/- Lemma 3.4 Matrix.card_GL_field -/
 
 -- abbrev SL := Matrix.SpecialLinearGroup
 
-lemma card_SL_field {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) :
+lemma card_SL_field {𝔽 : Type u} [Field 𝔽] [Fintype 𝔽] (n : ℕ) :
   Nat.card (SL (Fin n) 𝔽) = Nat.card (GL (Fin n) 𝔽) / (Fintype.card 𝔽 - 1) := by sorry
 
 /- Lemma 3.5. Correspondence theorem -/
@@ -212,8 +211,8 @@ instance five_prime : Fact (Nat.Prime 5) := { out := by decide }
 
 /- Theorem 3.6 -/
 theorem dicksons_classification_theorem_class_I {F : Type*} [Field F] [IsAlgClosed F]
-  {p : ℕ} [CharP F p] (hp : Prime p) (hp' : p = 0 ∨ Nat.Coprime (Nat.card G) p)
-  (G : Subgroup (SL(2,F)))  [Finite G] :
+  {p : ℕ} [CharP F p] (hp : Prime p) (G : Subgroup (SL(2,F))) [Finite G]
+   (hp' : p = 0 ∨ Nat.Coprime (Nat.card G) p) :
   IsCyclic G ∨
   Isomorphic G (DihedralGroup n)
   ∨
@@ -281,5 +280,3 @@ theorem FLT_classification_fin_subgroups_of_PGL2_over_AlgClosure_ZMod {p : ℕ}
   ∨
   Isomorphic G (PGL (Fin 2) (𝕂)) := by
     sorry
-
-#min_imports
diff --git a/lakefile.toml b/lakefile.toml
index 5b3787c..4002361 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -5,6 +5,8 @@ defaultTargets = ["ClassificationOfSubgroups"]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+autoImplicit = false
+linter.style.longLine = true
 
 [[require]]
 name = "mathlib"