Trigger CI for leanprover-community/batteries#1853

Author: mathlib-nightly-testing[bot]

Mathlib.lean

@@ -112,7 +112,6 @@ public import Mathlib.Algebra.Category.CommAlgCat.FiniteType
 public import Mathlib.Algebra.Category.CommAlgCat.Monoidal
 public import Mathlib.Algebra.Category.CommBialgCat
 public import Mathlib.Algebra.Category.CommHopfAlgCat
-public import Mathlib.Algebra.Category.ContinuousCohomology.Basic
 public import Mathlib.Algebra.Category.FGModuleCat.Abelian
 public import Mathlib.Algebra.Category.FGModuleCat.Basic
 public import Mathlib.Algebra.Category.FGModuleCat.Colimits
@@ -1442,6 +1441,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
 public import Mathlib.AlgebraicGeometry.Noetherian
 public import Mathlib.AlgebraicGeometry.Normalization
 public import Mathlib.AlgebraicGeometry.OpenImmersion
+public import Mathlib.AlgebraicGeometry.OrderOfVanishing
 public import Mathlib.AlgebraicGeometry.Over
 public import Mathlib.AlgebraicGeometry.PointsPi
 public import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
@@ -3242,6 +3242,7 @@ public import Mathlib.CategoryTheory.Preadditive.CommGrp_
 public import Mathlib.CategoryTheory.Preadditive.Comma
 public import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
 public import Mathlib.CategoryTheory.Preadditive.EndoFunctor
+public import Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
 public import Mathlib.CategoryTheory.Preadditive.FunctorCategory
 public import Mathlib.CategoryTheory.Preadditive.HomOrthogonal
 public import Mathlib.CategoryTheory.Preadditive.Indization
@@ -3381,6 +3382,7 @@ public import Mathlib.CategoryTheory.Sites.JointlySurjective
 public import Mathlib.CategoryTheory.Sites.LeftExact
 public import Mathlib.CategoryTheory.Sites.Limits
 public import Mathlib.CategoryTheory.Sites.LocalProperties
+public import Mathlib.CategoryTheory.Sites.LocalSite
 public import Mathlib.CategoryTheory.Sites.Localization
 public import Mathlib.CategoryTheory.Sites.LocallyBijective
 public import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
@@ -6379,6 +6381,8 @@ public import Mathlib.RepresentationTheory.Equiv
 public import Mathlib.RepresentationTheory.FDRep
 public import Mathlib.RepresentationTheory.FinGroupCharZero
 public import Mathlib.RepresentationTheory.FiniteIndex
+public import Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
+public import Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
 public import Mathlib.RepresentationTheory.Homological.FiniteCyclic
 public import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
 public import Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -125,15 +125,15 @@ lemma recOneCoe_coe {motive : WithOne α → Sort*} (h₁ h₂) (a : α) :
   rfl
 
 /-- Deconstruct an `x : WithOne α` to the underlying value in `α`, given a proof that `x ≠ 1`. -/
-@[to_additive unzero
+@[to_additive
 /-- Deconstruct an `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`. -/]
 def unone : ∀ {x : WithOne α}, x ≠ 1 → α | (x : α), _ => x
 
-@[to_additive (attr := simp) unzero_coe]
+@[to_additive (attr := simp)]
 theorem unone_coe {x : α} (hx : (x : WithOne α) ≠ 1) : unone hx = x :=
   rfl
 
-@[to_additive (attr := simp) coe_unzero]
+@[to_additive (attr := simp)]
 lemma coe_unone : ∀ {x : WithOne α} (hx : x ≠ 1), unone hx = x
   | (x : α), _ => rfl
 
@@ -194,4 +194,36 @@ instance instCommMonoid [CommSemigroup α] : CommMonoid (WithOne α) where
 theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : WithOne α) = (a : WithOne α)⁻¹ :=
   rfl
 
+/--
+Specialization of `Option.getD` to values in `WithOne α` that respects API boundaries.
+-/
+@[to_additive
+  /-- Specialization of `Option.getD` to values in `WithZero α` that respects API boundaries. -/]
+def unoneD (d : α) (x : WithOne α) : α := recOneCoe d id x
+
+@[to_additive (attr := simp)]
+theorem unoneD_one (d : α) : unoneD d 1 = d :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem unoneD_coe (d x : α) : unoneD d x = x :=
+  rfl
+
+@[to_additive]
+theorem unoneD_eq_iff {d y : α} {x : WithOne α} : unoneD d x = y ↔ x = y ∨ x = 1 ∧ y = d := by
+  induction x <;> simp [@eq_comm _ d]
+
+@[to_additive (attr := simp)]
+theorem unoneD_eq_self_iff {d : α} {x : WithOne α} : unoneD d x = d ↔ x = d ∨ x = 1 := by
+  simp [unoneD_eq_iff]
+
+@[to_additive]
+theorem unoneD_eq_unoneD_iff {d : α} {x y : WithOne α} :
+    unoneD d x = unoneD d y ↔ x = y ∨ x = d ∧ y = 1 ∨ x = 1 ∧ y = d := by
+  induction y <;> simp [unoneD_eq_iff, or_comm]
+
+@[to_additive]
+lemma unoneD_eq_unone {d : α} {x : WithOne α} (hx : x ≠ 1) : unoneD d x = unone hx := by
+  simp [unoneD_eq_iff]
+
 end WithOne

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -197,23 +197,21 @@ theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective
 alias _root_.LinearMapClass.ker_eq_bot := ker_eq_bot
 
 @[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
-    Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by
-  rw [← LinearMap.ker_eq_bot]
-  refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
-  · intro x ⟨hx, h'x⟩
-    have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x
-    rw [h] at this
-    simpa [mk_eq_zero] using this
-  · rintro ⟨x, hx⟩ h'x
-    have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩
-    rw [h] at this
-    simpa [mk_eq_zero] using this
-
-@[simp] theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M}
-    (hf : ∀ x ∈ p, f x ∈ p) :
-    Injective (f.restrict hf) ↔ Disjoint p (ker f) := by
-  rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
-    disjoint_iff]
+    Injective (f.domRestrict S) ↔ Disjoint S f.ker := by
+  simp [← ker_eq_bot, ker_domRestrict, disjoint_iff_comap_eq_bot]
+
+@[simp]
+theorem injective_restrict_iff {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂}
+    (hf : ∀ x ∈ p, f x ∈ q) : Injective (f.restrict hf) ↔ Disjoint p (ker f) := by
+  simp [← ker_eq_bot, ker_restrict, disjoint_iff_comap_eq_bot]
+
+@[deprecated (since := "2026-07-01")]
+alias injective_restrict_iff_disjoint := injective_restrict_iff
+
+@[simp]
+theorem injective_codRestrict_iff {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂}
+    (hf : ∀ x, f x ∈ q) : Injective (f.codRestrict q hf) ↔ Injective f :=
+  Set.injective_codRestrict _
 
 end Ring