perf: speed up InfiniteConnesRigidity proofs and imports

LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean

@@ -7,28 +7,22 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import Mathlib.Algebra.Group.MinimalAxioms
-public import Mathlib.Algebra.Module.ZMod
 public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-public import Mathlib.Data.Finsupp.Encodable
 public import Mathlib.Data.Finsupp.Pointwise
 public import Mathlib.GroupTheory.SemidirectProduct
-public import Mathlib.LinearAlgebra.Countable
-public import Mathlib.MeasureTheory.Function.ContinuousMapDense
 public import Mathlib.MeasureTheory.Function.Holder
 public import Mathlib.MeasureTheory.Function.L2Space
-public import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
-public import Mathlib.MeasureTheory.Group.Integral
-public import Mathlib.MeasureTheory.Measure.Regular
-public import Mathlib.RingTheory.DedekindDomain.Dvr
-public import Mathlib.RingTheory.KrullDimension.Polynomial
-public import Mathlib.RingTheory.Localization.Algebra
 public import Mathlib.Topology.Algebra.PontryaginDual
-public import Mathlib.Topology.Constructions
-public import Mathlib.Topology.ContinuousMap.SecondCountableSpace
-public import Mathlib.Topology.ContinuousMap.StoneWeierstrass
 public import Mathlib.Topology.Instances.ZMod
-public import Mathlib.Topology.Metrizable.Urysohn
 public import LeanPool.InfiniteConnesRigidity.UniversalLattice
+import Mathlib.LinearAlgebra.Countable
+import Mathlib.MeasureTheory.Function.ContinuousMapDense
+import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
+import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.RingTheory.KrullDimension.Polynomial
+import Mathlib.Topology.ContinuousMap.SecondCountableSpace
+import Mathlib.Topology.ContinuousMap.StoneWeierstrass
+import Mathlib.Topology.Metrizable.Urysohn
 
 /-!
 # Carry groups, duality, and crossed products
@@ -1919,15 +1913,12 @@ private theorem cornulierColumnRootProduct_apply (v : Index → IntegralPolynomi
           (show (2 : Index) ≠ cornulierLast by decide) (v 2) :
       IntegralSpecialLinearGroup) p q = _
   fin_cases p <;> fin_cases q <;>
-    simp only [cornulierLast, Fin.isValue, Nat.reduceAdd, Fin.zero_eta,
-      Matrix.SpecialLinearGroup.coe_mul,
-      Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply,
-      Matrix.add_apply, Matrix.one_apply, Matrix.single_apply, true_and,
-      Fin.sum_univ_four, ↓reduceIte, Fin.reduceEq, add_zero, one_ne_zero,
-      false_and, mul_ite, mul_one, mul_zero, zero_ne_one, zero_mul, ite_self,
-      zero_add, and_false,
-      Finset.sum_ite_eq', Finset.mem_univ, Fin.mk_one, Fin.reduceFinMk,
-      and_true, ite_mul, one_mul, Finset.sum_ite_eq]
+    simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk,
+      ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq,
+      ↓reduceIte,
+      Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply,
+      Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, mul_one,
+      mul_zero, add_zero, zero_add]
 
 /-- Cross-module support for the infinite Connes-rigidity construction. -/
 private def cornulierRowRootProduct (v : Index → IntegralPolynomial) :
@@ -1962,15 +1953,12 @@ private theorem cornulierRowRootProduct_apply (v : Index → IntegralPolynomial)
           (show cornulierLast ≠ (2 : Index) by decide) (v 2) :
       IntegralSpecialLinearGroup) p q = _
   fin_cases p <;> fin_cases q <;>
-    simp only [cornulierLast, Fin.isValue, Nat.reduceAdd, Fin.zero_eta,
-      Matrix.SpecialLinearGroup.coe_mul,
-      Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply,
-      Matrix.add_apply, Matrix.one_apply, Matrix.single_apply, true_and,
-      Fin.sum_univ_four, ↓reduceIte, Fin.reduceEq, add_zero, one_ne_zero,
-      false_and, mul_ite, mul_one, mul_zero, zero_ne_one, zero_mul, ite_self,
-      zero_add, and_false,
-      Finset.sum_ite_eq', Finset.mem_univ, Fin.mk_one, Fin.reduceFinMk,
-      and_true, ite_mul, one_mul, Finset.sum_ite_eq]
+    simp only [cornulierLast, Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk,
+      ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq,
+      ↓reduceIte,
+      Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply,
+      Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true, mul_one,
+      mul_zero, add_zero, zero_add]
 
 /-- Cross-module support for the infinite Connes-rigidity construction. -/
 private theorem cornulier_conjugate_K₁_root_mem
