Sync upstream mathlib4 (2026-08-02, +12 commits)

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -96,7 +96,7 @@ Projection of a needle onto the x-axis. The needle's center is at x-coordinate `
 `l` and angle `θ`. Note, `θ` is measured relative to the y-axis, that is, a vertical needle has
 `θ = 0`.
 -/
-def needleProjX (x θ : ℝ) : Set ℝ := Set.Icc (x - θ.sin * l / 2) (x + θ.sin * l / 2)
+noncomputable def needleProjX (x θ : ℝ) : Set ℝ := Set.Icc (x - θ.sin * l / 2) (x + θ.sin * l / 2)
 
 /--
 The indicator function of whether a needle at position `⟨x, θ⟩ : ℝ × ℝ` crosses the line `x = 0`.
@@ -120,7 +120,7 @@ noncomputable def N : Ω → ℝ := needleCrossesIndicator l ∘ B
 /--
 The possible x-positions and angle relative to the y-axis of a needle.
 -/
-abbrev needleSpace : Set (ℝ × ℝ) := Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 π
+noncomputable abbrev needleSpace : Set (ℝ × ℝ) := Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 π
 
 include hd in
 lemma volume_needleSpace : ℙ (needleSpace d) = ENNReal.ofReal (d * π) := by

Counterexamples/TopologistsSineCurve.lean

@@ -31,14 +31,14 @@ open Topology Filter Set Real
 namespace TopologistsSineCurve
 
 /-- The topologist's sine curve, i.e. the graph of `y = sin (x⁻¹)` for `0 < x`. -/
-def S : Set (ℝ × ℝ) := (fun x ↦ (x, sin x⁻¹)) '' Ioi 0
+noncomputable def S : Set (ℝ × ℝ) := (fun x ↦ (x, sin x⁻¹)) '' Ioi 0
 
 /-- The vertical line segment `{ (0, y) | -1 ≤ y ≤ 1 }`, which is the set of limit points of `S`
 not contained in `S` itself. -/
 def Z : Set (ℝ × ℝ) := (fun y ↦ (0, y)) '' Icc (-1) 1
 
 /-- The union of `S` and `Z` (which we will show is the closure of `S`). -/
-def T : Set (ℝ × ℝ) := S ∪ Z
+noncomputable def T : Set (ℝ × ℝ) := S ∪ Z
 
 /-- A sequence of `x`-values tending to 0 at which the sine curve has a given `y`-coordinate. -/
 noncomputable def xSeq (y : ℝ) (k : ℕ) := 1 / (arcsin y + (k + 1) * (2 * π))

Mathlib/Algebra/DirectSum/Basic.lean

@@ -305,14 +305,20 @@ section CongrLeft
 
 variable {κ : Type*}
 
-/-- Reindexing terms of a direct sum. -/
+/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence
+`h : ι ≃ κ`. -/
 def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) :=
   { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv }
 
 @[simp]
 theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) :
-    equivCongrLeft h f k = f (h.symm k) := by
-  exact DFinsupp.comapDomain'_apply _ h.right_inv _ _
+    equivCongrLeft h f k = f (h.symm k) :=
+  DFinsupp.comapDomain'_apply _ h.right_inv _ _
+
+@[simp]
+theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) :
+    equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x :=
+  DFinsupp.comapDomain'_single h.symm h.right_inv _ _
 
 end CongrLeft
 
@@ -342,6 +348,12 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i)
     sigmaCurry f i j = f ⟨i, j⟩ :=
   DFinsupp.sigmaCurry_apply (δ := δ) _ i j
 
