bump mathlib (#302)

* bump mathlib * remove some heavy imports
ImperialCollegeLondon · Jan 4, 2025 · b4c4cec · b4c4cec
1 parent ee88c84
commit b4c4cec
Show file tree

Hide file tree

Showing 9 changed files with 10 additions and 87 deletions.
diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean
@@ -1,8 +1,8 @@
 import Mathlib.Data.PNat.Basic
 import Mathlib.NumberTheory.FLT.Four
 import Mathlib.NumberTheory.FLT.Three
-import Mathlib.Tactic
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
+import Mathlib.Tactic.ModCases
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.RingTheory.SimpleModule
 import FLT.EllipticCurve.Torsion

diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -12,21 +12,26 @@ import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
-import FLT.HIMExperiments.flatness
 import FLT.HaarMeasure.DistribHaarChar.Basic
 import FLT.HaarMeasure.DistribHaarChar.Padic
 import FLT.HaarMeasure.DistribHaarChar.RealComplex
 import FLT.HaarMeasure.DomMulActMeasure
 import FLT.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
+import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
 import FLT.Mathlib.Algebra.BigOperators.Finprod
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
-import FLT.Mathlib.Algebra.Module.Equiv.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
 import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 import FLT.Mathlib.LinearAlgebra.Determinant
@@ -36,17 +41,10 @@ import FLT.Mathlib.NumberTheory.NumberField.Completion
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
 import FLT.Mathlib.RepresentationTheory.Basic
 import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
-import FLT.Mathlib.Topology.Algebra.Module.Equiv
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Topology.Algebra.Monoid
 import FLT.Mathlib.Topology.Constructions
 import FLT.Mathlib.Topology.Homeomorph
-import FLT.MathlibExperiments.Coalgebra.Monoid
-import FLT.MathlibExperiments.Coalgebra.Sweedler
-import FLT.MathlibExperiments.Coalgebra.TensorProduct
-import FLT.MathlibExperiments.HopfAlgebra.Basic
-import FLT.MathlibExperiments.IsCentralSimple
-import FLT.MathlibExperiments.IsFrobenius
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal

diff --git a/FLT/GaloisRepresentation/HardlyRamified.lean b/FLT/GaloisRepresentation/HardlyRamified.lean
@@ -1,5 +1,3 @@
-import Mathlib.Tactic
-
 /-
 Taylor: You could say that
 a representation

diff --git a/FLT/Mathlib/Algebra/Module/Equiv/Defs.lean b/FLT/Mathlib/Algebra/Module/Equiv/Defs.lean
diff --git a/FLT/Mathlib/Topology/Algebra/Module/Equiv.lean b/FLT/Mathlib/Topology/Algebra/Module/Equiv.lean
diff --git a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
@@ -2,7 +2,6 @@ import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
-import FLT.Mathlib.Topology.Algebra.Module.Equiv
 import FLT.Mathlib.Topology.Algebra.Monoid
 
 /-!

diff --git a/FLT/Mathlib/Topology/Homeomorph.lean b/FLT/Mathlib/Topology/Homeomorph.lean
@@ -1,7 +1,7 @@
 import Mathlib.Topology.Homeomorph
 
 -- elsewhere
-theorem _root_.Homeomorph.coinducing {A B : Type*} [τA : TopologicalSpace A]
+theorem Homeomorph.coinducing {A B : Type*} [τA : TopologicalSpace A]
     [τB : TopologicalSpace B] (e : A ≃ₜ B) : τB = τA.coinduced e := by
   ext U
   nth_rw 2 [isOpen_coinduced]
@@ -10,19 +10,3 @@ theorem _root_.Homeomorph.coinducing {A B : Type*} [τA : TopologicalSpace A]
 theorem Homeomorph.symm_apply_eq {M N : Type*} [TopologicalSpace M]
     [TopologicalSpace N] (e : M ≃ₜ N) {x : N} {y : M} :
   e.symm x = y ↔ x = e y := Equiv.symm_apply_eq _
-
-def Homeomorph.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
-    [∀ st, TopologicalSpace (A st)] :
-    (∀ (st : S ⊕ T), A st) ≃ₜ (∀ (s : S), A (.inl s)) × (∀ (t : T), A (.inr t)) where
-  __ := Equiv.sumPiEquivProdPi _
-  continuous_toFun := Continuous.prod_mk (by fun_prop) (by fun_prop)
-  continuous_invFun := continuous_pi <| by rintro (s | t) <;> simp <;> fun_prop
-
-def Homeomorph.pUnitPiEquiv (f : PUnit → Type*) [∀ x, TopologicalSpace (f x)] :
-    (∀ t, f t) ≃ₜ f () where
-  toFun a := a ()
-  invFun a _t := a
-  left_inv x := rfl
-  right_inv x := rfl
-  continuous_toFun := by simp; fun_prop
-  continuous_invFun := by simp; fun_prop
diff --git a/FLT/MathlibExperiments/IsFrobenius.lean b/FLT/MathlibExperiments/IsFrobenius.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Ivan Farabella. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ivan Farabella, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 -/
-import Mathlib.Tactic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ec3b0067299cb6178b8ef0e3a134e76646f4a909",
+   "rev": "e4220ebf1cdae020e7e79ba5a35d26e163bac828",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,