chore: bump Std, changes for leanprover-community/batteries#366

revert

.

fix a bit

blech

one more

comment out broken and unused results

chore: bump Std

remove redundant simp lemmas

cleanup

fix: make `Nat.testBit_bitwise` a simp-lemma again.

This fixes the Int.testbit_bitwise proofs

fix `castNum_testBit`

fix `testBit_eq_inth`

fixes

golf

golf

Apply suggestions from code review

Co-authored-by: Eric Wieser <[email protected]>

fix whitespace

fix name conflict

more efficient

restore lemma

feat: Mapping extreme points under continuous maps (#8574)

Prove that extreme points are preserved under affine equivalences, and the less trivial statement that a continuous affine map sends extreme points of a compact set to a superset of the extreme
points of the image of that set.

Also fix a few name and tweak the API a bit.

Co-authored-by: Yury G. Kudryashov <[email protected]>

chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613)

We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets.

feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643)

We prove some results about effective epimorphisms which allow us to deduce that a category which is `FinitaryPreExtensive` and `Preregular` is also `Precoherent`.

feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8724)

We had `ball_smul_ball` and `closedBall_smul_closedBall`.
Add versions with mixed `ball` and `closedBall`.
Also move this lemmas below and golf the proofs.

feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)

fix breakage in BitVec lemmas

Mathlib/Algebra/Lie/Killing.lean

@@ -242,7 +242,8 @@ lemma traceForm_eq_sum_weightSpaceOf [IsTriangularizable R L M] (z : L) :
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
   exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
 
--- In characteristic zero a stronger result holds (no `⊓ LieAlgebra.center K L`) TODO prove this!
+-- In characteristic zero (or even just `LinearWeights R L M`) a stronger result holds (no
+-- `⊓ LieAlgebra.center R L`) TODO prove this using `LieModule.traceForm_eq_sum_finrank_nsmul_mul`.
 lemma lowerCentralSeries_one_inf_center_le_ker_traceForm :
     lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L ≤ LinearMap.ker (traceForm R L M) := by
   /- Sketch of proof (due to Zassenhaus):
@@ -490,32 +491,33 @@ lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L]
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
   exact Finset.sum_congr (by simp) (fun χ _ ↦ traceForm_weightSpace_eq K L M χ x y)
 
-@[simp]
-lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot [LieAlgebra.IsNilpotent K L]
-    [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L]
-    (h : LinearMap.ker (traceForm K L M) = ⊥) :
-    span K (range (weight.toLinear K L M)) = ⊤ := by
+-- The reverse inclusion should also hold: TODO prove this!
+lemma LieModule.dualAnnihilator_ker_traceForm_le_span_weight [LieAlgebra.IsNilpotent K L]
+    [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L] :
+    (LinearMap.ker (traceForm K L M)).dualAnnihilator ≤ span K (range (weight.toLinear K L M)) := by
+  intro g hg
+  simp only [Submodule.mem_dualAnnihilator, LinearMap.mem_ker] at hg
   by_contra contra
   obtain ⟨f : Module.Dual K (Module.Dual K L), hf, hf'⟩ :=
