Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4 into nightly-testing

Author: kim-em

Mathlib.lean

@@ -4703,6 +4703,7 @@ import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.RepresentationTheory.Submodule
+import Mathlib.RepresentationTheory.Tannaka
 import Mathlib.RingTheory.AdicCompletion.Algebra
 import Mathlib.RingTheory.AdicCompletion.AsTensorProduct
 import Mathlib.RingTheory.AdicCompletion.Basic

Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

@@ -34,11 +34,14 @@ namespace Set
 
 /-! ### Translation/scaling of sets -/
 
-@[to_additive]
+@[to_additive vadd_set_prod]
 lemma smul_set_prod {M α : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) :
     c • (s ×ˢ t) = (c • s) ×ˢ (c • t) :=
   prodMap_image_prod (c • ·) (c • ·) s t
 
+@[deprecated (since := "2025-03-11")]
+alias vadd_set_sum := vadd_set_prod
+
 @[to_additive]
 lemma smul_set_pi {G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)]
     (c : G) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi fun i ↦ c • s i :=

Mathlib/Algebra/Group/Graph.lean

@@ -53,9 +53,12 @@ attribute [to_additive existing] coe_mgraph
 @[to_additive (attr := simp)]
 lemma mem_mgraph {f : G →* H} {x : G × H} : x ∈ f.mgraph ↔ f x.1 = x.2 := .rfl
 
-@[to_additive]
+@[to_additive mgraph_eq_mrange_prod]
 lemma mgraph_eq_mrange_prod (f : G →* H) : f.mgraph = mrange ((id _).prod f) := by aesop
 
+@[deprecated (since := "2025-03-11")]
+alias _root_.AddMonoidHom.mgraph_eq_mrange_sum := AddMonoidHom.mgraph_eq_mrange_prod
+
 /-- **Vertical line test** for monoid homomorphisms.
 
 Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
