merge master

Author: kim-em

Mathlib.lean

@@ -1547,6 +1547,7 @@ public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
 public import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
 public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
 public import Mathlib.Analysis.Calculus.ContDiff.Operations
+public import Mathlib.Analysis.Calculus.ContDiff.Polynomial
 public import Mathlib.Analysis.Calculus.ContDiff.RCLike
 public import Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
 public import Mathlib.Analysis.Calculus.ContDiff.WithLp
@@ -1763,6 +1764,7 @@ public import Mathlib.Analysis.Convolution
 public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
 public import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
 public import Mathlib.Analysis.Distribution.DerivNotation
+public import Mathlib.Analysis.Distribution.Distribution
 public import Mathlib.Analysis.Distribution.FourierSchwartz
 public import Mathlib.Analysis.Distribution.SchwartzSpace
 public import Mathlib.Analysis.Distribution.TemperateGrowth
@@ -2071,6 +2073,7 @@ public import Mathlib.Analysis.Real.Pi.Leibniz
 public import Mathlib.Analysis.Real.Pi.Wallis
 public import Mathlib.Analysis.Real.Spectrum
 public import Mathlib.Analysis.Seminorm
+public import Mathlib.Analysis.SpecialFunctions.Arcosh
 public import Mathlib.Analysis.SpecialFunctions.Arsinh
 public import Mathlib.Analysis.SpecialFunctions.Bernstein
 public import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
@@ -6257,6 +6260,7 @@ public import Mathlib.RingTheory.Smooth.Flat
 public import Mathlib.RingTheory.Smooth.Kaehler
 public import Mathlib.RingTheory.Smooth.Local
 public import Mathlib.RingTheory.Smooth.Locus
+public import Mathlib.RingTheory.Smooth.NoetherianDescent
 public import Mathlib.RingTheory.Smooth.Pi
 public import Mathlib.RingTheory.Smooth.StandardSmooth
 public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -305,3 +305,7 @@ lemma comp_mul' (f : A →ₐ B) : f.toLinearMap ∘ₗ μ = μ[R] ∘ₗ (f.toL
   TensorProduct.ext' <| by simp
 
 end AlgHom
+
+lemma LinearMap.toSpanSingleton_one_eq_algebraLinearMap [CommSemiring R] [Semiring A]
+    [Algebra R A] : toSpanSingleton R A 1 = Algebra.linearMap R A := by
+  ext; simp

Mathlib/Algebra/BigOperators/Fin.lean

@@ -168,6 +168,27 @@ theorem prod_trunc {a b : ℕ} (f : Fin (a + b) → M) (hf : ∀ j : Fin b, f (n
     (∏ i : Fin (a + b), f i) = ∏ i : Fin a, f (castAdd b i) := by
   rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
 
+@[to_additive]
+private lemma prod_insertNth_go :
+    ∀ n i (h : i < n + 1) x (p : Fin n → M), ∏ j, insertNth ⟨i, h⟩ x p j = x * ∏ j, p j
+  | n, 0, h, x, p => by simp
+  | 0, i, h, x, p => by simp [fin_one_eq_zero ⟨i, h⟩]
+  | n + 1, i + 1, h, x, p => by
+    obtain ⟨hd, tl, rfl⟩ := exists_cons p
+    have i_lt := Nat.lt_of_succ_lt_succ h
+    let i_fin : Fin (n + 1) := ⟨i, i_lt⟩
+    rw [show ⟨i + 1, h⟩ = i_fin.succ from rfl]
+    simp only [insertNth_succ_cons, prod_cons]
+    rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]
+
+@[to_additive (attr := simp)]
+theorem prod_insertNth i x (p : Fin n → M) : ∏ j, insertNth i x p j = x * ∏ j, p j :=
+  prod_insertNth_go n i.val i.isLt x p
+
+@[to_additive (attr := simp)]
+theorem mul_prod_removeNth i (f : Fin (n + 1) → M) : f i * ∏ j, removeNth i f j = ∏ j, f j := by
+  rw [← prod_insertNth, insertNth_self_removeNth]
+
 /-!
 ### Products over intervals: `Fin.cast`
 -/

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -198,11 +198,37 @@ lemma prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' 
     l.prod = a ^ l.count a :=
   _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)
 
