chore: bump mathlib (#354)

* bump mathlib

* Update FLT/AutomorphicRepresentation/Example.lean

Co-authored-by: Ruben Van de Velde <[email protected]>

---------

Co-authored-by: Ruben Van de Velde <[email protected]>

Author: kbuzzard

FLT.lean

@@ -27,7 +27,6 @@ import FLT.Mathlib.Algebra.Algebra.Hom
 import FLT.Mathlib.Algebra.Algebra.Pi
 import FLT.Mathlib.Algebra.Algebra.Tower
 import FLT.Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
 import FLT.Mathlib.Algebra.Order.Hom.Monoid

FLT/AutomorphicRepresentation/Example.lean

@@ -650,7 +650,7 @@ lemma preserves_zsmul {G H : Type*} [Zero G] [Add G] [Neg G] [SMul ℕ G] [SubNe
     (neg : ∀ x, f (-x) = - f x)
     (z : ℤ) (g : G) :
     f (zsmulRec (· • ·) z g) = z • f g := by
-  induction z with
+  cases z with
   | ofNat n =>
     rw [zsmulRec, nsmul, Int.ofNat_eq_coe, natCast_zsmul]
   | negSucc n =>

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -141,9 +141,9 @@ lemma intValuation_comap (hAB : Function.Injective (algebraMap A B))
 omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
     [Module.Finite A B] in
 lemma valuation_comap (w : HeightOneSpectrum B) (x : K) :
-    (comap A w).valuation x ^
+    (comap A w).valuation K x ^
     (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) =
-    w.valuation (algebraMap K L x) := by
+    w.valuation L (algebraMap K L x) := by
   obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) x
   simp [valuation, ← IsScalarTower.algebraMap_apply A K L, IsScalarTower.algebraMap_apply A B L,
     ← intValuation_comap A B (algebraMap_injective_of_field_isFractionRing A B K L), div_pow]
@@ -177,7 +177,7 @@ lemma _root_.IsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMap
   refine ⟨a / m, fun x hx ↦ ?_⟩
   simp_rw [← valuation_comap A]
   calc
-    (comap A w).valuation x ^ m < e (a / ↑m) ^ m := by gcongr; exacts [zero_le', hx]
+    (comap A w).valuation K x ^ m < e (a / ↑m) ^ m := by gcongr; exacts [zero_le', hx]
   _ = e (m • (a / ↑m)) := by
     dsimp [e]
     norm_cast

FLT/HaarMeasure/DistribHaarChar/RealComplex.lean

@@ -62,7 +62,7 @@ lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)
     (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ) _ _ using 2
   · simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def, eq_comm]
       using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)
-  · simp [key, ofReal_norm_eq_enorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]; rfl
+  · simp [key, ofReal_norm_eq_enorm, ENNReal.ofReal_pow, zpow_ofNat]; rfl
   · simp [key, zpow_ofNat]
 
 lemma Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by

FLT/Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -1,7 +1,6 @@
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Group.Pointwise
 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
-import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 

FLT/Mathlib/MeasureTheory/Group/Action.lean

@@ -6,9 +6,3 @@ theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpa
     @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ :=
   le_inf (inf_le_left.trans  <| induced_mono hσ)
          (inf_le_right.trans  <| induced_mono hτ)
-
-theorem DenseRange.piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)]
-    {f : (i : ι) → (X i) → (Y i)} (hf : ∀ i, DenseRange (f i)):
-    DenseRange (Pi.map f) := by
-  rw [DenseRange, Set.range_piMap]
-  exact dense_pi Set.univ (fun i _ => hf i)

FLT/Mathlib/Topology/Constructions.lean

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2836c275479466837c2593377bb54ae9fafc41d2",
+   "rev": "6d33eaf659620a8f914d9c9489dad0d27be88610",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",