merge

Cache/Requests.lean

@@ -28,7 +28,9 @@ section Get
 
 /-- Formats the config file for `curl`, containing the list of files to be downloaded -/
 def mkGetConfigContent (hashMap : IO.HashMap) : IO String := do
-  hashMap.foldM (init := "") fun acc _ hash => do
+  -- We sort the list so that the large files in `MathlibExtras` are requested first.
+  hashMap.toArray.qsort (fun ⟨p₁, _⟩ ⟨_, _⟩ => p₁.components.head? = "MathlibExtras")
+    |>.foldlM (init := "") fun acc ⟨_, hash⟩ => do
     let fileName := hash.asTarGz
     -- Below we use `String.quote`, which is intended for quoting for use in Lean code
     -- this does not exactly match the requirements for quoting for curl:

Mathlib/CategoryTheory/Adjunction/Comma.lean

@@ -145,16 +145,14 @@ section
 
 variable {F : C ⥤ D}
 
--- porting note: aesop can't seem to add something locally. Also no tactic.discrete_cases.
--- attribute [local tidy] tactic.discrete_cases
+attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
 
 /-- Given a left adjoint to `G`, we can construct an initial object in each structured arrow
 category on `G`. -/
 def mkInitialOfLeftAdjoint (h : F ⊣ G) (A : C) :
     IsInitial (StructuredArrow.mk (h.unit.app A) : StructuredArrow A G)
     where
   desc B := StructuredArrow.homMk ((h.homEquiv _ _).symm B.pt.hom)
-  fac _ := by rintro ⟨⟨⟩⟩
   uniq s m _ := by
     apply StructuredArrow.ext
     dsimp
@@ -168,7 +166,6 @@ def mkTerminalOfRightAdjoint (h : F ⊣ G) (A : D) :
     IsTerminal (CostructuredArrow.mk (h.counit.app A) : CostructuredArrow F A)
     where
   lift B := CostructuredArrow.homMk (h.homEquiv _ _ B.pt.hom)
-  fac _ := by rintro ⟨⟨⟩⟩
   uniq s m _ := by
     apply CostructuredArrow.ext
     dsimp

Mathlib/CategoryTheory/Category/Grpd.lean

@@ -117,8 +117,6 @@ set_option linter.uppercaseLean3 false in
 
 section Products
 
---attribute [local tidy] tactic.discrete_cases
-
 /-- Construct the product over an indexed family of groupoids, as a fan. -/
 def piLimitFan ⦃J : Type u⦄ (F : J → Grpd.{u, u}) : Limits.Fan F :=
   Limits.Fan.mk (@of (∀ j : J, F j) _) fun j => CategoryTheory.Pi.eval _ j

Mathlib/CategoryTheory/DiscreteCategory.lean

@@ -50,8 +50,7 @@ with the only morphisms being equalities.
 @[ext]
 structure Discrete (α : Type u₁) where
   /-- A wrapper for promoting any type to a category,
-  with the only morphisms being equalities.
-  -/
+  with the only morphisms being equalities. -/
   as : α
 #align category_theory.discrete CategoryTheory.Discrete
 
@@ -99,31 +98,36 @@ instance [Inhabited α] : Inhabited (Discrete α) :=
   ⟨⟨default⟩⟩
 
 instance [Subsingleton α] : Subsingleton (Discrete α) :=
-  ⟨by
-    intros
-    ext
-    apply Subsingleton.elim⟩
+  ⟨by aesop_cat⟩
 
 instance instSubsingletonDiscreteHom (X Y : Discrete α) : Subsingleton (X ⟶ Y) :=
   show Subsingleton (ULift (PLift _)) from inferInstance
 