@@ -165,9 +168,12 @@ attribute [to_additive existing] coe_graph graph_toSubmonoid
 @[to_additive]
 lemma mem_graph {f : G →* H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2 := .rfl
 
-@[to_additive]
+@[to_additive graph_eq_range_prod]
 lemma graph_eq_range_prod (f : G →* H) : f.graph = range ((id _).prod f) := by aesop
 
+@[deprecated (since := "2025-03-11")]
+alias AddMonoidHom.graph_eq_range_sum := graph_eq_range_prod
+
 /-- **Vertical line test** for group homomorphisms.
 
 Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -121,10 +121,13 @@ theorem top_prod (H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidH
 theorem top_prod_top : (⊤ : Subgroup G).prod (⊤ : Subgroup N) = ⊤ :=
   (top_prod _).trans <| comap_top _
 
-@[to_additive]
+@[to_additive (attr := simp) bot_prod_bot]
 theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
   SetLike.coe_injective <| by simp [coe_prod]
 
+@[deprecated (since := "2025-03-11")]
+alias _root_.AddSubgroup.bot_sum_bot := AddSubgroup.bot_prod_bot
+
 @[to_additive le_prod_iff]
 theorem le_prod_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
     J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K := by
@@ -555,17 +558,23 @@ section Ker
 
 variable {M : Type*} [MulOneClass M]
 
-@[to_additive]
+@[to_additive prodMap_comap_prod]
 theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N)
     (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') :
     (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
   SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
 
-@[to_additive]
+@[deprecated (since := "2025-03-11")]
+alias _root_.AddMonoidHom.sumMap_comap_sum := AddMonoidHom.prodMap_comap_prod
+
+@[to_additive ker_prodMap]
 theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
     (prodMap f g).ker = f.ker.prod g.ker := by
   rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
 
+@[deprecated (since := "2025-03-11")]
+alias _root_.AddMonoidHom.ker_sumMap := AddMonoidHom.ker_prodMap
+
 @[to_additive (attr := simp)]
 lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
 

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -298,11 +298,14 @@ theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
 theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
   (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)
 
-@[to_additive]
+@[to_additive ker_prod]
 theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
     (f.prod g).ker = f.ker ⊓ g.ker :=
   SetLike.ext fun _ => Prod.mk_eq_one
 
+@[deprecated (since := "2025-03-11")]
+alias _root_.AddMonoidHom.ker_sum := AddMonoidHom.ker_prod
+
 @[to_additive]
 theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
   ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩

Mathlib/Algebra/Group/Subgroup/Map.lean

@@ -376,7 +376,11 @@ defined by sending subgroups to their inverse images.
 
 See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
 -/
-@[simps]
+@[to_additive (attr := simps)
+"An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
+defined by sending subgroups to their inverse images.
+
+See also `AddEquiv.mapAddSubgroup` which maps subgroups to their forward images."]
 def comapSubgroup (f : G ≃* H) : Subgroup H ≃o Subgroup G where
   toFun := Subgroup.comap f
   invFun := Subgroup.comap f.symm
@@ -386,13 +390,23 @@ def comapSubgroup (f : G ≃* H) : Subgroup H ≃o Subgroup G where
     ⟨fun h => by simpa [Subgroup.comap_comap] using
       Subgroup.comap_mono (f := (f.symm : H →* G)) h, Subgroup.comap_mono⟩
 
+@[to_additive (attr := simp, norm_cast)]
+lemma coe_comapSubgroup (e : G ≃* H) : comapSubgroup e = Subgroup.comap e.toMonoidHom := rfl
+
+@[to_additive (attr := simp)]
+lemma symm_comapSubgroup (e : G ≃* H) : (comapSubgroup e).symm = comapSubgroup e.symm := rfl
+
 /--
 An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
 defined by sending subgroups to their forward images.
 
 See also `MulEquiv.comapSubgroup` which maps subgroups to their inverse images.
 -/
-@[simps]
+@[to_additive (attr := simps)
+"An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
+defined by sending subgroups to their forward images.
+
+See also `AddEquiv.comapAddSubgroup` which maps subgroups to their inverse images."]
 def mapSubgroup {H : Type*} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup H where
   toFun := Subgroup.map f
   invFun := Subgroup.map f.symm
@@ -402,6 +416,12 @@ def mapSubgroup {H : Type*} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup
     ⟨fun h => by simpa [Subgroup.map_map] using
       Subgroup.map_mono (f := (f.symm : H →* G)) h, Subgroup.map_mono⟩
 
+@[to_additive (attr := simp, norm_cast)]
+lemma coe_mapSubgroup (e : G ≃* H) : mapSubgroup e = Subgroup.map e.toMonoidHom := rfl
+
+@[to_additive (attr := simp)]
+lemma symm_mapSubgroup (e : G ≃* H) : (mapSubgroup e).symm = mapSubgroup e.symm := rfl
+
 end MulEquiv
 
 namespace Subgroup
@@ -410,6 +430,10 @@ open MonoidHom
 
 variable {N : Type*} [Group N] (f : G →* N)
 
+@[to_additive (attr := simp, norm_cast)]
+lemma comap_toSubmonoid (e : G ≃* N) (s : Subgroup N) :
+    (s.comap e).toSubmonoid = s.toSubmonoid.comap e.toMonoidHom := rfl
+
 @[to_additive]
 theorem map_comap_le (H : Subgroup N) : map f (comap f H) ≤ H :=
   (gc_map_comap f).l_u_le _

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -451,7 +451,8 @@ open UniqueMul in
     exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩
 
 open ULift in
-@[to_additive] instance [UniqueProds G] [UniqueProds H] : UniqueProds (G × H) := by
+@[to_additive] instance _root_.Prod.instUniqueProds [UniqueProds G] [UniqueProds H] :
+    UniqueProds (G × H) := by
   have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
   · exact of_injective_mulHom (downMulHom H) down_injective ‹_›
   · refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_)
@@ -541,7 +542,8 @@ instance instForall {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, TwoUnique
       · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
 
 open ULift in
-@[to_additive] instance [TwoUniqueProds G] [TwoUniqueProds H] : TwoUniqueProds (G × H) := by
+@[to_additive]instance _root_.Prod.instTwoUniqueProds [TwoUniqueProds G] [TwoUniqueProds H] :
+    TwoUniqueProds (G × H) := by
   have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
   · exact of_injective_mulHom (downMulHom H) down_injective ‹_›
   · refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)

Mathlib/Analysis/Analytic/Basic.lean

@@ -1103,7 +1103,6 @@ theorem HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
     have hAB : ∀ n, ‖A (n + 2)‖ ≤ B n := fun n =>
       calc
         ‖A (n + 2)‖ ≤ ‖p (n + 2)‖ * ↑(n + 2) * ‖y - (x, x)‖ ^ (n + 1) * ‖y.1 - y.2‖ := by
-          -- Porting note: `pi_norm_const` was `pi_norm_const (_ : E)`
           simpa only [Fintype.card_fin, pi_norm_const, Prod.norm_def, Pi.sub_def,
             Prod.fst_sub, Prod.snd_sub, sub_sub_sub_cancel_right] using
             (p <| n + 2).norm_image_sub_le (fun _ => y.1 - x) fun _ => y.2 - x
@@ -1124,7 +1123,7 @@ theorem HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
       simp only [add_mul]
       have : ‖a‖ < 1 := by simp only [Real.norm_eq_abs, abs_of_pos ha.1, ha.2]
       rw [div_eq_mul_inv, div_eq_mul_inv]
-      exact (hasSum_coe_mul_geometric_of_norm_lt_one this).add  -- Porting note: was `convert`!
+      exact (hasSum_coe_mul_geometric_of_norm_lt_one this).add
           ((hasSum_geometric_of_norm_lt_one this).mul_left 2)
     exact hA.norm_le_of_bounded hBL hAB
   suffices L =O[𝓟 (EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))]

Mathlib/Analysis/Analytic/Composition.lean

@@ -612,8 +612,6 @@ theorem compChangeOfVariables_sum {α : Type*} [AddCommMonoid α] (m M N : ℕ)
   -- 1 - show that the image belongs to `compPartialSumTarget m N N`
   · rintro ⟨k, blocks_fun⟩ H
     rw [mem_compPartialSumSource_iff] at H
-    -- Porting note: added
-    simp only at H
     simp only [mem_compPartialSumTarget_iff, Composition.length, Composition.blocks, H.left,
       map_ofFn, length_ofFn, true_and, compChangeOfVariables]
     intro j
@@ -1079,7 +1077,6 @@ theorem sizeUpTo_sizeUpTo_add (a : Composition n) (b : Composition a.length) {i
     sizeUpTo a (sizeUpTo b i + j) =
       sizeUpTo (a.gather b) i +
         sizeUpTo (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) j := by
-  -- Porting note: `induction'` left a spurious `hj` in the context
   induction j with
   | zero =>
     show

Mathlib/Analysis/Analytic/RadiusLiminf.lean

@@ -32,9 +32,8 @@ $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{‖p n‖}}$. The actual statement uses
 coercions. -/
 theorem radius_eq_liminf :
     p.radius = liminf (fun n => (1 / (‖p n‖₊ ^ (1 / (n : ℝ)) : ℝ≥0) : ℝ≥0∞)) atTop := by
-  -- Porting note: added type ascription to make elaborated statement match Lean 3 version
   have :
-    ∀ (r : ℝ≥0) {n : ℕ},
+    ∀ (r : ℝ≥0) {n},
       0 < n → ((r : ℝ≥0∞) ≤ 1 / ↑(‖p n‖₊ ^ (1 / (n : ℝ))) ↔ ‖p n‖₊ * r ^ n ≤ 1) := by
     intro r n hn
     have : 0 < (n : ℝ) := Nat.cast_pos.2 hn

Mathlib/Analysis/Analytic/Uniqueness.lean

@@ -47,9 +47,6 @@ theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p :
   clear h hc z_mem
   rcases n with - | n
   · exact norm_eq_zero.mp (by
-      -- Porting note: the symmetric difference of the `simpa only` sets:
-      -- added `zero_add, pow_one`
-      -- removed `zero_pow, Ne.def, Nat.one_ne_zero, not_false_iff`
       simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_add, pow_one,
         mul_zero, norm_le_zero_iff] using ht 0 (δε (Metric.mem_ball_self δ_pos)))
   · refine Or.elim (Classical.em (y = 0))
@@ -70,9 +67,7 @@ theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p :
           simpa only [norm_pow, _root_.norm_norm] using ht (k • y) (δε (mem_ball_zero_iff.mpr h₁))
           --simpa only [norm_pow, norm_norm] using ht (k • y) (δε (mem_ball_zero_iff.mpr h₁))
         _ = ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) := by
-          -- Porting note: added `Nat.succ_eq_add_one` since otherwise `ring` does not conclude.
-          simp only [norm_smul, mul_pow, Nat.succ_eq_add_one]
-          -- Porting note: removed `rw [pow_succ]`, since it now becomes superfluous.
+          simp only [norm_smul, mul_pow]
           ring
     have h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε :=
       inv_mul_cancel_right₀ h₀.ne.symm ε ▸

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -220,7 +220,6 @@ theorem IsEquivalent.smul {α E 𝕜 : Type*} [NormedField 𝕜] [NormedAddCommG
     (fun x ↦ a x • u x) ~[l] fun x ↦ b x • v x := by
   rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩
   have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
-    -- Porting note: `convert` has become too strong, so we need to specify `using 1`.
     convert (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).sub
       (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
     ext

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -813,7 +813,6 @@ theorem HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann =
       exact fun J hJ => (Finset.mem_filter.1 hJ).2
   /- Now we deal with boxes such that `π.tag J ∉ s`.
     In this case the estimate is straightforward. -/
-  -- Porting note: avoided strange elaboration issues by rewriting using `calc`
   calc
     dist (∑ J ∈ π.boxes with ¬tag π J ∈ s, vol J (f (tag π J)))
       (∑ J ∈ π.boxes with ¬tag π J ∈ s, g J)

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -93,7 +93,6 @@ theorem lower_ne_upper (i) : I.lower i ≠ I.upper i :=
 instance : Membership (ι → ℝ) (Box ι) :=
   ⟨fun I x ↦ ∀ i, x i ∈ Ioc (I.lower i) (I.upper i)⟩
 
--- Porting note: added
 /-- The set of points in this box: this is the product of half-open intervals `(lower i, upper i]`,
 where `lower` and `upper` are this box' corners. -/
 @[coe]
@@ -238,7 +237,6 @@ instance : SemilatticeSup (Box ι) :=
 In this section we define coercion from `WithBot (Box ι)` to `Set (ι → ℝ)` by sending `⊥` to `∅`.
 -/
 
--- Porting note: added
 /-- The set underlying this box: `⊥` is mapped to `∅`. -/
 @[coe]
 def withBotToSet (o : WithBot (Box ι)) : Set (ι → ℝ) := o.elim ∅ (↑)

Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

@@ -105,7 +105,8 @@ namespace Box
 
 variable [Fintype ι]
 
--- @[simp] -- Porting note: simp normal form is `volume_apply'`
+-- This is not a `simp` lemma because the left hand side simplifies already.
+-- See `volume_apply'` for the relevant `simp` lemma.
 theorem volume_apply (I : Box ι) :
     (volume : Measure (ι → ℝ)).toBoxAdditive I = ∏ i, (I.upper i - I.lower i) := by
   rw [Measure.toBoxAdditive_apply, coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]

Mathlib/Analysis/BoxIntegral/Partition/Split.lean

@@ -174,7 +174,6 @@ theorem iUnion_split (I : Box ι) (i : ι) (x : ℝ) : (split I i x).iUnion = I
 theorem isPartitionSplit (I : Box ι) (i : ι) (x : ℝ) : IsPartition (split I i x) :=
   isPartition_iff_iUnion_eq.2 <| iUnion_split I i x
 
--- Porting note: In the type, changed `Option.elim` to `Option.elim'`
 theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x : ℝ) (f : Box ι → M) :
     (∑ J ∈ (split I i x).boxes, f J) =
       (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f := by

Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean

@@ -274,7 +274,6 @@ theorem isHenstock_single_iff (hJ : J ≤ I) (h : x ∈ Box.Icc I) :
     IsHenstock (single I J hJ x h) ↔ x ∈ Box.Icc J :=
   forall_mem_single (fun x J => x ∈ Box.Icc J) hJ h
 
---@[simp] -- Porting note: Commented out, because `simp only [isHenstock_single_iff]` simplifies it
 theorem isHenstock_single (h : x ∈ Box.Icc I) : IsHenstock (single I I le_rfl x h) :=
   (isHenstock_single_iff (le_refl I) h).2 h
 

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -596,8 +596,9 @@ instance instNormedSpace : NormedSpace ℂ (CStarMatrix m n A) :=
 
 noncomputable instance instNonUnitalNormedRing :
     NonUnitalNormedRing (CStarMatrix n n A) where
-  dist_eq _ _ := rfl
-  norm_mul _ _ := by simpa only [norm_def', map_mul] using norm_mul_le _ _
+  __ : NormedAddCommGroup (CStarMatrix n n A) := inferInstance
+  __ : NonUnitalRing (CStarMatrix n n A) := inferInstance
+  norm_mul_le _ _ := by simpa only [norm_def', map_mul] using norm_mul_le _ _
 
 open ContinuousLinearMap CStarModule in
 /-- Matrices with entries in a C⋆-algebra form a C⋆-algebra. -/
@@ -649,7 +650,7 @@ variable {n : Type*} [Fintype n] [DecidableEq n]
 
 noncomputable instance instNormedRing : NormedRing (CStarMatrix n n A) where
   dist_eq _ _ := rfl
-  norm_mul := norm_mul_le
+  norm_mul_le := norm_mul_le
 
 noncomputable instance instNormedAlgebra : NormedAlgebra ℂ (CStarMatrix n n A) where
   norm_smul_le r M := by simpa only [norm_def, map_smul] using (toCLM M).opNorm_smul_le r

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -225,7 +225,7 @@ scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedSpace
 identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
 def instL2OpNormedRing : NormedRing (Matrix n n 𝕜) where
   dist_eq := l2OpNormedRingAux.dist_eq
-  norm_mul := l2OpNormedRingAux.norm_mul
+  norm_mul_le := l2OpNormedRingAux.norm_mul_le
 
 scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedRing
 

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -73,7 +73,6 @@ scoped[MultiplierAlgebra] notation "𝓜(" 𝕜 ", " A ")" => DoubleCentralizer
 
 open MultiplierAlgebra
 
--- Porting note: `ext` was generating the wrong extensionality lemma; it deconstructed the `×`.
 @[ext]
 lemma DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜]
     [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A]
@@ -430,7 +429,6 @@ maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a`
 Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the
 `algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See
 `DoubleCentralizer.coe_eq_algebraMap` below. -/
--- Porting note: added `noncomputable`; IR check does not recognise `ContinuousLinearMap.mul`
 @[coe]
 protected noncomputable def coe (a : A) : 𝓜(𝕜, A) :=
   { fst := ContinuousLinearMap.mul 𝕜 A a

Mathlib/Analysis/CStarAlgebra/lpSpace.lean

@@ -27,7 +27,7 @@ instance [∀ i, NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra (l
 -- aside from `∀ i, NormOneClass (A i)`, this holds automatically for C⋆-algebras though.
 instance [∀ i, Nontrivial (A i)] [∀ i, CStarAlgebra (A i)] : NormedRing (lp A ∞) where
   dist_eq := dist_eq_norm
-  norm_mul := norm_mul_le
+  norm_mul_le := norm_mul_le
 
 instance [∀ i, Nontrivial (A i)] [∀ i, CommCStarAlgebra (A i)] : CommCStarAlgebra (lp A ∞) where
   mul_comm := mul_comm

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -142,10 +142,8 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       refine le_trans ?_ (le_max_left _ _)
       apply Finset.le_max'
       apply Finset.mem_image_of_mem
-      -- Porting note: was
-      -- simp only [Finset.mem_range]
-      -- linarith
-      simpa only [Finset.mem_range, Nat.lt_add_one_iff]
+      simp only [Finset.mem_range]
+      omega
     refine ⟨M⁻¹ * δ n, by positivity, fun i hi x => ?_⟩
     calc
       ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by

Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean

@@ -23,7 +23,6 @@ open scoped Topology
 
 variable (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
--- Porting note: this definition was hidden inside the next instance.
 /-- A base bump function in an inner product space. This construction works in any space with a
 norm smooth away from zero but we do not have a typeclass for this. -/
 noncomputable def ContDiffBumpBase.ofInnerProductSpace : ContDiffBumpBase E where

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -952,8 +952,6 @@ theorem ContDiffWithinAt.clm_apply {f : E → F →L[𝕜] G} {g : E → F}
     ContDiffWithinAt 𝕜 n (fun x => (f x) (g x)) s x :=
   isBoundedBilinearMap_apply.contDiff.comp₂_contDiffWithinAt hf hg
 
--- Porting note: In Lean 3 we had to give implicit arguments in proofs like the following,
--- to speed up elaboration. In Lean 4 this isn't necessary anymore.
 theorem ContDiff.smulRight {f : E → F →L[𝕜] 𝕜} {g : E → G} (hf : ContDiff 𝕜 n f)
     (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => (f x).smulRight (g x) :=
   isBoundedBilinearMap_smulRight.contDiff.comp₂ (g := fun p => p.1.smulRight p.2) hf hg