chore(CategoryTheory): process porting notes, part 2 (#28776)

Go through all the porting notes in CategoryTheory, from Limits to Monoidal. Lots of them can be fixed, others are of the format "Lean 4 does this better" and a few are more TODOs which do not really depend on the port.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

@@ -136,9 +136,9 @@ theorem Types.isIso_colimitPointwiseProductToProductColimit (F : ∀ i, I i ⥤
     let yk' : (pointwiseProduct F).obj k :=
       (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
     obtain rfl : y = colimit.ι (pointwiseProduct F) k yk := by
-      simp only [k, yk, Types.Colimit.w_apply', hyk₀]
+      simp only [k, yk, Types.Colimit.w_apply, hyk₀]
     obtain rfl : y' = colimit.ι (pointwiseProduct F) k yk' := by
-      simp only [k, yk', Types.Colimit.w_apply', hyk₀']
+      simp only [k, yk', Types.Colimit.w_apply, hyk₀']
     dsimp only [pointwiseProduct_obj] at yk yk'
     have hch : ∀ (s : α), ∃ (i' : I s) (hi' : k s ⟶ i'),
         (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) =

Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean

@@ -182,23 +182,21 @@ instance functorCategoryHasColimitsOfShape [HasColimitsOfShape J C] :
     HasColimitsOfShape J (K ⥤ C) where
   has_colimit _ := inferInstance
 
--- Porting note: previously Lean could see through the binders and infer_instance sufficed
 instance functorCategoryHasLimitsOfSize [HasLimitsOfSize.{v₁, u₁} C] :
     HasLimitsOfSize.{v₁, u₁} (K ⥤ C) where
-  has_limits_of_shape := fun _ _ => inferInstance
+  has_limits_of_shape := inferInstance
 
--- Porting note: previously Lean could see through the binders and infer_instance sufficed
 instance functorCategoryHasColimitsOfSize [HasColimitsOfSize.{v₁, u₁} C] :
     HasColimitsOfSize.{v₁, u₁} (K ⥤ C) where
-  has_colimits_of_shape := fun _ _ => inferInstance
+  has_colimits_of_shape := inferInstance
 
 instance hasLimitCompEvaluation (F : J ⥤ K ⥤ C) (k : K) [HasLimit (F.flip.obj k)] :
     HasLimit (F ⋙ (evaluation _ _).obj k) :=
   hasLimit_of_iso (F := F.flip.obj k) (Iso.refl _)
 
 instance evaluation_preservesLimit (F : J ⥤ K ⥤ C) [∀ k, HasLimit (F.flip.obj k)] (k : K) :
     PreservesLimit F ((evaluation K C).obj k) :=
-    -- Porting note: added a let because X was not inferred
+  -- Porting note: added a let because X was not inferred
   let X : (k : K) → LimitCone (F.flip.obj k) := fun k => getLimitCone (F.flip.obj k)
   preservesLimit_of_preserves_limit_cone (combinedIsLimit _ X) <|
     IsLimit.ofIsoLimit (limit.isLimit _) (evaluateCombinedCones F X k).symm

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean

@@ -259,17 +259,22 @@ instance hasBiproduct_of_preserves : HasBiproduct (F.obj ∘ f) :=
     { bicone := F.mapBicone (biproduct.bicone f)
       isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }
 
+/-- This instance applies more often than `hasBiproduct_of_preserves`, but the discrimination
+tree key matches a lot more (since it does not look through lambdas). -/
+instance (priority := low) hasBiproduct_of_preserves' : HasBiproduct fun i => F.obj (f i) :=
+  HasBiproduct.mk
+    { bicone := F.mapBicone (biproduct.bicone f)
+      isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }
+
 /-- If `F` preserves a biproduct, we get a definitionally nice isomorphism
 `F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f)`. -/
 abbrev mapBiproduct : F.obj (⨁ f) ≅ ⨁ F.obj ∘ f :=
   biproduct.uniqueUpToIso _ (isBilimitOfPreserves _ (biproduct.isBilimit _))
 
 theorem mapBiproduct_hom :
-    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     (mapBiproduct F f).hom = biproduct.lift fun j => F.map (biproduct.π f j) := rfl
 
 theorem mapBiproduct_inv :
-    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     (mapBiproduct F f).inv = biproduct.desc fun j => F.map (biproduct.ι f j) := rfl
 
 end Bicone
@@ -364,16 +369,12 @@ section Bicone
 variable {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C}
 
 theorem biproduct.map_lift_mapBiprod (g : ∀ j, W ⟶ f j) :
-    -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F f
-    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     F.map (biproduct.lift g) ≫ (F.mapBiproduct f).hom = biproduct.lift fun j => F.map (g j) := by
   ext j
   dsimp only [Function.comp_def]
   simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]
 
 theorem biproduct.mapBiproduct_inv_map_desc (g : ∀ j, f j ⟶ W) :
-    -- Porting note: we need haveI to tell Lean about hasBiproduct_of_preserves F f
-    haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     (F.mapBiproduct f).inv ≫ F.map (biproduct.desc g) = biproduct.desc fun j => F.map (g j) := by
   ext j
   dsimp only [Function.comp_def]

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

@@ -232,10 +232,9 @@ lemma preservesPushout_symmetry : PreservesColimit (span g f) G where
     apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
     apply PushoutCocone.isColimitOfFlip
     apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
-    · refine @isColimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_ -- Porting note: more TC coddling
-      · exact PushoutCocone.flipIsColimit hc
-      · dsimp
-        infer_instance⟩
+    · -- Need to unfold these to allow the `PreservesColimit` instance to be found.
+      dsimp only [span_map_fst, span_map_snd]
+      exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)⟩
 
 theorem hasPushout_of_preservesPushout [HasPushout f g] : HasPushout (G.map f) (G.map g) :=
   ⟨⟨⟨_, isColimitPushoutCoconeMapOfIsColimit G _ (pushoutIsPushout _ _)⟩⟩⟩
@@ -312,8 +311,7 @@ lemma PreservesPushout.of_iso_comparison [i : IsIso (pushoutComparison G f g)] :
     PreservesColimit (span f g) G := by
   apply preservesColimit_of_preserves_colimit_cocone (pushoutIsPushout f g)
   apply (isColimitMapCoconePushoutCoconeEquiv _ _).symm _
-  -- Porting note: apply no longer creates goals for instances
-  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (span (G.map f) (G.map g))) i
+  exact IsColimit.ofPointIso _ (i := i)
 
 variable [PreservesColimit (span f g) G]
 

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

@@ -280,7 +280,7 @@ section
 
 attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
--- Porting note: would it be okay to use this more generally?
+-- TODO: would it be okay to use this more generally?
 attribute [local aesop safe cases (rule_sets := [CategoryTheory])] Eq
 
 /-- A binary fan with vertex `P` consists of the two projections `π₁ : P ⟶ X` and `π₂ : P ⟶ Y`. -/

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

@@ -75,7 +75,6 @@ open WalkingParallelPairHom
 
 /-- Composition of morphisms in the indexing diagram for (co)equalizers. -/
 def WalkingParallelPairHom.comp :
-    -- Porting note: changed X Y Z to implicit to match comp fields in precategory
     ∀ {X Y Z : WalkingParallelPair} (_ : WalkingParallelPairHom X Y)
       (_ : WalkingParallelPairHom Y Z), WalkingParallelPairHom X Z
   | _, _, _, id _, h => h
@@ -372,7 +371,6 @@ theorem Fork.IsLimit.lift_ι {s t : Fork f g} (hs : IsLimit s) : hs.lift t ≫ s
 theorem Cofork.IsColimit.π_desc {s t : Cofork f g} (hs : IsColimit s) : s.π ≫ hs.desc t = t.π :=
   hs.fac _ _
 
--- Porting note: `Fork.IsLimit.lift` was added in order to ease the port
 /-- If `s` is a limit fork over `f` and `g`, then a morphism `k : W ⟶ X` satisfying
 `k ≫ f = k ≫ g` induces a morphism `l : W ⟶ s.pt` such that `l ≫ fork.ι s = k`. -/
 def Fork.IsLimit.lift {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
@@ -393,7 +391,6 @@ def Fork.IsLimit.lift' {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h
 lemma Fork.IsLimit.mono {s : Fork f g} (hs : IsLimit s) : Mono s.ι where
   right_cancellation _ _ h := hom_ext hs h
 
--- Porting note: `Cofork.IsColimit.desc` was added in order to ease the port
 /-- If `s` is a colimit cofork over `f` and `g`, then a morphism `k : Y ⟶ W` satisfying
 `f ≫ k = g ≫ k` induces a morphism `l : s.pt ⟶ W` such that `cofork.π s ≫ l = k`. -/
 def Cofork.IsColimit.desc {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W)

Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

@@ -60,6 +60,9 @@ instance (priority := 90) hasFiniteLimits_of_hasLimitsOfSize₀ [HasLimitsOfSize
     HasFiniteLimits C :=
   hasFiniteLimits_of_hasLimitsOfSize C
 
+instance (J : Type) [hJ : SmallCategory J] : Category (ULiftHom (ULift J)) :=
+  (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
+
 /-- We can always derive `HasFiniteLimits C` by providing limits at an
 arbitrary universe. -/
 theorem hasFiniteLimits_of_hasFiniteLimits_of_size
@@ -71,12 +74,7 @@ theorem hasFiniteLimits_of_hasFiniteLimits_of_size
                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
       @ULiftHomULiftCategory.equiv J hJ
     apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
-      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
-      (@Equivalence.symm J hJ (ULiftHom (ULift J))
-      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
-    /- Porting note: tried to factor out (@instCategoryULiftHom (ULift J) (@uliftCategory J hJ)
-    but when doing that would then find the instance and say it was not definitionally equal to
-    the provided one (the same thing factored out) -/
+      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ l.symm _
 
 /-- A category has all finite colimits if every functor `J ⥤ C` with a `FinCategory J`
 instance and `J : Type` has a colimit.

Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean

@@ -61,8 +61,6 @@ class HasFiniteCoproducts : Prop where
   /-- `C` has all finite coproducts -/
   out (n : ℕ) : HasColimitsOfShape (Discrete (Fin n)) C
 
--- attribute [class] HasFiniteCoproducts Porting note: this doesn't seem necessary in Lean 4
-
 instance hasColimitsOfShape_discrete [HasFiniteCoproducts C] (ι : Type w) [Finite ι] :
     HasColimitsOfShape (Discrete ι) C := by
   rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -68,7 +68,7 @@ variable {X Y : C} (f : X ⟶ Y)
 
 /-- A factorisation of a morphism `f = e ≫ m`, with `m` monic. -/
 structure MonoFactorisation (f : X ⟶ Y) where
-  I : C -- Porting note: violates naming conventions but can't think a better replacement
+  I : C
   m : I ⟶ Y
   [m_mono : Mono m]
   e : X ⟶ I
@@ -221,7 +221,7 @@ variable (f)
 
 /-- Data exhibiting that a morphism `f` has an image. -/
 structure ImageFactorisation (f : X ⟶ Y) where
-  F : MonoFactorisation f -- Porting note: another violation of the naming convention
+  F : MonoFactorisation f
   isImage : IsImage F
 
 attribute [inherit_doc ImageFactorisation] ImageFactorisation.F ImageFactorisation.isImage
@@ -321,6 +321,18 @@ theorem IsImage.lift_ι {F : MonoFactorisation f} (hF : IsImage F) :
     hF.lift (Image.monoFactorisation f) ≫ image.ι f = F.m :=
   hF.lift_fac _
 
+@[reassoc (attr := simp)]
+theorem image.lift_mk_factorThruImage :
+    image.lift { I := image f, m := ι f, e := factorThruImage f } ≫ image.ι f = image.ι f :=
+  (Image.isImage f).lift_fac _
+
+@[reassoc (attr := simp)]
+theorem image.lift_mk_comp {C : Type u} [Category.{v} C] {X Y Z : C}
+    (f : X ⟶ Y) (g : Y ⟶ Z) [HasImage g] [HasImage (f ≫ g)]
+    (h : Y ⟶ image g) (H : (f ≫ h) ≫ image.ι g = f ≫ g) :
+    image.lift { I := image g, m := ι g, e := (f ≫ h) } ≫ image.ι g = image.ι (f ≫ g) :=
+  image.lift_fac _
+
 -- TODO we could put a category structure on `MonoFactorisation f`,
 -- with the morphisms being `g : I ⟶ I'` commuting with the `m`s
 -- (they then automatically commute with the `e`s)
@@ -441,23 +453,11 @@ def image.eqToHom (h : f = f') : image f ⟶ image f' :=
 instance (h : f = f') : IsIso (image.eqToHom h) :=
   ⟨⟨image.eqToHom h.symm,
       ⟨(cancel_mono (image.ι f)).1 (by
-          -- Porting note: added let's for used to be a simp [image.eqToHom]
-          let F : MonoFactorisation f' :=
-            ⟨image f, image.ι f, factorThruImage f, (by cat_disch)⟩
-          dsimp [image.eqToHom]
-          rw [Category.id_comp,Category.assoc,image.lift_fac F]
-          let F' : MonoFactorisation f :=
-            ⟨image f', image.ι f', factorThruImage f', (by cat_disch)⟩
-          rw [image.lift_fac F'] ),
+          subst h
+          simp [image.eqToHom, Category.assoc, Category.id_comp]),
         (cancel_mono (image.ι f')).1 (by
-          -- Porting note: added let's for used to be a simp [image.eqToHom]
-          let F' : MonoFactorisation f :=
-            ⟨image f', image.ι f', factorThruImage f', (by cat_disch)⟩
-          dsimp [image.eqToHom]
-          rw [Category.id_comp,Category.assoc,image.lift_fac F']
-          let F : MonoFactorisation f' :=
-            ⟨image f, image.ι f, factorThruImage f, (by cat_disch)⟩
-          rw [image.lift_fac F])⟩⟩⟩
+          subst h
+          simp [image.eqToHom])⟩⟩⟩
 
 /-- An equation between morphisms gives an isomorphism between the images. -/
 def image.eqToIso (h : f = f') : image f ≅ image f' :=
@@ -469,8 +469,8 @@ the image inclusion maps commute with `image.eqToIso`.
 theorem image.eq_fac [HasEqualizers C] (h : f = f') :
     image.ι f = (image.eqToIso h).hom ≫ image.ι f' := by
   apply image.ext
-  dsimp [asIso,image.eqToIso, image.eqToHom]
-  rw [image.lift_fac] -- Porting note: simp did not fire with this it seems
+  subst h
+  simp [asIso,image.eqToIso, image.eqToHom]
 
 end
 
@@ -488,8 +488,7 @@ def image.preComp [HasImage g] [HasImage (f ≫ g)] : image (f ≫ g) ⟶ image
 @[reassoc (attr := simp)]
 theorem image.preComp_ι [HasImage g] [HasImage (f ≫ g)] :
     image.preComp f g ≫ image.ι g = image.ι (f ≫ g) := by
-      dsimp [image.preComp]
-      rw [image.lift_fac] -- Porting note: also here, see image.eq_fac
+      simp [image.preComp]
 
 @[reassoc (attr := simp)]
 theorem image.factorThruImage_preComp [HasImage g] [HasImage (f ≫ g)] :
@@ -512,9 +511,8 @@ theorem image.preComp_comp {W : C} (h : Z ⟶ W) [HasImage (g ≫ h)] [HasImage
     image.preComp f (g ≫ h) ≫ image.preComp g h =
       image.eqToHom (Category.assoc f g h).symm ≫ image.preComp (f ≫ g) h := by
   apply (cancel_mono (image.ι h)).1
-  dsimp [image.preComp, image.eqToHom]
-  repeat (rw [Category.assoc,image.lift_fac])
-  rw [image.lift_fac,image.lift_fac]
+  simp only [preComp, Category.assoc, fac, lift_mk_comp, eqToHom]
+  rw [image.lift_fac]
 
 variable [HasEqualizers C]
 
@@ -673,8 +671,6 @@ section
 
 attribute [local ext] ImageMap
 
-/- Porting note: ImageMap.mk.injEq has LHS simplify to True due to the next instance
-We make a replacement -/
 theorem ImageMap.map_uniq_aux {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g}
     (map : image f.hom ⟶ image g.hom)
     (map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right := by cat_disch)
@@ -683,11 +679,11 @@ theorem ImageMap.map_uniq_aux {f g : Arrow C} [HasImage f.hom] [HasImage g.hom]
   have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι,map_ι']
   apply (cancel_mono (image.ι g.hom)).1 this
 
--- Porting note: added to get variant on ImageMap.mk.injEq below
 theorem ImageMap.map_uniq {f g : Arrow C} [HasImage f.hom] [HasImage g.hom]
     {sq : f ⟶ g} (F G : ImageMap sq) : F.map = G.map := by
   apply ImageMap.map_uniq_aux _ F.map_ι _ G.map_ι
 
+/-- `@[simp]`-normal form of `ImageMap.mk.injEq`. -/
 @[simp]
 theorem ImageMap.mk.injEq' {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g}
     (map : image f.hom ⟶ image g.hom)

Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

@@ -396,10 +396,7 @@ def coconeOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) : Cocone F
 def colimitOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) :
     IsColimit (coconeOfDiagramTerminal tX F) where
   desc s := s.ι.app X
-  uniq s m w := by
-    conv_rhs => dsimp -- Porting note: why do I need this much firepower?
-    rw [← w X, coconeOfDiagramTerminal_ι_app, tX.hom_ext (tX.from X) (𝟙 _)]
-    simp
+  uniq s m w := by simp [← w X]
 
 lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
     (X : J) (hX : IsTerminal X) :