+@[to_additive (attr := simp)]
+theorem prod_insertIdx {i} (hlen : i ≤ l.length) (hcomm : ∀ a' ∈ l.take i, Commute a a') :
+    (l.insertIdx i a).prod = a * l.prod := by
+  induction i generalizing l
+  case zero => rfl
+  case succ i ih =>
+    obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)
+    simp only [insertIdx_succ_cons, prod_cons,
+      ih (Nat.le_of_lt_succ hlen) (fun a' a'_mem => hcomm a' (mem_of_mem_tail a'_mem))]
+    exact Commute.left_comm (hcomm hd (mem_of_mem_head? rfl)).symm tl.prod
+
+@[to_additive (attr := simp)]
+theorem mul_prod_eraseIdx {i} (hlen : i < l.length) (hcomm : ∀ a' ∈ l.take i, Commute l[i] a') :
+    l[i] * (l.eraseIdx i).prod = l.prod := by
+  rw [← prod_insertIdx (by grind : i ≤ (l.eraseIdx i).length) (fun a' a'_mem =>
+      hcomm a' (by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem)),
+    insertIdx_eraseIdx_getElem hlen]
+
 end Monoid
 
 section CommMonoid
 variable [CommMonoid M] {a : M} {l l₁ l₂ : List M}
 
+@[to_additive (attr := simp)]
+theorem CommMonoid.prod_insertIdx {i} (h : i ≤ l.length) : (l.insertIdx i a).prod = a * l.prod :=
+  List.prod_insertIdx h (fun a' _ ↦ Commute.all a a')
+
+@[to_additive (attr := simp)]
+theorem CommMonoid.mul_prod_eraseIdx {i} (h : i < l.length) : l[i] * (l.eraseIdx i).prod = l.prod :=
+  List.mul_prod_eraseIdx h (fun a' _ ↦ Commute.all l[i] a')
+
 @[to_additive (attr := simp)]
 lemma prod_erase [DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod :=
   prod_erase_of_comm ha fun x _ y _ ↦ mul_comm x y

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -487,11 +487,8 @@ def HomEquiv.fromRestriction {X : ModuleCat R} {Y : ModuleCat S}
       { toFun := fun s : S => g <| (s • y : Y)
         map_add' := fun s1 s2 : S => by simp only [add_smul]; rw [map_add]
         map_smul' := fun r (s : S) => by
-          -- Porting note: dsimp clears out some rw's but less eager to apply others with Lean 4
-          dsimp
-          rw [← g.hom.map_smul]
-          erw [smul_eq_mul, mul_smul]
-          rfl }
+          rw [ModuleCat.restrictScalars.smul_def _ (M := ModuleCat.of _ _) _ _, ← g.hom.map_smul]
+          simp [mul_smul] }
     map_add' := fun y1 y2 : Y =>
       LinearMap.ext fun s : S => by
         simp [smul_add, map_add]

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -132,22 +132,16 @@ theorem leftUnitor_naturality {M N : SemimoduleCat R} (f : M ⟶ N) :
   ext : 1
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
   apply TensorProduct.ext
-  ext x
-  dsimp
-  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
-  rw [map_smul]
-  rfl
+  ext
+  simp [tensorHom, tensorObj, leftUnitor]
 
 theorem rightUnitor_naturality {M N : SemimoduleCat R} (f : M ⟶ N) :
     tensorHom f (𝟙 (SemimoduleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
   ext : 1
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
   apply TensorProduct.ext
-  ext x
-  dsimp
-  erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
-  rw [map_smul]
-  rfl
+  ext
+  simp [tensorHom, tensorObj, rightUnitor]
 
 theorem triangle (M N : SemimoduleCat.{u} R) :
     (associator M (SemimoduleCat.of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom =

Mathlib/Algebra/DirectSum/Module.lean

@@ -429,30 +429,8 @@ noncomputable def IsInternal.collectedBasis (h : IsInternal A) {α : ι → Type
 @[simp]
 theorem IsInternal.collectedBasis_coe (h : IsInternal A) {α : ι → Type*}
     (v : ∀ i, Basis (α i) R (A i)) : ⇑(h.collectedBasis v) = fun a : Σ i, α i ↦ ↑(v a.1 a.2) := by
-  funext a
-  -- Porting note: was
-  -- simp only [IsInternal.collectedBasis, toModule, coeLinearMap, Basis.coe_ofRepr,
-  --   Basis.repr_symm_apply, DFinsupp.lsum_apply_apply, DFinsupp.mapRange.linearEquiv_apply,
-  --   DFinsupp.mapRange.linearEquiv_symm, DFinsupp.mapRange_single, linearCombination_single,
-  --   LinearEquiv.ofBijective_apply, LinearEquiv.symm_symm, LinearEquiv.symm_trans_apply, one_smul,
-  --   sigmaFinsuppAddEquivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
-  --   sigmaFinsuppLequivDFinsupp_apply]
-  -- convert DFinsupp.sumAddHom_single (fun i ↦ (A i).subtype.toAddMonoidHom) a.1 (v a.1 a.2)
-  simp only [IsInternal.collectedBasis, coeLinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm,
-    LinearEquiv.symm_symm, LinearEquiv.trans_apply, sigmaFinsuppLequivDFinsupp_apply,
-    AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
-    sigmaFinsuppAddEquivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
-    LinearEquiv.ofBijective_apply]
-  rw [DFinsupp.mapRange.linearEquiv_symm]
-  -- `DFunLike.coe (β := fun x ↦ ⨁ (i : ι), ↥(A i))`
-  -- appears in the goal, but the lemma is expecting
-  -- `DFunLike.coe (β := fun x ↦ Π₀ (i : ι), ↥(A i))`
-  erw [DFinsupp.mapRange.linearEquiv_apply]
-  simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, linearCombination_single, one_smul,
-    toModule]
-  -- Similarly here.
-  erw [DFinsupp.lsum_single]
-  simp only [Submodule.coe_subtype]
+  simp [IsInternal.collectedBasis, coeLinearMap, DFinsupp.mapRange.linearEquiv,
+    toModule, DFinsupp.lsum]
 
 theorem IsInternal.collectedBasis_mem (h : IsInternal A) {α : ι → Type*}
     (v : ∀ i, Basis (α i) R (A i)) (a : Σ i, α i) : h.collectedBasis v a ∈ A a.1 := by simp

Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

@@ -74,8 +74,8 @@ noncomputable def coneOfHasLimitEval : Cone F where
       naturality := fun i j φ => by
         ext n
         dsimp
-        erw [limit.w]
-        rw [id_comp] }
+        simp only [Category.id_comp]
+        rw [← eval_map, ← Functor.comp_map, limit.w] }
 
 /-- The cone `coneOfHasLimitEval F` is limit. -/
 noncomputable def isLimitConeOfHasLimitEval : IsLimit (coneOfHasLimitEval F) :=
@@ -151,8 +151,8 @@ noncomputable def coconeOfHasColimitEval : Cocone F where
       naturality := fun i j φ => by
         ext n
         dsimp
-        erw [colimit.w (F ⋙ eval C c n) φ]
-        rw [comp_id] }
+        simp only [Category.comp_id]
+        rw [← eval_map, ← Functor.comp_map, colimit.w] }
 
 /-- The cocone `coconeOfHasLimitEval F` is colimit. -/
 noncomputable def isColimitCoconeOfHasColimitEval : IsColimit (coconeOfHasColimitEval F) :=

Mathlib/Algebra/Module/CharacterModule.lean

@@ -200,7 +200,7 @@ lemma eq_zero_of_ofSpanSingleton_apply_self (a : A)
     (h : ofSpanSingleton a ⟨a, Submodule.mem_span_singleton_self a⟩ = 0) : a = 0 := by
   erw [ofSpanSingleton, LinearMap.toAddMonoidHom_coe, LinearMap.comp_apply,
      intSpanEquivQuotAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
-    AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_one,
+    AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_apply_one,
     AddCircle.coe_eq_zero_iff] at h
   rcases h with ⟨n, hn⟩
   apply_fun Rat.den at hn

Mathlib/Algebra/Module/PID.lean

@@ -214,7 +214,7 @@ theorem torsion_by_prime_power_decomposition (hM : Module.IsTorsion' M (Submonoi
           ext i : 3
           simp only [LinearMap.coe_comp, Function.comp_apply, mkQ_apply]
           rw [LinearEquiv.coe_toLinearMap, LinearMap.id_apply, DirectSum.toModule_lof,
-            liftQSpanSingleton_apply, LinearMap.toSpanSingleton_one, Ideal.Quotient.mk_eq_mk,
+            liftQSpanSingleton_apply, LinearMap.toSpanSingleton_apply_one, Ideal.Quotient.mk_eq_mk,
             map_one (Ideal.Quotient.mk _), (this i).choose_spec.right]
     · exact (mk_surjective _).forall.mpr fun x =>
         ⟨(@hM x).choose, by rw [← Quotient.mk_smul, (@hM x).choose_spec, Quotient.mk_zero]⟩