chore: get rid of the ForMathlib folder

FLT/FLT_files.lean

@@ -5,22 +5,30 @@ import FLT.Basic.Reductions
 import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
 import FLT.DivisionAlgebra.Finiteness
 import FLT.EllipticCurve.Torsion
-import FLT.ForMathlib.DomMulActMeasure
-import FLT.ForMathlib.MiscLemmas
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
 import FLT.HaarMeasure.DistribHaarChar
+import FLT.HaarMeasure.DomMulActMeasure
 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.Module.Equiv.Defs
+import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
 import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.Mathlib.RingTheory.Norm.Defs
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+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
@@ -30,9 +38,6 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
-import FLT.Mathlib.RingTheory.Norm.Defs
-import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
-import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal

FLT/HaarMeasure/DistribHaarChar.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Andrew Yang, Yaël Dillies, Javier López-Contreras. All righ
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Yaël Dillies, Javier López-Contreras
 -/
+import FLT.HaarMeasure.DomMulActMeasure
 import FLT.Mathlib.Data.ENNReal.Inv
-import FLT.ForMathlib.DomMulActMeasure
 
 /-!
 # The distributive character of Haar measures

FLT/Mathlib/Algebra/BigOperators/Finprod.lean

@@ -0,0 +1,20 @@
+import Mathlib.Algebra.BigOperators.Finprod
+import Mathlib.Algebra.BigOperators.Pi
+
+@[to_additive]
+lemma finprod_option {ι : Type*} {B : Type*} [Finite ι] [CommMonoid B] (φ : Option ι → B) :
+    (∏ᶠ oi, φ oi) = φ none * ∏ᶠ (j : ι),  φ (some j) := by
+  rw [← finprod_mem_univ]
+  convert finprod_mem_insert φ (show none ∉ Set.range Option.some by aesop)
+    (Set.finite_range some)
+  · exact (Set.insert_none_range_some ι).symm
+  · rw [finprod_mem_range]
+    exact Option.some_injective ι
+
+@[to_additive]
+lemma finprod_apply {α ι N : Type*} [CommMonoid N] [Finite ι] (f : ι → α → N) (a : α) :
+    (∏ᶠ i, f i) a = ∏ᶠ i, (f i) a := by
+  classical
+  simp only [finprod_def, dif_pos (Set.toFinite _), Finset.prod_apply]
+  symm
+  apply Finset.prod_subset <;> aesop

FLT/Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -0,0 +1,21 @@
+import Mathlib.Algebra.Module.Equiv.Defs
+import Mathlib.Algebra.Module.Pi
+import Mathlib.Algebra.Module.Prod
+
+variable (R : Type*) [Semiring R] in
+def LinearEquiv.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
+    [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
+    (∀ (st : S ⊕ T), A st) ≃ₗ[R] (∀ (s : S), A (.inl s)) × (∀ (t : T), A (.inr t)) where
+  __ := Equiv.sumPiEquivProdPi _
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+variable (R : Type*) [Semiring R] in
+def LinearEquiv.pUnitPiEquiv (f : PUnit → Type*) [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] :
+    ((t : PUnit) → (f t)) ≃ₗ[R] f () where
+  toFun a := a ()
+  invFun a _t := a
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl

FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -0,0 +1,15 @@
+import Mathlib.Algebra.Module.LinearMap.Defs
+import Mathlib.Data.Fintype.Option
+import FLT.Mathlib.Algebra.BigOperators.Finprod
+
+theorem LinearMap.finsum_apply {R : Type*} [Semiring R] {A B : Type*} [AddCommMonoid A] [Module R A]
+    [AddCommMonoid B] [Module R B] {ι : Type*} [Finite ι] (φ : ∀ _ : ι, A →ₗ[R] B) (a : A) :
+    (∑ᶠ i, φ i) a = ∑ᶠ i, φ i a := by
+  induction ι using Finite.induction_empty_option
+  · case of_equiv X Y e hx =>
+    convert hx (φ ∘ e)
+    · exact (finsum_comp_equiv e).symm
+    · exact (finsum_comp_equiv e).symm
+  · simp [finsum_of_isEmpty]
+  · case h_option X _ hX =>
+    simp [finsum_option, hX]

FLT/Mathlib/Topology/Algebra/Module/Basic.lean

@@ -0,0 +1,30 @@
+import Mathlib.Topology.Algebra.Module.Basic
+import FLT.Mathlib.Algebra.Module.Equiv.Defs
+import FLT.Mathlib.Topology.Homeomorph
+
+def ContinuousLinearEquiv.piCongrLeft (R : Type*) [Semiring R] {ι ι' : Type*}
+    (φ : ι → Type*) [∀ i, AddCommMonoid (φ i)] [∀ i, Module R (φ i)]
+    [∀ i, TopologicalSpace (φ i)]
+    (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i where
+  __ := Homeomorph.piCongrLeft e
+  __ := LinearEquiv.piCongrLeft R φ e
+
+
+section Pi
+
+variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemiring R]
+
+variable {ι : Type*} [Finite ι] {A : ι → Type*} [∀ i, AddCommMonoid (A i)]
+  [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
+def ContinuousLinearEquiv.sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*)
+    (A : S ⊕ T → Type*) [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)]
+    [∀ st, TopologicalSpace (A st)] :
+    ((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t)) where
+  __ := LinearEquiv.sumPiEquivProdPi R S T A
+  __ := Homeomorph.sumPiEquivProdPi S T A
+
+def ContinuousLinearEquiv.pUnitPiEquiv (R : Type*) [Semiring R] (f : PUnit → Type*)
+    [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] [∀ x, TopologicalSpace (f x)] :
+    ((t : PUnit) → f t) ≃L[R] f () where
+  __ := LinearEquiv.pUnitPiEquiv R f
+  __ := Homeomorph.pUnitPiEquiv f