bump mathlib dependancies

Author: AlexBrodbelt

ClassificationOfSubgroups/Ch4_PGLIsoPSLOverAlgClosedField/ProjectiveGeneralLinearGroup.lean

@@ -89,8 +89,7 @@ theorem mem_center_general_linear_group_iff {n : Type u} [DecidableEq n]
     intro hM N
     obtain ⟨r, rfl⟩ := hM
     ext i j
-    simp [GeneralLinearGroup.coe_mul, GeneralLinearGroup.coe_mul,
-      ← coe_scalar_matrix, scalar_commute]
+    simp
 
 end Center
 
@@ -188,10 +187,10 @@ lemma exists_SL_eq_scaled_GL_of_IsAlgClosed {n F : Type*} [hn₁ : Fintype n] [D
     simp [hα]
   obtain ⟨α, hα⟩ := hα'
   have det_inv_c_G_eq_one : det (α⁻¹ • G).1 = (1 : F) := by
-    simp [← hα, inv_smul_eq_iff, Units.smul_def]
+    simp [← hα, Units.smul_def]
   use α, ⟨(α⁻¹ • G), det_inv_c_G_eq_one⟩
   ext
-  simp [coe]
+  simp
 
 open Function
 
@@ -206,7 +205,7 @@ instance (n R : Type*) [Fintype n] [DecidableEq n] [CommRing R] :
   refine IsScalarTower.of_smul_one_mul ?_
   intro r g
   ext
-  simp [GeneralLinearGroup.coe_mul]
+  simp
 
 
 theorem Injective_PSL_monoidHom_PGL  (n F : Type*) [hn₁ : Fintype n] [DecidableEq n]
@@ -235,7 +234,7 @@ theorem SpecialLinearGroup.toGL_inj {n : Type*} [DecidableEq n] [Fintype n] {R :
   [CommRing R] : Injective (@SpecialLinearGroup.toGL n _ _ R _) := by
   refine (injective_iff_map_eq_one SpecialLinearGroup.toGL).mpr ?_
   intro x hx
-  simp [GeneralLinearGroup.ext_iff, coe] at hx
+  simp [GeneralLinearGroup.ext_iff] at hx
   ext i j
   exact hx i j
 
@@ -258,7 +257,7 @@ theorem ker_SL_monoidHom_PGL_eq_center (n F : Type*) [hn₁ : Fintype n] [Decida
     simp [mem_center_iff]
     intro y
     ext i j
-    simp [coe, ← hr]
+    simp [← hr]
     exact CommMonoid.mul_comm (y i j) r
 
 theorem Surjective_PSL_monoidHom_PGL (n F : Type*) [hn₁ : Fintype n] [DecidableEq n]
@@ -274,9 +273,7 @@ theorem Surjective_PSL_monoidHom_PGL (n F : Type*) [hn₁ : Fintype n] [Decidabl
     suffices c⁻¹ • 1 * G = S by
       simp [← h]
       ext
-      simp [GeneralLinearGroup.scalar,
-        nonsing_inv_mul _ <| isUnits_det_units (SpecialLinearGroup.toGL S),
-        ← Matrix.smul_one_eq_diagonal]
+      simp
     rw [← h, smul_mul_assoc, one_mul, inv_smul_eq_iff]
   rw [← hG, class_G_eq_class_S]
   -- by definition these equivalence classes are the same

ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S1_SpecialMatrices.lean

@@ -103,7 +103,7 @@ lemma d_eq_diagonal (δ : Fˣ) :
 lemma d_one_eq_one : d (1 : Fˣ) = 1 := by ext <;> simp [d]
 
 @[simp]
-lemma d_neg_one_eq_neg_one : d (-1 : Fˣ) = -1 := by ext <;> simp [d, inv_neg_one]
+lemma d_neg_one_eq_neg_one : d (-1 : Fˣ) = -1 := by ext <;> simp [d]
 
 @[simp]
 lemma neg_d_eq_d_neg (δ : Fˣ) : - d δ = d (-δ) :=  by ext <;> simp [d, inv_neg]

ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S2_SpecialSubgroups.lean

@@ -85,7 +85,7 @@ lemma diagonal_iff_upper_and_lower {M: Matrix (Fin 2) (Fin 2) F} :
     obtain ⟨a, b, d, hM_upper⟩ := h_upper
     obtain ⟨a', c, d', hM_lower⟩ := h_lower
     use a, d
-    ext <;> simp [← hM_upper, ← hM_lower]
+    ext <;> simp [← hM_upper]
     have : b = M 0 1 := by rw [← hM_upper]; rfl
     rw [this]
     rw [← hM_lower]
@@ -127,6 +127,10 @@ def D_iso_units (F : Type*) [Field F] : SpecialSubgroups.D F ≃* Fˣ where
                 repeat'
                   simp_rw [← hδ₁, ← hδ₂]
                   simp [SpecialMatrices.d, mul_comm]
+@[simp]
+lemma d_mem_D {F : Type*} [Field F] {δ : Fˣ} : d δ ∈ D F := by
+  use δ
+
 
 end Diagonal
 section Shear
@@ -175,9 +179,8 @@ lemma D_meet_S_eq_bot (F : Type*) [Field F] : D F ⊓ S F = ⊥ := by
   · intro h
     simp at h
     constructor
-    · simp [h]; exact Subgroup.one_mem (D F)
-    · simp [h]; exact Subgroup.one_mem (S F)
-
+    · simp [h]
+    · simp [h]
 /--
   This is H in the notes.
 -/
@@ -190,7 +193,7 @@ def L (F : Type*) [Field F] : Subgroup SL(2,F) where
               ext
               · simp [d, s]
               · simp [d, s]
-              · field_simp [d, s]; ring
+              · simp [d, s]; field_simp
               · simp [d, s, mul_comm]
   one_mem' := ⟨1, 0, by simp⟩
   inv_mem' := by
@@ -220,12 +223,16 @@ lemma mem_L_iff_lower_triangular [DecidableEq F] {x : SL(2,F)} :
     have a_is_unit : IsUnit a := isUnit_of_mul_eq_one a d had
     have a_inv_eq_d : a⁻¹ = d := DivisionMonoid.inv_eq_of_mul a d had
     use a_is_unit.unit, c * a_is_unit.unit
-    simp [SpecialMatrices.d, SpecialMatrices.s, had]
-    ext <;> field_simp [a_inv_eq_d, had, ← hx]; exact (eq_one_div_of_mul_eq_one_right had).symm
+    simp [SpecialMatrices.d, SpecialMatrices.s]
+    ext <;>
+    simp [← a_inv_eq_d, ← hx]
+    rw [← mul_assoc]
+    have a_ne_zero : a ≠ 0 := left_ne_zero_of_mul_eq_one had
+    field_simp [a_ne_zero]
 
 lemma S_le_L : S F ≤ L F := by
   rintro x ⟨σ, rfl⟩
-  rw [L, mem_mk, Set.mem_setOf_eq]
+  rw [L, mem_mk]
   use 1, σ
   rw [d_one_eq_one, one_mul]
 
@@ -250,7 +257,7 @@ lemma normal_S_subgroupOf_L {F : Type*} [Field F] : ((S F).subgroupOf (L F)).Nor
         inv_d_eq_d_inv, mul_assoc, mul_assoc (s (-σ)), ← mul_assoc (s σ'),
         ← mul_assoc (d δ⁻¹), ← mul_assoc (d δ⁻¹), d_eq_inv_d_inv δ,
         d_mul_s_mul_d_inv_eq_s, s_mul_s_eq_s_add, s_mul_s_eq_s_add]
-      rw [S, inv_inv, neg_add_cancel_comm_assoc, mem_mk, Set.mem_setOf_eq]
+      rw [S, inv_inv, neg_add_cancel_comm_assoc, mem_mk]
       use σ' * (δ : F) * (δ : F)
     · rintro ⟨σ', hσ'⟩
       rw [mem_subgroupOf]
@@ -338,23 +345,8 @@ lemma D_join_S_eq_L (F : Type*) [Field F]: D F ⊔ S F = L F := by
     rfl
 
 
--- def foo {G : Type*} [Group G] (H K : Subgroup G) : (H ⊔ K :) ⧸ K ≃* H := by sorry
 
 
--- noncomputable def pi : (L F) →* (D F) where
---   toFun := fun l => ⟨d (l.property.choose), ⟨l.property.choose, rfl⟩⟩
---   map_one' := by
---     have d_one_in_L : d 1 * s 0 ∈ L F := ⟨1, 0, by simp⟩
---     have one_eq_d_one : (⟨d 1 * s 0, d_one_in_L⟩ : L F) = 1 := by simp
---     have : Exists.choose (⟨d 1 * s 0, d_one_in_L⟩ : L F).property = 1 := by sorry
---     rw [← one_eq_d_one]
---     ext
---     · simp only [Fin.isValue, OneMemClass.coe_one, SpecialLinearGroup.coe_one, one_apply_eq]
---       sorry
---     · exact rfl
---     · exact rfl
---     · sorry
---   map_mul' := by sorry
 
 -- second isomorphism theorem!!!!
 #check QuotientGroup.quotientInfEquivProdNormalQuotient
@@ -499,15 +491,15 @@ def DW (F : Type*) [Field F] : Subgroup SL(2,F) where
 
 lemma D_leq_DW : D F ≤ DW F := by
   rintro x ⟨δ, rfl⟩
-  rw [DW, mem_mk, Set.mem_union, Set.mem_setOf_eq]
+  rw [DW, mem_mk]
   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
   rintro x ⟨d', hd', w, hw, rfl⟩
   obtain ⟨δ, rfl⟩ := hd'
-  rw [DW, coe_set_mk, Set.mem_union, Set.mem_setOf_eq]
+  rw [DW, coe_set_mk]
   right
   use δ
   rw [Set.mem_singleton_iff] at hw
@@ -578,8 +570,7 @@ lemma Field.one_eq_neg_one_of_two_eq_zero (two_eq_zero : (2 : F) = 0) : 1 = (-1
 lemma SpecialLinearGroup.neg_one_eq_one_of_two_eq_zero (two_eq_zero : (2 : F) = 0) :
   1 = (-1 : SL(2,F)) := by
   ext
-  <;> simp [Field.one_eq_neg_one_of_two_eq_zero]
-  <;> exact Field.one_eq_neg_one_of_two_eq_zero two_eq_zero
+  <;> simpa using Field.one_eq_neg_one_of_two_eq_zero two_eq_zero
 
 
 
@@ -626,7 +617,7 @@ lemma card_Z_eq_two_of_two_ne_zero [NeZero (2 : F)]: Nat.card (Z F) = 2 := by
   use 1, ⟨-1, neg_one_mem_Z⟩
   split_ands
   · intro h
-    rw [Subtype.ext_val_iff] at h
+    rw [Subtype.ext_iff] at h
     -- -1 ≠ 1 for characteristic different to 2
     simp at h
   · rw [Set.eq_univ_iff_forall]
@@ -703,7 +694,7 @@ instance IsCyclic_Z : IsCyclic (Z F) := by
     rw [card_Z_eq_one_of_two_eq_zero two_eq_zero]
     simp only [orderOf_eq_one_iff, exists_eq]
 
-instance IsCommutative_Z : IsCommutative (Z F) := inferInstance
+instance IsCommutative_Z : IsMulCommutative (Z F) := inferInstance
 
 
 namespace IsPGroup
@@ -834,14 +825,14 @@ lemma S_mul_Z_subset_SZ :
 
 section CommutativeSubgroups
 
-lemma IsCommutative_iff {G : Type*} [Group G] (H : Subgroup G) :
-  IsCommutative H ↔ ∀ x y : H, x * y = y * x := by
+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_isCommutative G _ H h x y (by simp) (by simp)
+    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_isCommutative]
+    rw [← le_centralizer_iff_isMulCommutative]
     intro y hy
     rw [mem_centralizer_iff]
     intro x hx
@@ -850,20 +841,20 @@ lemma IsCommutative_iff {G : Type*} [Group G] (H : Subgroup G) :
     simp only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] at h
     exact h
 
-instance IsCommutative_D : IsCommutative (D F) := by
-  rw [IsCommutative_iff]
+instance IsMulCommutative_D : IsMulCommutative (D F) := by
+  rw [IsMulCommutative_iff]
   rintro ⟨x, ⟨δ₁, hδ₁⟩⟩ ⟨y, ⟨δ₂, hδ₂⟩⟩
-  simp [Subtype.ext_val_iff, coe_mul, ← hδ₁, ← hδ₂, mul_comm]
+  simp [← hδ₁, ← hδ₂, mul_comm]
 
-instance IsCommutative_S (F : Type*) [Field F] : IsCommutative (S F) := by
-  rw [IsCommutative_iff]
+instance IsMulCommutative_S (F : Type*) [Field F] : IsMulCommutative (S F) := by
+  rw [IsMulCommutative_iff]
   rintro ⟨x, ⟨σ₁, hσ₁⟩⟩ ⟨y, ⟨σ₂, hσ₂⟩⟩
-  simp [@Subtype.ext_val_iff]
+  simp [Subtype.ext_iff]
   rw [← hσ₁, ← hσ₂]
   simp [add_comm]
 
-instance IsCommutative_SZ (F : Type*) [Field F] : IsCommutative (SZ F) := by
-  refine le_centralizer_iff_isCommutative.mp ?_
+instance IsMulCommutative_SZ (F : Type*) [Field F] : IsMulCommutative (SZ F) := by
+  refine le_centralizer_iff_isMulCommutative.mp ?_
   rintro x (⟨σ₁, rfl⟩ | ⟨σ₁, rfl⟩)
   repeat
   rw [mem_centralizer_iff]
@@ -923,15 +914,15 @@ lemma S_join_Z_eq_SZ : S F ⊔ Z F = SZ F := by
         rw [Set.mem_mul]
         use s σ
         split_ands
-        simp [Z, closure_neg_one_eq]
+        simp only [SetLike.mem_coe]
         use σ
         simp
       apply Subgroup.subset_closure mem_Z_mul_S
     · have mem_Z_mul_T : -s σ ∈ ((S F) : Set SL(2,F)) * (Z F) := by
         rw [Set.mem_mul]
         use s σ
         split_ands
-        simp [Z, closure_neg_one_eq]
+        simp only [SetLike.mem_coe]
         use σ
         simp
       apply Subgroup.subset_closure mem_Z_mul_T

ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S3_JordanNormalFormOfSL.lean

@@ -1,10 +1,5 @@
 import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S2_SpecialSubgroups
-import Mathlib.Algebra.GroupWithZero.Conj
-import Mathlib.FieldTheory.IsAlgClosed.Basic
-import Mathlib.LinearAlgebra.FreeModule.PID
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
-import Mathlib.RingTheory.Artinian.Instances
-import Mathlib.RingTheory.FiniteLength
+import Mathlib
 
 set_option autoImplicit false
 set_option linter.style.longLine true
@@ -57,8 +52,8 @@ lemma associated_of_dvd_mul_irreducibles {k : Type*} [Field k] {q p₁ p₂: k[X
   rcases hp₂ with ⟨-, hp₂⟩
   rcases hd₁ with ⟨k₁, hk₁⟩
   rcases hd₂ with ⟨k₂, hk₂⟩
-  specialize hp₁ d₁ k₁ hk₁
-  specialize hp₂ d₂ k₂ hk₂
+  specialize hp₁ hk₁
+  specialize hp₂ hk₂
   rcases hp₁ with (h₁ | h₁)
   · rcases hp₂ with (h₂ | h₂)
     · left
@@ -194,7 +189,8 @@ lemma Matrix.conj_s_eq {x : F} {a b c d : F} :
   s x * !![a, b; c, d] * s (-x) =
   !![-b * x + a, b; (-b) * x * x + (a -d) * x + c, b*x + d] := by
   simp [s]
-  ext; ring_nf
+  ring_nf
+  trivial
 
 def SpecialLinearGroup.mk' {n : ℕ} (M : Matrix (Fin n) (Fin n) F) (h : det M = 1) : SL(n, F) :=
   ⟨M, h⟩
@@ -212,13 +208,13 @@ theorem isTriangularizable_of_algClosed [DecidableEq F] [IsAlgClosed F]
   by_cases hβ : β ≠ 0
   · obtain ⟨σ, hσ⟩ := exists_root_of_special_poly α β γ δ hβ
     use s σ
-    simp [M_coe_eq, s, Matrix.conj_s_eq]
+    simp [M_coe_eq, s]
     ring_nf at hσ ⊢
     exact hσ
   simp at hβ
   · use w
     rw [upper_triangular_iff]
-    simp [M_coe_eq, w, inv_def, hβ]
+    simp [M_coe_eq, w, hβ]
 
 /-
 A 2x2 upper triangular matrix is conjugate to a diagonal matrix if `a ≠ d`
@@ -227,7 +223,6 @@ lemma upper_triangular_isConj_diagonal_of_nonzero_det  [DecidableEq F]
   {a b d : F} (had : a - d ≠ 0) : ∃ C : SL(2,F), C * !![a, b; 0, d] * C⁻¹ = !![a, 0; 0, d] := by
   use ⟨!![1, b / (a - d); 0, 1], by simp⟩
   simp
-  ext
   repeat'
   field_simp
   ring_nf
@@ -239,8 +234,7 @@ lemma upper_triangular_isConj_jordan {a b : F} (hb : b ≠ 0) :
   IsConj !![a, b; 0, a] !![a, 1; 0, a] := by
   use GeneralLinearGroup.mk' !![1 / b, 0; 0, 1]
     (by simp; apply invertibleOfNonzero <| inv_ne_zero hb)
-  ext
-  repeat' field_simp
+  ext <;> simp <;> field_simp
 
 /-
 A 2x2 lower triangular matrix is conjugate to an upper triangular matrix
@@ -307,7 +301,7 @@ theorem SL2_IsConj_d_or_IsConj_s_or_IsConj_neg_s_of_AlgClosed [DecidableEq F] [I
   -- Because !![a, b; 0, d] is conjugate to S it also has determinant 1
   have det_eq_one : det !![a, b; 0, d] = 1 := by
     rw [← det_coe_S_eq_one, h]
-    simp only [det_mul, SpecialLinearGroup.det_coe, mul_one, one_mul]
+    simp only [det_mul, SpecialLinearGroup.det_coe, mul_one]
   have had := det_eq_one
   -- The determinant being equal to 1 implies a * d = 1
   simp at had