-/-
-Porting note: It seems that `aesop` currently has no way to add lemmas locally.
-
-attribute [local tidy] tactic.discrete_cases
-`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), PLift _]]
--/
-
 /- Porting note: rewrote `discrete_cases` tactic -/
-/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
+/-- A simple tactic to run `cases` on any `Discrete α` hypotheses. -/
 macro "discrete_cases" : tactic =>
   `(tactic| fail_if_no_progress casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 
 open Lean Elab Tactic in
-/-- Wrapper for `discrete_cases` so `aesop_cat` can call it. -/
+/--
+Use:
+```
+attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+  CategoryTheory.Discrete.discreteCases
+```
+to locally gives `aesop_cat` the ability to call `cases` on
+`Discrete` and `(_ : Discrete _) ⟶ (_ : Discrete _)` hypotheses.
+-/
 def discreteCases : TacticM Unit := do
   evalTactic (← `(tactic| discrete_cases))
 
+-- Porting note:
+-- investigate turning on either
+-- `attribute [aesop safe cases (rule_sets [CategoryTheory])] Discrete`
+-- or
+-- `attribute [aesop safe tactic (rule_sets [CategoryTheory])] discreteCases`
+-- globally.
+
 instance [Unique α] : Unique (Discrete α) :=
   Unique.mk' (Discrete α)
 
@@ -135,19 +139,13 @@ theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
 /-- Promote an equation between the wrapped terms in `X Y : Discrete α` to a morphism `X ⟶ Y`
 in the discrete category. -/
 protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
-  eqToHom
-    (by
-      ext
-      exact h)
+  eqToHom (by aesop_cat)
 #align category_theory.discrete.eq_to_hom CategoryTheory.Discrete.eqToHom
 
 /-- Promote an equation between the wrapped terms in `X Y : Discrete α` to an isomorphism `X ≅ Y`
 in the discrete category. -/
 protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
-  eqToIso
-    (by
-      ext
-      exact h)
+  eqToIso (by aesop_cat)
 #align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso
 
 /-- A variant of `eqToHom` that lifts terms to the discrete category. -/
@@ -170,16 +168,16 @@ variable {C : Type u₂} [Category.{v₂} C]
 instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
   ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩
 
+attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+  CategoryTheory.Discrete.discreteCases
+
 /-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/
 def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where
   obj := F ∘ Discrete.as
   map {X Y} f := by
     dsimp
     rcases f with ⟨⟨h⟩⟩
     exact eqToHom (congrArg _ h)
-  map_comp := fun {X Y Z} f g => by
-    discrete_cases
-    aesop_cat
 #align category_theory.discrete.functor CategoryTheory.Discrete.functor
 
 @[simp]
@@ -206,8 +204,8 @@ a natural transformation is just a collection of maps,
 as the naturality squares are trivial.
 -/
 @[simps]
-def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G
-    where
+def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) :
+    F ⟶ G where
   app := f
   naturality := fun {X Y} ⟨⟨g⟩⟩ => by
     discrete_cases
@@ -221,7 +219,8 @@ a natural isomorphism is just a collection of isomorphisms,
 as the naturality squares are trivial.
 -/
 @[simps!]
-def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G :=
+def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) :
+    F ≅ G :=
   NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by
     discrete_cases
     rcases g
@@ -256,17 +255,9 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D
   functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
   inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
   unitIso :=
-    Discrete.natIso fun i =>
-      eqToIso
-        (by
-          discrete_cases
-          simp)
+    Discrete.natIso fun i => eqToIso (by aesop_cat)
   counitIso :=
-    Discrete.natIso fun j =>
-      eqToIso
-        (by
-          discrete_cases
-          simp)
+    Discrete.natIso fun j => eqToIso (by aesop_cat)
 #align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence
 
 /-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
@@ -291,8 +282,8 @@ open Opposite
 protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α :=
   let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
   Equivalence.mk F.leftOp F
-    (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _))
-    (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _)
+  (NatIso.ofComponents fun ⟨X⟩ => Iso.refl _)
+  (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _)
 
 #align category_theory.discrete.opposite CategoryTheory.Discrete.opposite
 
@@ -301,9 +292,7 @@ variable {C : Type u₂} [Category.{v₂} C]
 @[simp]
 theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) :
     F.map f = 𝟙 (F.obj j) := by
-  have h : f = 𝟙 j := by
-    rcases f with ⟨⟨f⟩⟩
-    rfl
+  have h : f = 𝟙 j := by aesop_cat
   rw [h]
   simp
 #align category_theory.discrete.functor_map_id CategoryTheory.Discrete.functor_map_id

Mathlib/CategoryTheory/GradedObject.lean

@@ -196,18 +196,13 @@ variable [HasCoproducts.{0} C]
 
 section
 
---attribute [local tidy] tactic.discrete_cases
+attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
 
 /-- The total object of a graded object is the coproduct of the graded components.
 -/
 noncomputable def total : GradedObject β C ⥤ C where
   obj X := ∐ fun i : β => X i
   map f := Limits.Sigma.map fun i => f i
-  map_id := fun X => by
-    dsimp
-    ext
-    simp only [ι_colimMap, Discrete.natTrans_app, Category.comp_id]
-    apply Category.id_comp
 #align category_theory.graded_object.total CategoryTheory.GradedObject.total
 
 end

Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

@@ -76,7 +76,9 @@ def conesEquivInverse (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
           rfl }
 #align category_theory.over.construct_products.cones_equiv_inverse CategoryTheory.Over.ConstructProducts.conesEquivInverse
 
---attribute [local tidy] tactic.discrete_cases -- Porting note: no tidy
+-- Porting note: this should help with the additional `naturality` proof we now have to give in
+-- `conesEquivFunctor`, but doesn't.
+-- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simps]
@@ -91,7 +93,10 @@ def conesEquivFunctor (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
   map f := { Hom := Over.homMk f.Hom }
 #align category_theory.over.construct_products.cones_equiv_functor CategoryTheory.Over.ConstructProducts.conesEquivFunctor
 
---attribute [local tidy] tactic.case_bash -- Porting note: no tidy
+-- Porting note: unfortunately `aesop` can't cope with a `cases` rule here for the type synonym
+-- `WidePullbackShape`.
+-- attribute [local aesop safe cases (rule_sets [CategoryTheory])] WidePullbackShape
+-- If this worked we could avoid the `rintro` in `conesEquivUnitIso`.
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simp]
@@ -104,6 +109,8 @@ def conesEquivUnitIso (B : C) (F : Discrete J ⥤ Over B) :
     (by rintro (j | j) <;> aesop_cat)
 #align category_theory.over.construct_products.cones_equiv_unit_iso CategoryTheory.Over.ConstructProducts.conesEquivUnitIso
 
+-- TODO: Can we add `:= by aesop` to the second arguments of `NatIso.ofComponents` and
+--       `Cones.ext`?
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simp]
 def conesEquivCounitIso (B : C) (F : Discrete J ⥤ Over B) :
@@ -158,7 +165,7 @@ theorem over_finiteProducts_of_finiteWidePullbacks [HasFiniteWidePullbacks C] {B
 
 end ConstructProducts
 
---attribute [local tidy] tactic.discrete_cases -- Porting note: no tidy
+attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
 
 /-- Construct terminal object in the over category. This isn't an instance as it's not typically the
 way we want to define terminal objects.
@@ -170,17 +177,14 @@ theorem over_hasTerminal (B : C) : HasTerminal (Over B) where
     { cone :=
         { pt := Over.mk (𝟙 _)
           π :=
-            { app := fun p => p.as.elim
-              -- Porting note: Added a proof for `naturality`
-              naturality := fun X => X.as.elim } }
+            { app := fun p => p.as.elim } }
       isLimit :=
         { lift := fun s => Over.homMk _
           fac := fun _ j => j.as.elim
           uniq := fun s m _ => by
             simp only
             ext
-            -- Porting note: Added a proof to `Over.homMk_left`
-            rw [Over.homMk_left _ (by dsimp; rw [Category.comp_id])]
+            rw [Over.homMk_left _]
             have := m.w
             dsimp at this
             rwa [Category.comp_id, Category.comp_id] at this } }

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

@@ -150,13 +150,14 @@ section
 variable {F G : Discrete WalkingPair ⥤ C} (f : F.obj ⟨left⟩ ⟶ G.obj ⟨left⟩)
   (g : F.obj ⟨right⟩ ⟶ G.obj ⟨right⟩)
 
--- attribute [local tidy] tactic.discrete_cases Porting note: no more local, no more tidy
+attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+  CategoryTheory.Discrete.discreteCases
 
 /-- The natural transformation between two functors out of the
  walking pair, specified by its components. -/
 def mapPair : F ⟶ G where
   app j := Discrete.recOn j fun j => WalkingPair.casesOn j f g
-  naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by dsimp at u; cases u; simp
+  naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by aesop_cat
 #align category_theory.limits.map_pair CategoryTheory.Limits.mapPair
 
 @[simp]
@@ -174,7 +175,7 @@ components. -/
 @[simps!]
 def mapPairIso (f : F.obj ⟨left⟩ ≅ G.obj ⟨left⟩) (g : F.obj ⟨right⟩ ≅ G.obj ⟨right⟩) : F ≅ G :=
   NatIso.ofComponents (fun j => Discrete.recOn j fun j => WalkingPair.casesOn j f g)
-    (fun {X} {Y} ⟨⟨u⟩⟩ => by dsimp; cases X; cases Y; cases u; simp)
+    (fun ⟨⟨u⟩⟩ => by aesop_cat)
 #align category_theory.limits.map_pair_iso CategoryTheory.Limits.mapPairIso
 
 end
@@ -292,26 +293,25 @@ variable {X Y : C}
 
 section
 
--- attribute [local tidy] tactic.discrete_cases Porting note: no local, no tidy
+attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+  CategoryTheory.Discrete.discreteCases
+-- Porting note: 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`. -/
 @[simps pt]
 def BinaryFan.mk {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : BinaryFan X Y where
   pt := P
   π :=
-    -- Porting removed use of casesOn to preserve computability
-    { app := fun ⟨j⟩ => by cases j <;> simpa
-      naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by cases u; simp }
+    { app := fun ⟨j⟩ => by cases j <;> simpa }
 #align category_theory.limits.binary_fan.mk CategoryTheory.Limits.BinaryFan.mk
 
 /-- A binary cofan with vertex `P` consists of the two inclusions `ι₁ : X ⟶ P` and `ι₂ : Y ⟶ P`. -/
 @[simps pt]
 def BinaryCofan.mk {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : BinaryCofan X Y where
   pt := P
   ι :=
-    -- Porting removed use of casesOn to preserve computability
-    { app := fun ⟨j⟩ => by cases j <;> simpa
-      naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by cases u; simp }
+    { app := fun ⟨j⟩ => by cases j <;> simpa }
 #align category_theory.limits.binary_cofan.mk CategoryTheory.Limits.BinaryCofan.mk
 
 end

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -97,13 +97,15 @@ variable {F : J → C}
 
 namespace Bicone
 
--- attribute [local tidy] tactic.discrete_cases Porting note: removed
+attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+  CategoryTheory.Discrete.discreteCases
+-- Porting note: would it be okay to use this more generally?
+attribute [local aesop safe cases (rule_sets [CategoryTheory])] Eq
 
 /-- Extract the cone from a bicone. -/
 def toCone (B : Bicone F) : Cone (Discrete.functor F) where
   pt := B.pt
-  π := { app := fun j => B.π j.as
-         naturality := by intro ⟨j⟩ ⟨j'⟩ ⟨⟨f⟩⟩; cases f; simp}
+  π := { app := fun j => B.π j.as }
 #align category_theory.limits.bicone.to_cone CategoryTheory.Limits.Bicone.toCone
 
 @[simp]
@@ -206,15 +208,13 @@ def whisker {f : J → C} (c : Bicone f) (g : K ≃ J) : Bicone (f ∘ g) where
     split_ifs with h h' h' <;> simp [Equiv.apply_eq_iff_eq g] at h h' <;> tauto
 #align category_theory.limits.bicone.whisker CategoryTheory.Limits.Bicone.whisker
 
--- attribute [local tidy] tactic.discrete_cases Porting note: removed
-
 /-- Taking the cone of a whiskered bicone results in a cone isomorphic to one gained
 by whiskering the cone and postcomposing with a suitable isomorphism. -/
 def whiskerToCone {f : J → C} (c : Bicone f) (g : K ≃ J) :
     (c.whisker g).toCone ≅
       (Cones.postcompose (Discrete.functorComp f g).inv).obj
         (c.toCone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
-  Cones.ext (Iso.refl _) (by intro ⟨j⟩; simp)
+  Cones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.bicone.whisker_to_cone CategoryTheory.Limits.Bicone.whiskerToCone
 
 /-- Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained
@@ -223,7 +223,7 @@ def whiskerToCocone {f : J → C} (c : Bicone f) (g : K ≃ J) :
     (c.whisker g).toCocone ≅
       (Cocones.precompose (Discrete.functorComp f g).hom).obj
         (c.toCocone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
-  Cocones.ext (Iso.refl _) (by intro ⟨j⟩; simp)
+  Cocones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.bicone.whisker_to_cocone CategoryTheory.Limits.Bicone.whiskerToCocone
 
 /-- Whiskering a bicone with an equivalence between types preserves being a bilimit bicone. -/