@@ -4384,7 +4372,8 @@ def coordinateProduct : V →ₗ[F] V →ₗ[F] V where
         apply auxiliaryBasis.repr.injective
         ext i
         simp only [map_smul, Basis.repr_symm_apply, Basis.repr_linearCombination, Finsupp.mul_apply,
-          Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, mul_left_comm, RingHom.id_apply] }
+          Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
+        ring }
   map_add' x y := by
     apply LinearMap.ext
     intro z
@@ -6276,9 +6265,12 @@ public
 def kDLinear : K →* (D ≃ₗ[F] D) where
   toFun k := (kLinear k).prodCongr (kDividedSquareLinear k)
   map_one' := by
-    ext d <;> simp
+    ext d <;>
+      simp only [map_one, LinearEquiv.prodCongr_apply, LinearEquiv.coe_one, id_eq, Prod.mk.eta]
   map_mul' k l := by
-    ext d <;> simp
+    ext d <;>
+      simp only [map_mul, LinearEquiv.prodCongr_apply, LinearEquiv.mul_apply, kLinear_apply,
+        kDividedSquareLinear_val]
 
 
 
@@ -7113,13 +7105,13 @@ def crossedIndexEquiv
         ⟨fun k ↦ ξ (e.symm k), by
           change Memℓp (fun k ↦ ξ (e.symm k)) 2
           rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)]
-          exact (e.symm.summable_iff).2
+          exact (e.symm.summable_iff (f := fun i ↦ ‖ξ i‖ ^ (2 : ℝ≥0∞).toReal)).2
             ((lp.memℓp ξ).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩
       invFun := fun ξ ↦
         ⟨fun k ↦ ξ (e k), by
           change Memℓp (fun k ↦ ξ (e k)) 2
           rw [memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal)]
-          exact (e.summable_iff).2
+          exact (e.summable_iff (f := fun i ↦ ‖ξ i‖ ^ (2 : ℝ≥0∞).toReal)).2
             ((lp.memℓp ξ).summable (by norm_num : 0 < (2 : ℝ≥0∞).toReal))⟩
       left_inv := by
         intro ξ

LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean

@@ -3449,8 +3449,7 @@ private def gammaGroupFactorUnitary (n : ℕ) :
 private def lambdaGroupFactorUnitary :
     GroupL2 lambdaGroup ≃ₗᵢ[ℂ]
       crossedHilbert paperSplitHaarAction := by
-  change GroupL2 (SemidirectProduct (Multiplicative D) K kDAction) ≃ₗᵢ[ℂ]
-    crossedHilbert paperSplitHaarAction
+  change GroupL2 Lambda ≃ₗᵢ[ℂ] crossedHilbert paperSplitHaarAction
   exact groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv
 
 end
@@ -3730,12 +3729,8 @@ private theorem lambdaGroupFactorUnitary_conj_inr (k : K) :
         paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap := by
   change
     (groupFactorUnitary kDAction paperSplitHaarAction splitFourierEquiv).conjStarAlgEquiv
-      (leftRegularUnitary
-        (SemidirectProduct.inr k :
-          SemidirectProduct (Multiplicative D) K kDAction) :
-          GroupL2 (SemidirectProduct (Multiplicative D) K kDAction)
-            →L[ℂ]
-          GroupL2 (SemidirectProduct (Multiplicative D) K kDAction)) =
+      (leftRegularUnitary (SemidirectProduct.inr k : Lambda) :
+          GroupL2 Lambda →L[ℂ] GroupL2 Lambda) =
       (crossedGroupUnitary paperSplitHaarAction k).toContinuousLinearEquiv.toContinuousLinearMap
   apply groupFactorUnitary_conj_inr
   exact splitTaggedFourierCovariance
