Merge remote-tracking branch 'origin/master' into bump/v4.22.0

Author: mathlib4-bot

Mathlib.lean

@@ -2353,6 +2353,7 @@ import Mathlib.CategoryTheory.Monad.Limits
 import Mathlib.CategoryTheory.Monad.Monadicity
 import Mathlib.CategoryTheory.Monad.Products
 import Mathlib.CategoryTheory.Monad.Types
+import Mathlib.CategoryTheory.Monoidal.Action.Basic
 import Mathlib.CategoryTheory.Monoidal.Bimod
 import Mathlib.CategoryTheory.Monoidal.Bimon_
 import Mathlib.CategoryTheory.Monoidal.Braided.Basic
@@ -5033,11 +5034,17 @@ import Mathlib.RepresentationTheory.Coinduced
 import Mathlib.RepresentationTheory.Coinvariants
 import Mathlib.RepresentationTheory.FDRep
 import Mathlib.RepresentationTheory.FiniteIndex
+import Mathlib.RepresentationTheory.GroupCohomology.Basic
+import Mathlib.RepresentationTheory.GroupCohomology.Functoriality
+import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
+import Mathlib.RepresentationTheory.GroupCohomology.LowDegree
+import Mathlib.RepresentationTheory.GroupCohomology.Resolution
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
 import Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
+import Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
 import Mathlib.RepresentationTheory.Homological.Resolution
 import Mathlib.RepresentationTheory.Induced
 import Mathlib.RepresentationTheory.Invariants

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -6,9 +6,10 @@ Authors: Jujian Zhang
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Limits
-import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Linear.LinearFunctor
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 /-!
 # Change Of Rings

Mathlib/Algebra/Lie/BaseChange.lean

@@ -5,8 +5,6 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Lie.TensorProduct
-import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # Extension and restriction of scalars for Lie algebras and Lie modules
@@ -165,16 +163,14 @@ def baseChange : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
   { (N : Submodule R M).baseChange A with
     lie_mem := by
       intro x m hm
-      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
-        Submodule.mem_toAddSubmonoid] at hm ⊢
+      rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢
+      rw [Submodule.baseChange_eq_span] at hm
       obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
       refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
       · change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
         simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
-        suffices ∀ n : (N : Submodule R M).map (TensorProduct.mk R A M 1),
-            ⁅a ⊗ₜ[R] y, (n : A ⊗[R] M)⁆ ∈ (N : Submodule R M).baseChange A by
-          exact Submodule.sum_mem _ fun n _ ↦ Submodule.smul_mem _ _ (this n)
-        rintro ⟨-, ⟨n : M, hn : n ∈ N, rfl⟩⟩
+        refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
+        rw [Subtype.coe_mk, ← h]
         exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)
       · rw [add_lie]
         exact ((N : Submodule R M).baseChange A).add_mem hy hz }
@@ -193,8 +189,8 @@ lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ N) :
 
 lemma mem_baseChange_iff {m : A ⊗[R] M} :
     m ∈ N.baseChange A ↔
-    m ∈ Submodule.span A ((N : Submodule R M).map (TensorProduct.mk R A M 1)) :=
-  Iff.rfl
+    m ∈ Submodule.span A ((N : Submodule R M).map (TensorProduct.mk R A M 1)) := by
+  rw [← Submodule.baseChange_eq_span]; rfl
 
 @[simp]
 lemma baseChange_bot : (⊥ : LieSubmodule R L M).baseChange A = ⊥ := by
@@ -219,30 +215,11 @@ lemma lie_baseChange {I : LieIdeal R L} {N : LieSubmodule R L M} :
     exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx,
            1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩
   · rintro - ⟨x, hx, m, hm, rfl⟩