-    Module.exists_dual_map_eq_bot_of_lt_top K (lt_top_iff_ne_top.mpr contra) inferInstance
+    Submodule.exists_dual_map_eq_bot_of_nmem contra inferInstance
   let x : L := (Module.evalEquiv K L).symm f
   replace hf' : ∀ χ ∈ weight K L M, χ x = 0 := by
     intro χ hχ
     change weight.toLinear K L M ⟨χ, hχ⟩ x = 0
     rw [Module.apply_evalEquiv_symm_apply, ← Submodule.mem_bot (R := K), ← hf', Submodule.mem_map]
     exact ⟨weight.toLinear K L M ⟨χ, hχ⟩, Submodule.subset_span (mem_range_self _), rfl⟩
-  have hx : x ≠ 0 := (LinearEquiv.map_ne_zero_iff _).mpr hf
-  apply hx
-  rw [← Submodule.mem_bot (R := K), ← h, LinearMap.mem_ker]
+  have hx : g x ≠ 0 := by simpa
+  refine hx (hg _ ?_)
   ext y
   rw [LieModule.traceForm_eq_sum_finrank_nsmul_mul, LinearMap.zero_apply]
   exact Finset.sum_eq_zero fun χ hχ ↦ by simp [hf' χ hχ]
 
 /-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
 Killing form, the corresponding roots span the dual space of `H`. -/
+@[simp]
 lemma LieAlgebra.IsKilling.span_weight_eq_top [FiniteDimensional K L] [IsKilling K L]
     (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L] :
     span K (range (weight.toLinear K H L)) = ⊤ := by
-  simp
+  simpa using LieModule.dualAnnihilator_ker_traceForm_le_span_weight K H L
 
 end Field

Mathlib/Algebra/Module/LinearMap.lean

@@ -62,10 +62,7 @@ open Function
 
 universe u u' v w x y z
 
-variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
-variable {k : Type*} {S : Type*} {S₃ : Type*} {T : Type*}
-variable {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*}
-variable {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {ι : Type*}
+variable {R R₁ R₂ R₃ k S S₃ T M M₁ M₂ M₃ N₁ N₂ N₃ ι : Type*}
 
 /-- A map `f` between modules over a semiring is linear if it satisfies the two properties
 `f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this
@@ -87,7 +84,7 @@ is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
 `M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
 `σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
 maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. -/
-structure LinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*)
+structure LinearMap {R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*)
     (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
     AddHom M M₂ where
   /-- A linear map preserves scalar multiplication.
@@ -150,7 +147,6 @@ namespace SemilinearMapClass
 variable (F : Type*)
 variable [Semiring R] [Semiring S]
 variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
-variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃]
 variable [Module R M] [Module R M₂] [Module S M₃]
 variable {σ : R →+* S}
 
@@ -174,8 +170,23 @@ theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
     c • f x = f (σ' c • x) := by simp
 #align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv
 
+/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
+abbrev semilinearMap : M →ₛₗ[σ] M₃ where
+  toFun := f
+  map_add' := map_add f
+  map_smul' := map_smulₛₗ f
+
 end SemilinearMapClass
 
+namespace LinearMapClass
+variable {F : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
+  (f : F) [LinearMapClass F R M₁ M₂]
+
+/-- Reinterpret an element of a type of linear maps as a linear map. -/
+abbrev linearMap : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f
+
+end LinearMapClass
+
 namespace LinearMap
 
 section AddCommMonoid
@@ -566,7 +577,7 @@ theorem id_comp : id.comp f = f :=
 #align linear_map.id_comp LinearMap.id_comp
 
 theorem comp_assoc
-    {R₄ : Type*} {M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄]
+    {R₄ M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄]
     {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄}
     [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
     (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :

Mathlib/Analysis/Convex/Exposed.lean

@@ -265,7 +265,7 @@ protected theorem isExtreme (hAB : IsExposed 𝕜 A B) : IsExtreme 𝕜 A B := b
 end IsExposed
 
 theorem exposedPoints_subset_extremePoints : A.exposedPoints 𝕜 ⊆ A.extremePoints 𝕜 := fun _ hx =>
-  mem_extremePoints_iff_extreme_singleton.2 (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme
+  (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme.mem_extremePoints
 #align exposed_points_subset_extreme_points exposedPoints_subset_extremePoints
 
 end LinearOrderedRing

Mathlib/Analysis/Convex/Extreme.lean

@@ -123,12 +123,7 @@ theorem isExtreme_biInter {F : Set (Set E)} (hF : F.Nonempty) (hA : ∀ B ∈ F,
 #align is_extreme_bInter isExtreme_biInter
 
 theorem isExtreme_sInter {F : Set (Set E)} (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExtreme 𝕜 A B) :
-    IsExtreme 𝕜 A (⋂₀ F) := by
-  obtain ⟨B, hB⟩ := hF
-  refine' ⟨(sInter_subset_of_mem hB).trans (hAF B hB).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ _⟩
-  simp_rw [mem_sInter] at hxF ⊢
-  have h := fun B hB ↦ (hAF B hB).2 hx₁A hx₂A (hxF B hB) hx
-  exact ⟨fun B hB ↦ (h B hB).1, fun B hB ↦ (h B hB).2⟩
+    IsExtreme 𝕜 A (⋂₀ F) := by simpa [sInter_eq_biInter] using isExtreme_biInter hF hAF
 #align is_extreme_sInter isExtreme_sInter
 
 theorem mem_extremePoints : x ∈ A.extremePoints 𝕜 ↔
@@ -137,13 +132,15 @@ theorem mem_extremePoints : x ∈ A.extremePoints 𝕜 ↔
 #align mem_extreme_points mem_extremePoints
 
 /-- x is an extreme point to A iff {x} is an extreme set of A. -/
-theorem mem_extremePoints_iff_extreme_singleton : x ∈ A.extremePoints 𝕜 ↔ IsExtreme 𝕜 A {x} := by
-  refine' ⟨_, fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩⟩
+@[simp] lemma isExtreme_singleton : IsExtreme 𝕜 A {x} ↔ x ∈ A.extremePoints 𝕜 := by
+  refine ⟨fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩, ?_⟩
   rintro ⟨hxA, hAx⟩
   use singleton_subset_iff.2 hxA
   rintro x₁ hx₁A x₂ hx₂A y (rfl : y = x)
   exact hAx hx₁A hx₂A
-#align mem_extreme_points_iff_extreme_singleton mem_extremePoints_iff_extreme_singleton
+#align mem_extreme_points_iff_extreme_singleton isExtreme_singleton
+
+alias ⟨IsExtreme.mem_extremePoints, _⟩ := isExtreme_singleton
 
 theorem extremePoints_subset : A.extremePoints 𝕜 ⊆ A :=
   fun _ hx ↦ hx.1
@@ -167,8 +164,7 @@ theorem inter_extremePoints_subset_extremePoints_of_subset (hBA : B ⊆ A) :
 
 theorem IsExtreme.extremePoints_subset_extremePoints (hAB : IsExtreme 𝕜 A B) :
     B.extremePoints 𝕜 ⊆ A.extremePoints 𝕜 :=
-  fun _ hx ↦ mem_extremePoints_iff_extreme_singleton.2
-    (hAB.trans (mem_extremePoints_iff_extreme_singleton.1 hx))
+  fun _ ↦ by simpa only [←isExtreme_singleton] using hAB.trans
 #align is_extreme.extreme_points_subset_extreme_points IsExtreme.extremePoints_subset_extremePoints
 
 theorem IsExtreme.extremePoints_eq (hAB : IsExtreme 𝕜 A B) :
@@ -236,6 +232,21 @@ theorem extremePoints_pi (s : ∀ i, Set (π i)) :
 
 end OrderedSemiring
 
+section OrderedRing
+variable {L : Type*} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
+  [LinearEquivClass L 𝕜 E F]
+
+lemma image_extremePoints (f : L) (s : Set E) :
+    f '' extremePoints 𝕜 s = extremePoints 𝕜 (f '' s) := by
+  ext b
+  obtain ⟨a, rfl⟩ := EquivLike.surjective f b
+  have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
+    image_openSegment _ (LinearMapClass.linearMap f).toAffineMap
+  simp only [mem_extremePoints, (EquivLike.surjective f).forall,
+    (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this]
+
+end OrderedRing
+
 section LinearOrderedRing
 
 variable [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E]
@@ -258,7 +269,7 @@ theorem mem_extremePoints_iff_forall_segment : x ∈ A.extremePoints 𝕜 ↔
 
 theorem Convex.mem_extremePoints_iff_convex_diff (hA : Convex 𝕜 A) :
     x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ Convex 𝕜 (A \ {x}) := by
-  use fun hx ↦ ⟨hx.1, (mem_extremePoints_iff_extreme_singleton.1 hx).convex_diff hA⟩
+  use fun hx ↦ ⟨hx.1, (isExtreme_singleton.2 hx).convex_diff hA⟩
   rintro ⟨hxA, hAx⟩
   refine' mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ _⟩
   rw [convex_iff_segment_subset] at hAx

Mathlib/Analysis/Convex/KreinMilman.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.Convex.Exposed
 import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+import Mathlib.Topology.Algebra.ContinuousAffineMap
 
 #align_import analysis.convex.krein_milman from "leanprover-community/mathlib"@"279297937dede7b1b3451b7b0f1786352ad011fa"
 
@@ -51,20 +52,19 @@ See chapter 8 of [Barry Simon, *Convexity*][simon2011]
 
 -/
 
-
 open Set
+open scoped Classical
 
-open Classical
-
-variable {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E]
+variable {E F : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E]
   [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E}
+  [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T1Space F]
 
 /-- **Krein-Milman lemma**: In a LCTVS, any nonempty compact set has an extreme point. -/
-theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty) :
+theorem IsCompact.extremePoints_nonempty (hscomp : IsCompact s) (hsnemp : s.Nonempty) :
     (s.extremePoints ℝ).Nonempty := by
   let S : Set (Set E) := { t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t }
   rsuffices ⟨t, ⟨⟨x, hxt⟩, htclos, hst⟩, hBmin⟩ : ∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t
-  · refine' ⟨x, mem_extremePoints_iff_extreme_singleton.2 _⟩
+  · refine ⟨x, IsExtreme.mem_extremePoints ?_⟩
     rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]
     by_contra hyx
     obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
@@ -88,7 +88,7 @@ theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty)
       (hFS t.mem).2.1
   obtain htu | hut := hF.total t.mem u.mem
   exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
-#align is_compact.has_extreme_point IsCompact.has_extreme_point
+#align is_compact.has_extreme_point IsCompact.extremePoints_nonempty
 
 /-- **Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull
     of its extreme points. -/
@@ -101,7 +101,24 @@ theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex
     geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
   have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
   obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn
-  obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩
+  obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩
   linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
     h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]
 #align closure_convex_hull_extreme_points closure_convexHull_extremePoints
+
+/-- A continuous affine map is surjective from the extreme points of a compact set to the extreme
+points of the image of that set. This inclusion is in general strict. -/
+lemma surjOn_extremePoints_image (f : E →A[ℝ] F) (hs : IsCompact s) :
+    SurjOn f (extremePoints ℝ s) (extremePoints ℝ (f '' s)) := by
+  rintro w hw
+  -- The fiber of `w` is nonempty and compact
+  have ht : IsCompact {x ∈ s | f x = w} := hs.inter_right $ isClosed_singleton.preimage f.continuous
+  have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw
+  -- Hence by the Krein-Milman lemma it has an extreme point `x`
+  obtain ⟨x, ⟨hx, rfl⟩, hyt⟩ := ht.extremePoints_nonempty ht₀
+  -- `f x = w` and `x` is an extreme point of `s`, so we're done
+  refine mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩
+  have := by simpa using image_openSegment _ f.toAffineMap y z
+  have := hw.2 (mem_image_of_mem _ hy) (mem_image_of_mem _ hz) $ by
+    rw [←this]; exact mem_image_of_mem _ hxyz
+  exact hyt ⟨hy, this.1⟩ ⟨hz, this.2⟩ hxyz

Mathlib/Analysis/Seminorm.lean

@@ -919,31 +919,6 @@ theorem closedBall_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x :
   exact closedBall_finset_sup_eq_iInter _ _ _ hr
 #align seminorm.closed_ball_finset_sup Seminorm.closedBall_finset_sup
 
-theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
-    Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
-  rw [Set.subset_def]
-  intro x hx
-  rw [Set.mem_smul] at hx
-  rcases hx with ⟨a, y, ha, hy, hx⟩
-  rw [← hx, mem_ball_zero, map_smul_eq_mul]
-  gcongr
-  · exact mem_ball_zero_iff.mp ha
-  · exact p.mem_ball_zero.mp hy
-#align seminorm.ball_smul_ball Seminorm.ball_smul_ball
-
-theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
-    Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by
-  rw [Set.subset_def]
-  intro x hx
-  rw [Set.mem_smul] at hx
-  rcases hx with ⟨a, y, ha, hy, hx⟩
-  rw [← hx, mem_closedBall_zero, map_smul_eq_mul]
-  rw [mem_closedBall_zero_iff] at ha
-  gcongr
-  · exact (norm_nonneg a).trans ha
-  · exact p.mem_closedBall_zero.mp hy
-#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall
-
 @[simp]
 theorem ball_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) : p.ball x r = ∅ := by
   ext
@@ -959,6 +934,37 @@ theorem closedBall_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r <
   exact hr.trans_le (map_nonneg _ _)
 #align seminorm.closed_ball_eq_emptyset Seminorm.closedBall_eq_emptyset
 
+theorem closedBall_smul_ball (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) :
+    Metric.closedBall (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
+  simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
+  refine fun a ha b hb ↦ mul_lt_mul' ha hb (map_nonneg _ _) ?_
+  exact hr₁.lt_or_lt.resolve_left <| ((norm_nonneg a).trans ha).not_lt
+
+theorem ball_smul_closedBall (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) :
+    Metric.ball (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
+  simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
+    map_smul_eq_mul]
+  intro a ha b hb
+  rw [mul_comm, mul_comm r₁]
+  refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_lt.resolve_left ?_)
+  exact ((map_nonneg p b).trans hb).not_lt
+
+theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
+    Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
+  rcases eq_or_ne r₂ 0 with rfl | hr₂
+  · simp
+  · exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans
+      (ball_smul_closedBall _ _ hr₂)
+#align seminorm.ball_smul_ball Seminorm.ball_smul_ball
+
+theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
+    Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by
+  simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
+  intro a ha b hb
+  gcongr
+  exact (norm_nonneg _).trans ha
+#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall
+
 -- Porting note: TODO: make that an `iff`
 theorem neg_mem_ball_zero (r : ℝ) (hx : x ∈ ball p 0 r) : -x ∈ ball p 0 r := by
   simpa only [mem_ball_zero, map_neg_eq_map] using hx

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -254,6 +254,11 @@ abbrev Sigma.desc {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P)
   colimit.desc _ (Cofan.mk P p)
 #align category_theory.limits.sigma.desc CategoryTheory.Limits.Sigma.desc
 
+instance {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a)) := by
+  convert IsIso.id _
+  ext
+  simp
+
 /-- A version of `Cocones.ext` for `Cofan`s. -/
 @[simps!]
 def Cofan.ext {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt)