Trigger CI for leanprover-community/batteries#1099

Mathlib.lean

@@ -2268,7 +2268,6 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
-import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
 import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
 import Mathlib.CategoryTheory.Square

Mathlib/Algebra/Free.lean

@@ -61,9 +61,6 @@ instance [Inhabited α] : Inhabited (FreeMagma α) := ⟨of default⟩
 @[to_additive]
 instance : Mul (FreeMagma α) := ⟨FreeMagma.mul⟩
 
--- Porting note: invalid attribute 'match_pattern', declaration is in an imported module
--- attribute [match_pattern] Mul.mul
-
 @[to_additive (attr := simp)]
 theorem mul_eq (x y : FreeMagma α) : mul x y = x * y := rfl
 
@@ -80,12 +77,10 @@ theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f 
 
 end FreeMagma
 
-#adaptation_note /-- nightly-2024-02-25
-we need to write `mul x y` in the second pattern, instead of `x * y`. --/
 /-- Lifts a function `α → β` to a magma homomorphism `FreeMagma α → β` given a magma `β`. -/
 def FreeMagma.liftAux {α : Type u} {β : Type v} [Mul β] (f : α → β) : FreeMagma α → β
   | FreeMagma.of x => f x
-  | mul x y => liftAux f x * liftAux f y
+  | x * y => liftAux f x * liftAux f y
 
 /-- Lifts a function `α → β` to an additive magma homomorphism `FreeAddMagma α → β` given
 an additive magma `β`. -/
@@ -185,13 +180,11 @@ end Category
 
 end FreeMagma
 
-#adaptation_note /-- nightly-2024-02-25
-we need to write `mul x y` in the second pattern, instead of `x * y`. -/
 /-- `FreeMagma` is traversable. -/
 protected def FreeMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u}
     (F : α → m β) : FreeMagma α → m (FreeMagma β)
   | FreeMagma.of x => FreeMagma.of <$> F x
-  | mul x y => (· * ·) <$> x.traverse F <*> y.traverse F
+  | x * y => (· * ·) <$> x.traverse F <*> y.traverse F
 
 /-- `FreeAddMagma` is traversable. -/
 protected def FreeAddMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u}
@@ -262,12 +255,10 @@ end Category
 
 end FreeMagma
 
-#adaptation_note /-- nightly-2024-02-25
-we need to write `mul x y` in the second pattern, instead of `x * y`. -/
 /-- Representation of an element of a free magma. -/
 protected def FreeMagma.repr {α : Type u} [Repr α] : FreeMagma α → Lean.Format
   | FreeMagma.of x => repr x
-  | mul x y => "( " ++ x.repr ++ " * " ++ y.repr ++ " )"
+  | x * y => "( " ++ x.repr ++ " * " ++ y.repr ++ " )"
 
 /-- Representation of an element of a free additive magma. -/
 protected def FreeAddMagma.repr {α : Type u} [Repr α] : FreeAddMagma α → Lean.Format
@@ -279,12 +270,10 @@ attribute [to_additive existing] FreeMagma.repr
 @[to_additive]
 instance {α : Type u} [Repr α] : Repr (FreeMagma α) := ⟨fun o _ => FreeMagma.repr o⟩
 
-#adaptation_note /-- nightly-2024-02-25
-we need to write `mul x y` in the second pattern, instead of `x * y`. -/
 /-- Length of an element of a free magma. -/
 def FreeMagma.length {α : Type u} : FreeMagma α → ℕ
   | FreeMagma.of _x => 1
-  | mul x y => x.length + y.length
+  | x * y => x.length + y.length
 
 /-- Length of an element of a free additive magma. -/
 def FreeAddMagma.length {α : Type u} : FreeAddMagma α → ℕ

Mathlib/Algebra/LinearRecurrence.lean

@@ -92,7 +92,8 @@ theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α}
   rw [mkSol]
   split_ifs with h'
   · exact mod_cast heq ⟨n, h'⟩
-  · rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
+  · dsimp only
+    rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
     congr with k
     have : n - E.order + k < n := by omega
     rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -640,12 +640,12 @@ $r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$. -/
 theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
     [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
     l.prod.snd =
-      (l.enum.map fun x : ℕ × tsze R M =>
-          ((l.map fst).take x.1).prod •> x.snd.snd <• ((l.map fst).drop x.1.succ).prod).sum := by
+      (l.zipIdx.map fun x : tsze R M × ℕ =>
+          ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum := by
   induction l with
   | nil => simp
   | cons x xs ih =>
-    rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom]
+    rw [List.zipIdx_cons']
     simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
       List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
       List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,

Mathlib/Analysis/Analytic/Composition.lean

@@ -550,7 +550,7 @@ def compChangeOfVariables (m M N : ℕ) (i : Σ n, Fin n → ℕ) (hi : i ∈ co
   rw [mem_compPartialSumSource_iff] at hi
   refine ⟨∑ j, f j, ofFn fun a => f a, fun hi' => ?_, by simp [sum_ofFn]⟩
   rename_i i
-  obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn, Set.mem_range] at hi'
+  obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'
   exact (hi.2 j).1
 
 @[simp]

Mathlib/CategoryTheory/SmallObject/Construction.lean

@@ -9,18 +9,18 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
 /-!
 # Construction for the small object argument
 
-Given a family of morphisms `f i : A i ⟶ B i` in a category `C`
-and an object `S : C`, we define a functor
-`SmallObject.functor f S : Over S ⥤ Over S` which sends
-an object given by `πX : X ⟶ S` to the pushout `functorObj f πX`:
+Given a family of morphisms `f i : A i ⟶ B i` in a category `C`,
+we define a functor
+`SmallObject.functor f : Arrow S ⥤ Arrow S` which sends
+an object given by arrow `πX : X ⟶ S` to the pushout `functorObj f πX`:
 ```
 ∐ functorObjSrcFamily f πX ⟶       X
 
             |                      |
             |                      |
             v                      v
 
-∐ functorObjTgtFamily f πX ⟶ functorObj f S πX
+∐ functorObjTgtFamily f πX ⟶ functorObj f πX
 ```
 where the morphism on the left is a coproduct (of copies of maps `f i`)
 indexed by a type `FunctorObjIndex f πX` which parametrizes the
@@ -33,8 +33,8 @@ A i ⟶ X
 B i ⟶ S
 ```
 
-The morphism `ιFunctorObj f S πX : X ⟶ functorObj f πX` is part of
-a natural transformation `SmallObject.ε f S : 𝟭 (Over S) ⟶ functor f S`.
+The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is part of
+a natural transformation `SmallObject.ε f : 𝟭 (Arrow C) ⟶ functor f S`.
 The main idea in this construction is that for any commutative square
 as above, there may not exist a lifting `B i ⟶ X`, but the construction
 provides a tautological morphism `B i ⟶ functorObj f πX`
@@ -62,7 +62,7 @@ variable {C : Type u} [Category.{v} C] {I : Type w} {A B : I → C} (f : ∀ i,
 
 section
 
-variable {S : C} {X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y)
+variable {S X : C} (πX : X ⟶ S)
 
 /-- Given a family of morphisms `f i : A i ⟶ B i` and a morphism `πX : X ⟶ S`,
 this type parametrizes the commutative squares with a morphism `f i` on the left
@@ -79,7 +79,6 @@ structure FunctorObjIndex where
 attribute [reassoc (attr := simp)] FunctorObjIndex.w
 
 variable [HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C]
-  [HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C]
 
 /-- The family of objects `A x.i` parametrized by `x : FunctorObjIndex f πX`. -/
 abbrev functorObjSrcFamily (x : FunctorObjIndex f πX) : C := A x.i
@@ -101,10 +100,9 @@ noncomputable abbrev functorObjLeft :
     ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX :=
   Limits.Sigma.map (functorObjLeftFamily f πX)
 
-section
 variable [HasPushout (functorObjTop f πX) (functorObjLeft f πX)]
 
-/-- The functor `SmallObject.functor f S : Over S ⥤ Over S` that is part of
+/-- The functor `SmallObject.functor f : Arrow C ⥤ Arrow C` that is part of
 the small object argument for a family of morphisms `f`, on an object given
 as a morphism `πX : X ⟶ S`. -/
 noncomputable abbrev functorObj : C :=
@@ -141,79 +139,92 @@ lemma ρFunctorObj_π : ρFunctorObj f πX ≫ πFunctorObj f πX = π'FunctorOb
 lemma ιFunctorObj_πFunctorObj : ιFunctorObj f πX ≫ πFunctorObj f πX = πX := by
   simp [ιFunctorObj, πFunctorObj]
 
-/-- The canonical morphism `∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY)`
-induced by a morphism in `φ : X ⟶ Y` such that `φ ≫ πX = πY`. -/
-noncomputable def functorMapSrc (hφ : φ ≫ πY = πX) :
-    ∐ (functorObjSrcFamily f πX) ⟶ ∐ functorObjSrcFamily f πY :=
-  Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ φ) x.b (by simp [hφ])) (fun _ => 𝟙 _)
+section
 
-end
+variable {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY)
+  [HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C]
+  [HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C]
 
-variable (hφ : φ ≫ πY = πX)
+/-- The canonical morphism `∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY)`
+induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`. -/
+noncomputable def functorMapSrc :
+    ∐ (functorObjSrcFamily f πX) ⟶ ∐ functorObjSrcFamily f πY :=
+  Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ τ.left) (x.b ≫ τ.right) (by simp))
+    (fun _ => 𝟙 _)
 
 @[reassoc]
 lemma ι_functorMapSrc (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b)
-    (t' : A i ⟶ Y) (fac : t ≫ φ = t') :
-    Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapSrc f πX πY φ hφ =
+    (b' : B i ⟶ T) (hb' : b ≫ τ.right = b')
+    (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') :
+    Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapSrc f τ =
       Sigma.ι (functorObjSrcFamily f πY)
-        (FunctorObjIndex.mk i t' b (by rw [← w, ← fac, assoc, hφ])) := by
-  subst fac
+        (FunctorObjIndex.mk i t' b' (by
+          have := τ.w
+          dsimp at this
+          rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) := by
+  subst hb' ht'
   simp [functorMapSrc]
 
 @[reassoc (attr := simp)]
 lemma functorMapSrc_functorObjTop :
-    functorMapSrc f πX πY φ hφ ≫ functorObjTop f πY = functorObjTop f πX ≫ φ := by
+    functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ τ.left := by
   ext ⟨i, t, b, w⟩
-  simp [ι_functorMapSrc_assoc f πX πY φ hφ i t b w _ rfl]
+  simp [ι_functorMapSrc_assoc f τ i t b w _ rfl]
 
 /-- The canonical morphism `∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY`
-induced by a morphism in `φ : X ⟶ Y` such that `φ ≫ πX = πY`. -/
-noncomputable def functorMapTgt (hφ : φ ≫ πY = πX) :
+induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`. -/
+noncomputable def functorMapTgt :
     ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY :=
-  Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ φ) x.b (by simp [hφ])) (fun _ => 𝟙 _)
+  Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ τ.left) (x.b ≫ τ.right) (by simp))
+    (fun _ => 𝟙 _)
 
 @[reassoc]
 lemma ι_functorMapTgt (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b)
-    (t' : A i ⟶ Y) (fac : t ≫ φ = t') :
-    Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapTgt f πX πY φ hφ =
+    (b' : B i ⟶ T) (hb' : b ≫ τ.right = b')
+    (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') :
+    Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapTgt f τ =
       Sigma.ι (functorObjTgtFamily f πY)
-        (FunctorObjIndex.mk i t' b (by rw [← w, ← fac, assoc, hφ])) := by
-  subst fac
+        (FunctorObjIndex.mk i t' b' (by
+          have := τ.w
+          dsimp at this
+          rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) := by
+  subst hb' ht'
   simp [functorMapTgt]
 
 lemma functorMap_comm :
-    functorObjLeft f πX ≫ functorMapTgt f πX πY φ hφ =
-      functorMapSrc f πX πY φ hφ ≫ functorObjLeft f πY := by
+    functorObjLeft f πX ≫ functorMapTgt f τ =
+      functorMapSrc f τ ≫ functorObjLeft f πY := by
   ext ⟨i, t, b, w⟩
   simp only [ι_colimMap_assoc, Discrete.natTrans_app, ι_colimMap,
-    ι_functorMapTgt f πX πY φ hφ i t b w _ rfl,
-    ι_functorMapSrc_assoc f πX πY φ hφ i t b w _ rfl]
+    ι_functorMapTgt f τ i t b w _ rfl,
+    ι_functorMapSrc_assoc f τ i t b w _ rfl]
 
 variable [HasPushout (functorObjTop f πX) (functorObjLeft f πX)]
   [HasPushout (functorObjTop f πY) (functorObjLeft f πY)]
 
-/-- The functor `SmallObject.functor f S : Over S ⥤ Over S` that is part of
+/-- The functor `SmallObject.functor f S : Arrow S ⥤ Arrow S` that is part of
 the small object argument for a family of morphisms `f`, on morphisms. -/
 noncomputable def functorMap : functorObj f πX ⟶ functorObj f πY :=
-  pushout.map _ _ _ _ φ (functorMapTgt f πX πY φ hφ) (functorMapSrc f πX πY φ hφ) (by simp)
-    (functorMap_comm f πX πY φ hφ)
+  pushout.map _ _ _ _ τ.left (functorMapTgt f τ) (functorMapSrc f τ) (by simp)
+    (functorMap_comm f τ)
 
 @[reassoc (attr := simp)]
-lemma functorMap_π : functorMap f πX πY φ hφ ≫ πFunctorObj f πY = πFunctorObj f πX := by
+lemma functorMap_π : functorMap f τ ≫ πFunctorObj f πY = πFunctorObj f πX ≫ τ.right := by
   ext ⟨i, t, b, w⟩
-  · simp [functorMap, hφ]
-  · simp [functorMap, ι_functorMapTgt_assoc f πX πY φ hφ i t b w _ rfl]
+  · simp [functorMap]
+  · simp [functorMap, ι_functorMapTgt_assoc f τ i t b w _ rfl]
 
 variable (X) in
 @[simp]
-lemma functorMap_id : functorMap f πX πX (𝟙 X) (by simp) = 𝟙 _ := by
+lemma functorMap_id : functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 _ := by
   ext ⟨i, t, b, w⟩
   · simp [functorMap]
-  · simp [functorMap, ι_functorMapTgt_assoc f πX πX (𝟙 X) (by simp) i t b w t (by simp)]
+  · simp [functorMap,
+      ι_functorMapTgt_assoc f (𝟙 (Arrow.mk πX)) i t b w b (by simp) t (by simp)]
 
 @[reassoc (attr := simp)]
 lemma ιFunctorObj_naturality :
-    ιFunctorObj f πX ≫ functorMap f πX πY φ hφ = φ ≫ ιFunctorObj f πY := by
+    ιFunctorObj f πX ≫ functorMap f τ = τ.left ≫ ιFunctorObj f πY := by
   simp [ιFunctorObj, functorMap]
 
 lemma ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S)
@@ -225,31 +236,39 @@ lemma ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S)
 
 end
 
-variable (S : C) [HasPushouts C]
-  [∀ {X : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C]
+variable [HasPushouts C]
+  [∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C]
 
-/-- The functor `Over S ⥤ Over S` that is constructed in order to apply the small
+/-- The functor `Arrow C ⥤ Arrow C` that is constructed in order to apply the small
 object argument to a family of morphisms `f i : A i ⟶ B i`, see the introduction
 of the file `Mathlib.CategoryTheory.SmallObject.Construction` -/
 @[simps! obj map]
-noncomputable def functor : Over S ⥤ Over S where
-  obj π := Over.mk (πFunctorObj f π.hom)
-  map {π₁ π₂} φ := Over.homMk (functorMap f π₁.hom π₂.hom φ.left (Over.w φ))
-  map_id _ := by ext; dsimp; simp
-  map_comp {π₁ π₂ π₃} φ φ' := by
-    ext1
-    dsimp
-    ext ⟨i, t, b, w⟩
-    · simp
-    · simp [functorMap, ι_functorMapTgt_assoc f π₁.hom π₂.hom φ.left (Over.w φ) i t b w _ rfl,
-        ι_functorMapTgt_assoc f π₁.hom π₃.hom (φ.left ≫ φ'.left) (Over.w (φ ≫ φ')) i t b w _ rfl,
-        ι_functorMapTgt_assoc f π₂.hom π₃.hom (φ'.left) (Over.w φ') i (t ≫ φ.left) b
-          (by simp [w]) (t ≫ φ.left ≫ φ'.left) (by simp)]
-
-/-- The canonical natural transformation `𝟭 (Over S) ⟶ functor f S`. -/
-@[simps! app]
-noncomputable def ε : 𝟭 (Over S) ⟶ functor f S where
-  app w := Over.homMk (ιFunctorObj f w.hom)
+noncomputable def functor : Arrow C ⥤ Arrow C where
+  obj π := Arrow.mk (πFunctorObj f π.hom)
+  map {π₁ π₂} τ := Arrow.homMk (functorMap f τ) τ.right
+  map_id g := by
+    ext
+    · apply functorMap_id
+    · dsimp
+  map_comp {π₁ π₂ π₃} τ τ' := by
+    ext
+    · dsimp
+      simp [functorMap]
+      ext ⟨i, t, b, w⟩
+      · simp
+      · simp [ι_functorMapTgt_assoc f τ i t b w _ rfl _ rfl,
+          ι_functorMapTgt_assoc f (τ ≫ τ') i t b w _ rfl _ rfl,
+          ι_functorMapTgt_assoc f τ' i (t ≫ τ.left) (b ≫ τ.right)
+            (by simp [reassoc_of% w]) (b ≫ τ.right ≫ τ'.right) (by simp)
+            (t ≫ (τ ≫ τ').left) (by simp)]
+    · dsimp
+
+/-- The canonical natural transformation `𝟭 (Arrow C) ⟶ functor f`. -/
+@[simps app]
+noncomputable def ε : 𝟭 (Arrow C) ⟶ functor f where
+  app π := Arrow.homMk (ιFunctorObj f π.hom) (𝟙 _)
+
+end
 
 end SmallObject