-    revert m
-    apply Submodule.span_induction
-      (p := fun x' _ ↦ ∀ m' ∈ N.baseChange A, ⁅x', m'⁆ ∈ Submodule.span A s) (hx := hx)
-    · rintro _ ⟨y : L, hy : y ∈ I, rfl⟩ m hm
-      apply Submodule.span_induction
-        (p := fun m' _ ↦ ⁅(1 : A) ⊗ₜ[R] y, m'⁆ ∈ Submodule.span A s) (hx := hm)
-      · rintro - ⟨m', hm' : m' ∈ N, rfl⟩
-        rw [TensorProduct.mk_apply, LieAlgebra.ExtendScalars.bracket_tmul, mul_one]
-        apply Submodule.subset_span
-        exact ⟨y, hy, m', hm', rfl⟩
-      · simp
-      · intro u v _ _ hu hv
-        rw [lie_add]
-        exact Submodule.add_mem _ hu hv
-      · intro a u _ hu
-        rw [lie_smul]
-        exact Submodule.smul_mem _ a hu
-    · simp
-    · intro x y _ _ hx hy m' hm'
-      rw [add_lie]
-      exact Submodule.add_mem _ (hx _ hm') (hy _ hm')
-    · intro a x _ hx m' hm'
-      rw [smul_lie]
-      exact Submodule.smul_mem _ a (hx _ hm')
+    rw [mem_baseChange_iff] at hx hm
+    refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
+      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm
+    · rintro - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
+    all_goals { intros; simp [add_mem, Submodule.smul_mem, *] }
 
 end LieSubmodule
 

Mathlib/Algebra/Module/PID.lean

@@ -218,7 +218,8 @@ theorem torsion_by_prime_power_decomposition (hM : Module.IsTorsion' M (Submonoi
       rw [Submodule.map_span, Submodule.map_top, range_mkQ] at hs'; simp only [mkQ_apply] at hs'
       simp only [s']; rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove]
       rw [← Set.range_comp, ← Set.insert_image_compl_eq_range _ j, Function.comp_apply,
-        (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _), span_insert_zero] at hs'
+        (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _),
+        Submodule.span_insert_zero] at hs'
       exact hs'
 
 end PTorsion

Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

@@ -101,7 +101,7 @@ theorem finite_integral_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r)
     ext x
     simp only [mem_setOf_eq, mem_closedBall_zero_iff]
     exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
-  rw [setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall h_int)]
+  rw [setLIntegral_congr_fun measurableSet_Ioi h_int]
   set f := fun t : ℝ ↦ μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
   set mB := μ (Metric.ball (0 : E) 1)
   -- the next two inequalities are in fact equalities but we don't need that
@@ -115,15 +115,15 @@ theorem finite_integral_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r)
       refine μ.addHaar_closedBall (0 : E) ?_
       rw [sub_nonneg]
       exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
-    rw [setLIntegral_congr_fun measurableSet_Ioc (ae_of_all _ h_int'),
+    rw [setLIntegral_congr_fun measurableSet_Ioc h_int',
       lintegral_mul_const' _ _ measure_ball_lt_top.ne]
     exact ENNReal.mul_lt_top
       (finite_integral_rpow_sub_one_pow_aux (finrank ℝ E) hnr) measure_ball_lt_top
   · -- The integral from 1 to ∞ is zero:
     have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
       simp only [f, closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
     -- The integral over the constant zero function is finite:
-    rw [setLIntegral_congr_fun measurableSet_Ioi (ae_of_all volume <| h_int''), lintegral_const 0,
+    rw [setLIntegral_congr_fun measurableSet_Ioi h_int'', lintegral_const 0,
       zero_mul]
     exact WithTop.top_pos
 

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -162,8 +162,8 @@ theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ℝ≥0∞) :
       · simp_rw [det_fderivPolarCoordSymm]; rfl
       exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
     _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
-      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet ?_
-      filter_upwards with _ hx using by rw [abs_of_pos hx.1]
+      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
+      rw [abs_of_pos hx.1]
 
 end Real
 
@@ -286,8 +286,7 @@ theorem lintegral_comp_pi_polarCoord_symm (f : (ι → ℝ × ℝ) → ℝ≥0
   convert (lintegral_image_eq_lintegral_abs_det_fderiv_mul volume measurableSet_pi_polarCoord_target
     (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt)
       injOn_pi_polarCoord_symm f).symm using 1
-  refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target ?_
-  filter_upwards with x hx
+  refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)
   simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
     abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]