+@[simp]
+theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i) (x : δ k.1 k.2) :
+    sigmaCurry (of (fun k ↦ δ k.1 k.2) k x) =
+      of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) :=
+  DFinsupp.sigmaCurry_single k x
+
 /-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`. -/
 def sigmaUncurry : (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2 where
@@ -360,6 +372,37 @@ def sigmaCurryEquiv : (⨁ i : Σ _i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j :=
 
 end Sigma
 
+section SigmaFiber
+
+variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂)
+variable {β : ι₁ → Type w} [Π i, AddCommMonoid (β i)]
+
+/-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type
+`ι₂` together with the fibres of a map `f : ι₁ → ι₂`. -/
+def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i :=
+  (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans
+    (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i)))
+
+theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) :
+    sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := rfl
+
+@[simp]
+theorem sigmaFiberAddEquiv_apply_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) :
+    sigmaFiberAddEquiv f x j i' = x i' := rfl
+
+@[simp]
+theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) :
+    sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) :=
+  let h := Equiv.sigmaFiberEquiv f
+  let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩
+  calc sigmaFiberAddEquiv f (of β (h k) x)
+    _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by
+      rw [sigmaFiberAddEquiv_apply]
+      exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _)
+    _ = of _ k.1 (of _ k.2 x) := by simp
+
+end SigmaFiber
+
 /-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `AddSubmonoid M`
 indexed by `ι`.
 

Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean

@@ -16,7 +16,7 @@ where `C` has enough injectives, we define the right derived functor
 between the corresponding bounded below derived categories.
 
 TODO(@joelriou): show that this functor is triangulated and refactor
-the definiton of `Functor.rightDerived`
+the definition of `Functor.rightDerived`
 
 -/
 

Mathlib/Algebra/Homology/Homotopy.lean

@@ -714,9 +714,12 @@ def HomologicalComplex.homotopyEquivalences :
 
 namespace HomotopyEquiv
 
+variable {C D E : HomologicalComplex V c}
+
+variable (C) in
 /-- Any complex is homotopy equivalent to itself. -/
-@[refl]
-def refl (C : HomologicalComplex V c) : HomotopyEquiv C C where
+@[refl, simps]
+def refl : HomotopyEquiv C C where
   hom := 𝟙 C
   inv := 𝟙 C
   homotopyHomInvId := Homotopy.ofEq (by simp)
@@ -726,16 +729,16 @@ instance : Inhabited (HomotopyEquiv C C) :=
   ⟨refl C⟩
 
 /-- Being homotopy equivalent is a symmetric relation. -/
-@[symm]
-def symm {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : HomotopyEquiv D C where
+@[symm, simps]
+def symm (f : HomotopyEquiv C D) : HomotopyEquiv D C where
   hom := f.inv
   inv := f.hom
   homotopyHomInvId := f.homotopyInvHomId
   homotopyInvHomId := f.homotopyHomInvId
 
 /-- Homotopy equivalence is a transitive relation. -/
-@[trans]
-def trans {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E) :
+@[trans, simps]
+def trans (f : HomotopyEquiv C D) (g : HomotopyEquiv D E) :
     HomotopyEquiv C E where
   hom := f.hom ≫ g.hom
   inv := g.inv ≫ f.inv
@@ -749,8 +752,59 @@ def ofIso {ι : Type*} {V : Type u} [Category.{v} V] [Preadditive V] {c : Comple
     {C D : HomologicalComplex V c} (f : C ≅ D) : HomotopyEquiv C D :=
   ⟨f.hom, f.inv, Homotopy.ofEq f.3, Homotopy.ofEq f.4⟩
 
+lemma homotopyEquivalences_hom (f : HomotopyEquiv C D) :
+    homotopyEquivalences _ _ f.hom := ⟨f, rfl⟩
+
+lemma homotopyEquivalences_inv (f : HomotopyEquiv C D) :
+    homotopyEquivalences _ _ f.inv := f.symm.homotopyEquivalences_hom
+
+/-- If `f` if a homotopy equivalence and `h` is a homotopy from `f.hom` to
+a morphism `g`, then this is a homotopy equivalence whose `hom` field is `g`. -/
+@[simps hom inv]
+def copy (f : HomotopyEquiv C D) {g : C ⟶ D} (h : Homotopy f.hom g) :
+    HomotopyEquiv C D where
+  hom := g
+  inv := f.inv
+  homotopyHomInvId := (h.symm.compRight _).trans f.homotopyHomInvId
+  homotopyInvHomId := (h.symm.compLeft _).trans f.homotopyInvHomId
+
 end HomotopyEquiv
 
+namespace HomologicalComplex
+
+lemma homotopyEquivalences.of_isIso (f : C ⟶ D) [IsIso f] : homotopyEquivalences _ _ f :=
+  ⟨.ofIso (asIso f), rfl⟩
+
+lemma homotopyEquivalences.of_homotopy {f g : C ⟶ D} (h : homotopyEquivalences _ _ f)
+    (hfg : Homotopy f g) :
+    homotopyEquivalences _ _ g := by
+  obtain ⟨e, rfl⟩ := h
+  exact ⟨e.copy hfg, by simp⟩
+
+instance : (homotopyEquivalences V c).IsMultiplicative where
+  id_mem K := ⟨.refl _, rfl⟩
+  comp_mem f g := by
+    rintro ⟨f, rfl⟩ ⟨g, rfl⟩
+    exact ⟨f.trans g, rfl⟩
+
+instance : (homotopyEquivalences V c).HasTwoOutOfThreeProperty where
+  of_postcomp f _ := by
+    rintro ⟨g, rfl⟩ ⟨e, he⟩
+    refine (e.trans g.symm).homotopyEquivalences_hom.of_homotopy ?_
+    simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, Category.assoc]
+    exact g.homotopyHomInvId.compLeftId f
+  of_precomp _ g := by
+    rintro ⟨f, rfl⟩ ⟨e, he⟩
+    refine (f.symm.trans e).homotopyEquivalences_hom.of_homotopy ?_
+    simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, ← Category.assoc]
+    exact f.homotopyInvHomId.compRightId g
+
+instance : (homotopyEquivalences V c).RespectsIso :=
+  MorphismProperty.respectsIso_of_isStableUnderComposition
+    (fun _ _ _ _ ↦ .of_isIso _)
+
+end HomologicalComplex
+
 end
 
 namespace CategoryTheory

Mathlib/Algebra/Order/Star/Basic.lean

@@ -472,7 +472,7 @@ instance (priority := 100) StarRingEquivClass.instOrderIsoClass [EquivLike F R S
 
 /-- While `IsSelfAdjoint.map` assumes the map is star-preserving, this lemma instead assumes the
 map is an order-preserving additive map from a space where self-adjoint elements can be expressed as
-differences of nonnegative elemens, and whose codomain is a star-ordered ring. When such maps are
+differences of nonnegative elements, and whose codomain is a star-ordered ring. When such maps are
 linear over `ℂ`, they are also star-preserving, and this lemma is used to establish that one by
 splitting into real and imaginary parts. -/
 @[aesop safe apply (rule_sets := [CStarAlgebra])]

Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

@@ -254,7 +254,7 @@ noncomputable def toNondegComplex : K[X] ⟶ s.nondegComplex :=
 set_option backward.defeqAttrib.useBackward true in
 /-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
 this is the split monomormphism from the chain complex `s.nondegComplex` to
-the alternating face map complex fo `X`. -/
+the alternating face map complex of `X`. -/
 @[no_expose]
 noncomputable def fromNondegComplex : s.nondegComplex ⟶ K[X] :=
   (fullyFaithfulToKaroubi _).preimage

Mathlib/Analysis/CStarAlgebra/Basic.lean

@@ -77,6 +77,26 @@ instance [NormedField 𝕜] [NormedSpace 𝕜 E] [Star 𝕜] [TrivialStar 𝕜]
     NormedSpace 𝕜 (selfAdjoint E) where
   norm_smul_le _ _ := norm_smul_le _ (_ : E)
 
+variable (x : E) (r : ℝ)
+
+@[simp] lemma Metric.star_ball : star (ball x r) = ball (star x) r := by
+  simpa using star_isometry.preimage_ball (star x) r
+
+@[simp] lemma Metric.star_closedBall : star (closedBall x r) = closedBall (star x) r := by
+  simpa using star_isometry.preimage_closedBall (star x) r
+
+@[simp] lemma Metric.star_sphere : star (sphere x r) = sphere (star x) r := by
+  simpa using star_isometry.preimage_sphere (star x) r
+
+@[simp] lemma dist_star_star (x y : E) : dist (star x) (star y) = dist x y :=
+  star_isometry.dist_eq x y
+
+@[simp] lemma edist_star_star (x y : E) : edist (star x) (star y) = edist x y :=
+  star_isometry.edist_eq x y
+
+@[simp] lemma nndist_star_star (x y : E) : nndist (star x) (star y) = nndist x y :=
+  star_isometry.nndist_eq x y
+
 end NormedStarGroup
 
 instance RingHomIsometric.starRingEnd [NormedCommRing E] [StarRing E] [NormedStarGroup E] :

Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean

@@ -117,7 +117,7 @@ theorem gl_smul_eq_self_iff_quadratic (h : 0 < g.val.det) :
   simp [gl_smul_eq_iff_num_eq, σ, h, num, denom]
   grind
 
-/-- If `g` is a non-scalar orientation perserving matrix with a fixed point in `ℍ`,
+/-- If `g` is a non-scalar orientation preserving matrix with a fixed point in `ℍ`,
 then it's an elliptic matrix. -/
 theorem isElliptic_of_exists_smul_eq_self (h : 0 < g.val.det) (hgc : g ∉ Subgroup.center _)
     (hfix : ∃ z : ℍ, g • z = z) : g.IsElliptic := by

Mathlib/CategoryTheory/IsoCat.lean

@@ -17,7 +17,7 @@ This is a strict notion, stronger than an equivalence of categories `C ≌ D`.
 We also define `Functor.IsIso` as a property saying that a functor is fully faithful and
 bijective on objects. We develop basic api for these two concepts.
 
-Unless the application explicitely demands an isomorphism, the equivalence of categories is
+Unless the application explicitly demands an isomorphism, the equivalence of categories is
 to be preferred.
 
 ## Main definitions

Mathlib/CategoryTheory/Limits/Elements.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
+Authors: Markus Himmel, Emily Riehl
 -/
 module
 
@@ -22,10 +22,6 @@ the category of elements of `A` has limits of shape `I` and the forgetful functo
 
 - If `A` is (co)representable, then `A.Elements` has an initial object.
 
-## TODOs
-
-- Show that `A` is (co)representable if `A.Elements` has an initial object.
-
 -/
 
 set_option backward.defeqAttrib.useBackward true
@@ -135,4 +131,53 @@ end Initial
 
 end CategoryOfElements
 
+namespace Functor.Elements
+
+/-- An initial object in the category `F.Elements` of a covariant functor defines a
+corepresentation for that functor. -/
+def corepresentableByOfIsInitial {F : C ⥤ Type w} {E : Elements F} (he : IsInitial E) :
+    CorepresentableBy F E.fst where
+  homEquiv :=
+    { toFun f := F.map f E.snd
+      invFun y := (he.to ⟨_, y⟩).val
+      left_inv f := Subtype.ext_iff.mp (he.hom_ext (he.to ⟨_, F.map f E.snd⟩) ⟨f, rfl⟩)
+      right_inv y := (he.to ⟨_, y⟩).prop }
+
+lemma isCorepresentable_of_hasInitial (F : C ⥤ Type w) [HasInitial (Elements F)] :
+    IsCorepresentable F where
+  has_corepresentation :=
+    ⟨(⊥_ F.Elements).fst,
+      (Nonempty.intro (corepresentableByOfIsInitial initialIsInitial))⟩
+
+theorem hasInitial_iff_isCorepresentable (F : C ⥤ Type w) :
+    HasInitial (Elements F) ↔ IsCorepresentable F where
+  mp _ := isCorepresentable_of_hasInitial F
+  mpr _ := inferInstance
+
+/-- An initial object in the category `F.Elements` of a contravariant functor defines a
+representation for that functor. -/
+def representableByOfIsInitial {F : Cᵒᵖ ⥤ Type w} {E : Elements F} (he : IsInitial E) :
+    RepresentableBy F (E.fst.unop) where
+  homEquiv :=
+    { toFun f := F.map f.op E.snd
+      invFun y := (he.to ⟨_, y⟩).val.unop
+      left_inv f := by
+        have :=
+          Subtype.ext_iff.mp (he.hom_ext (he.to ⟨_, F.map f.op E.snd⟩) ⟨f.op, rfl⟩)
+        simp only [this, Quiver.Hom.unop_op]
+      right_inv y := (he.to ⟨_, y⟩).prop }
+
+lemma isRepresentable_of_hasInitial (F : Cᵒᵖ ⥤ Type w) [HasInitial (Elements F)] :
+    IsRepresentable F where
+  has_representation :=
+    ⟨(⊥_ F.Elements).fst.unop,
+      (Nonempty.intro (representableByOfIsInitial initialIsInitial))⟩
+
+theorem hasInitial_iff_isRepresentable (F : Cᵒᵖ ⥤ Type w) :
+    HasInitial (Elements F) ↔ IsRepresentable F where
+  mp _ := isRepresentable_of_hasInitial F
+  mpr _ := inferInstance
+
+end Functor.Elements
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Precoverage/Generates.lean

@@ -74,7 +74,7 @@ lemma Generates.isSheaf_of_forall (h : K.Generates J) (F : Cᵒᵖ ⥤ Type w)
   /- By assumption, the statement holds for `w = max u v`. The idea of the proof is
   to construct a suitable `Type max u v` valued subsheaf of `F` for each covering sieve `S` in
   `J` and every family of sections over `S` to check the necessary conditions.
-  We explain existence below, uniqueness works similary. -/
+  We explain existence below, uniqueness works similarly. -/
   intro X S hS
   rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
   refine ⟨?_, ?_⟩

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -402,9 +402,9 @@ lemma reachable_eq_of_maximal_isAcyclic (F : SimpleGraph V)
   have : ∃ d ∈ p.darts, d.fst ∈ s ∧ d.snd ∉ s := p.exists_boundary_dart s rfl this
   rcases this with ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩
   have : ¬F.Reachable v' u' := mt ConnectedComponent.sound <| s.mem_supp_iff u' |>.mp hu ▸ hv
-  suffices F ⊔ edge v' u' ≤ F by grind [Adj.reachable, sup_le_iff, le_iff_adj, edge_adj]
+  suffices F ⊔ edge v' u' ≤ F by grind [Adj.reachable, sup_le_iff, le_iff_adj]
   refine h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left
-  grind [Maximal, sup_le, le_iff_adj, edge_adj, huv.symm]
+  grind [Maximal, sup_le, le_iff_adj, huv.symm]
 
 /-- A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph. -/
 theorem maximal_isAcyclic_iff_reachable_eq {F : SimpleGraph V} (hle : F ≤ G) (hF : F.IsAcyclic) :

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -221,7 +221,7 @@ instance : Max (SimpleGraph V) where
     { Adj := x.Adj ⊔ y.Adj
       symm.symm v w h := by rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm] }
 
-@[simp]
+@[simp, grind =]
 theorem sup_adj (x y : SimpleGraph V) (v w : V) : (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w :=
   Iff.rfl