@@ -3847,17 +3842,17 @@ private def toStarAlgEquiv (U : PaperFactorUnitaryWitness G H) :
     exact U.unitary.conjStarAlgEquiv.apply_symm_apply y
   map_mul' x y := by
     apply Subtype.ext
-    exact map_mul U.unitary.conjStarAlgEquiv
+    exact U.unitary.conjStarAlgEquiv.map_mul'
       (x : GroupL2 G →L[ℂ] GroupL2 G)
       (y : GroupL2 G →L[ℂ] GroupL2 G)
   map_add' x y := by
     apply Subtype.ext
-    exact map_add U.unitary.conjStarAlgEquiv
+    exact U.unitary.conjStarAlgEquiv.map_add'
       (x : GroupL2 G →L[ℂ] GroupL2 G)
       (y : GroupL2 G →L[ℂ] GroupL2 G)
   map_star' x := by
     apply Subtype.ext
-    exact map_star U.unitary.conjStarAlgEquiv
+    exact U.unitary.conjStarAlgEquiv.map_star'
       (x : GroupL2 G →L[ℂ] GroupL2 G)
   map_smul' c x := by
     apply Subtype.ext
@@ -5115,7 +5110,6 @@ private structure PaperAnalyticInput where
 
 /-- Cross-module support for the infinite Connes-rigidity construction. -/
 private theorem paperLambda_hasNoOrderFour : HasNoOrderFour Lambda := by
-  change HasNoOrderFour (SemidirectProduct (Multiplicative D) K kDAction)
   apply semidirect_hasNoOrderFour_of_no_nontrivial_torsion_of_exponentTwo
     (N := Multiplicative D) (Q := K) kDAction K_no_nontrivial_torsion
   intro d

LeanPool/InfiniteConnesRigidity/GroupConstruction.lean

@@ -6263,7 +6263,7 @@ private theorem shalom_normalizedFixedVector_of_relativePair
         ((‖p‖ : ℂ)⁻¹) • (p : W)‖ < _
     rw [map_smul, ← smul_sub, norm_smul, norm_inv,
       Complex.norm_real, Real.norm_of_nonneg (norm_nonneg p)]
-    simpa only [← Submodule.norm_coe, div_eq_mul_inv, mul_comm] using hfrac
+    simpa only [← Submodule.norm_coe, div_eq_inv_mul] using hfrac
 
 /-- Cross-module support for the infinite Connes-rigidity construction. -/
 private theorem shalom_normalizedConstantFixedVector_of_integerPair
@@ -7533,15 +7533,12 @@ private theorem upperUnitriangular_factorization (g : Q)
   apply Matrix.SpecialLinearGroup.ext
   intro i j
   fin_cases i <;> fin_cases j <;>
-    simp only [Nat.reduceAdd, Fin.zero_eta, Fin.isValue, Fin.mk_one,
-      Fin.reduceFinMk, Matrix.SpecialLinearGroup.coe_mul,
-      Matrix.SpecialLinearGroup.transvection_coe, Matrix.mul_apply,
-      Matrix.add_apply, Matrix.one_apply, Fin.reduceEq, false_and,
-      not_false_eq_true, Matrix.single_apply_of_ne, add_zero,
-      Matrix.single_apply, ite_mul, one_mul, zero_mul, Finset.sum_ite_eq,
-      Finset.mem_univ, ↓reduceIte, one_ne_zero, true_and,
-      Fin.sum_univ_four, zero_ne_one, mul_ite, mul_one, mul_zero,
-      ite_self, zero_add, and_false, Finset.sum_ite_eq', and_true,
+    simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk,
+      ConnesRigidity.MennickeIdentity.specialLinear_mul_transvection_apply, Fin.reduceEq,
+      ↓reduceIte,
+      Matrix.SpecialLinearGroup.transvection_coe, Matrix.add_apply, Matrix.one_apply,
+      Matrix.single_apply, one_ne_zero, zero_ne_one, and_self, and_false, and_true,
+      mul_one, mul_zero, add_zero, zero_add,
       h00, h11, h22, h33, h10, h20, h21, h30, h31, h32]
 
 /-- Cross-module support for the infinite Connes-rigidity construction. -/