chore: bump to 4.28.0-rc1

HoTTLean/ForMathlib.lean

@@ -1,10 +1,11 @@
+import Mathlib.Tactic.DepRewrite
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
 import Mathlib.CategoryTheory.Groupoid.Discrete
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.Logic.Function.ULift
 import Mathlib.CategoryTheory.Category.Cat
-import Mathlib.CategoryTheory.Category.Grpd
+import Mathlib.CategoryTheory.Groupoid.Grpd.Basic
 import Mathlib.Data.Part
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Core
@@ -101,29 +102,29 @@ namespace CategoryTheory.Cat
 
 /-- This is the proof of equality used in the eqToHom in `Cat.eqToHom_hom` -/
 theorem eqToHom_hom_aux {C1 C2 : Cat.{v,u}} (x y: C1) (eq : C1 = C2) :
-    (x ⟶ y) = ((eqToHom eq).obj x ⟶ (eqToHom eq).obj y) := by
+    (x ⟶ y) = ((eqToHom eq).toFunctor.obj x ⟶ (eqToHom eq).toFunctor.obj y) := by
   cases eq
   simp[CategoryStruct.id]
 
 /-- This is the turns the hom part of eqToHom functors into a cast-/
 theorem eqToHom_hom {C1 C2 : Cat.{v,u}} {x y: C1} (f : x ⟶ y) (eq : C1 = C2) :
-    (eqToHom eq).map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by
+    (eqToHom eq).toFunctor.map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by
   cases eq
   simp[CategoryStruct.id]
 
 /-- This turns the object part of eqToHom functors into casts -/
 theorem eqToHom_obj {C1 C2 : Cat.{v,u}} (x : C1) (eq : C1 = C2) :
-    (eqToHom eq).obj x = cast (congrArg Bundled.α eq) x := by
+    (eqToHom eq).toFunctor.obj x = cast (congrArg Bundled.α eq) x := by
   cases eq
   simp[CategoryStruct.id]
 
 abbrev homOf {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) :
-    Cat.of C ⟶ Cat.of D := F
+    Cat.of C ⟶ Cat.of D := ⟨F⟩
 
 @[simps] def ULift_lte_iso_self {C : Type (max u u₁)} [Category.{v} C] :
     Cat.of (ULift.{u} C) ≅ Cat.of C where
-  hom := ULift.downFunctor
-  inv := ULift.upFunctor
+  hom := homOf ULift.downFunctor
+  inv := homOf ULift.upFunctor
 
 @[simp] def ULift_succ_iso_self {C : Type (u + 1)} [Category.{v} C] :
     of (ULift.{u, u + 1} C) ≅ of C := ULift_lte_iso_self.{v,u,u+1}
@@ -135,8 +136,8 @@ def ofULift (C : Type u) [Category.{v} C] : Cat.{v, max u w} :=
   of $ ULift.{w} C
 
 def uLiftFunctor : Cat.{v,u} ⥤ Cat.{v, max u w} where
-  obj X := Cat.ofULift.{w} X
-  map F := Cat.homOf $ ULift.downFunctor ⋙ F ⋙ ULift.upFunctor
+  obj X := ofULift.{w} X
+  map F := homOf $ ULift.downFunctor ⋙ F.toFunctor ⋙ ULift.upFunctor
 
 end CategoryTheory.Cat
 
@@ -401,16 +402,15 @@ variable {Γ : Type u₂} [Category.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
 
 @[simp] theorem Cat.map_id_obj {A : Γ ⥤ Cat.{v₁,u₁}}
     {x : Γ} {a : A.obj x} :
-    (A.map (𝟙 x)).obj a = a := by
-  have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp
-  exact Functor.congr_obj this a
+    (A.map (𝟙 x)).toFunctor.obj a = a := by
+  simp
 
 theorem Cat.map_id_map {A : Γ ⥤ Cat.{v₁,u₁}}
     {x : Γ} {a b : A.obj x} {f : a ⟶ b} :
-    (A.map (𝟙 x)).map f = eqToHom Cat.map_id_obj
+    (A.map (𝟙 x)).toFunctor.map f = eqToHom Cat.map_id_obj
       ≫ f ≫ eqToHom Cat.map_id_obj.symm := by
-  have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp
-  exact Functor.congr_hom this f
+  rw! [show A.map (𝟙 x) = 𝟙 (A.obj x) by simp]
+  simp
 
 end
 
@@ -624,14 +624,6 @@ lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
     cases h
     simp
 
-lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C)
-    (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) :
-    F = G :=
-  calc F
-    _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq
-    _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h
-    _ = G := Discrete.functor_eq.symm
-
 lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)
     (hab : a.1 ≍ b.1) : a ≍ b := by
   aesop_cat

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -60,8 +60,6 @@ variable (F : Pseudofunctor B Cat) {a b : B}
     (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ :=
   LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩
 
-attribute [reassoc] StrongTrans.naturality_comp_inv_app
-
 end
 
 lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat)

HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Hua
 -/
 import Mathlib.CategoryTheory.Groupoid.FreeGroupoid
-import Mathlib.CategoryTheory.Category.Grpd
+import Mathlib.CategoryTheory.Groupoid.Grpd.Basic
 import Mathlib.CategoryTheory.Adjunction.Reflective
 import Mathlib.CategoryTheory.Localization.Predicate
 import Mathlib.CategoryTheory.Monad.Limits
 import Mathlib.CategoryTheory.Category.Cat.Limit
 
-import HoTTLean.ForMathlib.CategoryTheory.Localization.Predicate
-
 /-!
 # Free groupoid on a category
 
@@ -190,15 +188,15 @@ open Category.FreeGroupoid
 @[simps]
 def free : Cat.{u,u} ⥤ Grpd.{u,u} where
   obj C := Grpd.of <| Category.FreeGroupoid C
-  map {C D} F := map F
-  map_id C := by simp [Grpd.id_eq_id, ← map_id]; rfl
-  map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]; rfl
+  map {C D} F := map F.toFunctor
+  map_id C := by simp [Grpd.id_eq_id, ← map_id]
+  map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]
 
 /-- The unit of the free-forgetful adjunction between `Grpd` and `Cat`. -/
 @[simps]
 def freeForgetAdjunction.unit : 𝟭 Cat ⟶ free ⋙ forgetToCat where
-  app C := Category.FreeGroupoid.of C
-  naturality C D F := by simp [forgetToCat, Cat.comp_eq_comp, map, lift_spec]
+  app C := ⟨Category.FreeGroupoid.of C⟩
+  naturality C D F := by ext; simp [forgetToCat, map, lift_spec]
 
 /-- The counit of the free-forgetful adjunction between `Grpd` and `Cat`. -/
 @[simps]
@@ -218,7 +216,7 @@ def freeForgetAdjunction : free ⊣ Grpd.forgetToCat where
     apply lift_unique
     simp [Functor.assoc, lift_spec, Grpd.id_eq_id]
   right_triangle_components G := by
-    simp [forgetToCat, Cat.comp_eq_comp, lift_spec, Cat.id_eq_id]
+    ext; simp [forgetToCat, lift_spec]
 
 instance : Reflective Grpd.forgetToCat where
   L := free

HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean

@@ -1,6 +1,5 @@
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Functor.TwoSquare
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 import HoTTLean.ForMathlib
 
 universe w v u v₁ u₁ v₂ u₂ v₃ u₃

HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean

@@ -1,7 +1,7 @@
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import HoTTLean.ForMathlib.CategoryTheory.WeakPullback
 
 /-!

HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean

@@ -56,24 +56,24 @@ def functorMapExpr (e : Expr) (lvl_params : Bool) : MetaM (Expr × List Level) :
     let some (hom, _, _) := eTp.eq? | throwError "expected an equality, got{indentD eTp}"
     if !hom.isAppOf ``Quiver.Hom then
       throwError "expected an equality of morphisms, got{indentD eTp}"
-    let [.succ v₁, u₁] := hom.getAppFn.constLevels! |
+    let [v₁, u₁] := hom.getAppFn.constLevels! |
       throwError "unexpected universe levels in{indentD hom.getAppFn}"
     let e' ← mkAppM' (.const ``eq_functor_map [v₁, u₁, v₂, u₂]) #[e]
     simpType categorySimp' e'
   return (e, [v₂, u₂])
 
-syntax (name := functor_map) "functor_map" (" (" &"attr" ":=" Parser.Term.attrInstance,* ")")? : attr
+syntax (name := functor_map) "functor_map" optAttrArg : attr
 
 initialize registerBuiltinAttribute {
   name := `functor_map
   descr := ""
   applicationTime := .afterCompilation
   add := fun src ref kind => match ref with
-  | `(attr| functor_map $[(attr := $stx?,*)]?) => MetaM.run' do
+  | `(attr| functor_map $stx?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`functor_map` can only be used as a global attribute"
-    addRelatedDecl src "_functor_map" ref stx? fun type value levels => do
-      let (e, levels') ← functorMapExpr (← mkExpectedTypeHint value type) true
+    addRelatedDecl src (src.appendAfter "_functor_map") ref stx? fun value levels => do
+      let (e, levels') ← functorMapExpr value true
       pure (e, levels ++ levels'.map fun | .param n => n | _ => panic! "")
   | _ => throwUnsupportedSyntax }
 

HoTTLean/ForPoly.lean

@@ -256,8 +256,8 @@ theorem fan_snd_map' {E B E' B' : C} {P : UvPoly E B} {P' : UvPoly E' B'}
   slice_lhs 1 2 => rw [← this]
   slice_lhs 2 3 => apply Category.comp_id
   simp [α, Over.starPullbackIsoStar]
-  slice_lhs 5 6 => apply pullback.lift_fst
-  simp [Over.mapForget]
+  slice_lhs 4 5 => apply pullback.lift_fst
+  simp
 
 open ExponentiableMorphism in
 theorem fan_snd_map {E B A E' B' A' : C} {P : UvPoly E B} {P' : UvPoly E' B'}

HoTTLean/Model/Natural/NaturalModel.lean

@@ -267,6 +267,7 @@ lemma snd_mk (A : y(Γ) ⟶ M.Ty) (B : y(M.ext A) ⟶ X) :
     snd M (mk M A B) _ (fst_mk ..) = B := by
   dsimp only [snd, mk]
   rw! [UvPoly.Equiv.snd'_mk']
+  rfl
 
 section
 variable {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : y(Γ) ⟶ M.Ptp.obj X}
@@ -1152,7 +1153,7 @@ lemma comp_j : ym(ii.motiveSubst σ _) ≫ j i a C r r_tp =
     j i (ym(σ) ≫ a) (ym(ii.motiveSubst σ _) ≫ C) (ym(σ) ≫ r) (by
       simp [r_tp, IdIntro.comp_reflSubst'_assoc]) := by
   simp only [j]
-  conv => rhs; rw! [i.lift_comp_left a C r r_tp]
+  rw! [i.lift_comp_left a C r r_tp]
   rw [ie.equivSnd_comp_left]
   simp only [← Category.assoc]
   congr 1

HoTTLean/Model/Unstructured/Interpretation.lean

@@ -1152,7 +1152,7 @@ theorem EqTmIH.idRec_refl {Γ A M t r l l'} :
     have sr := rtp ▸ Part.mem_unique hR sM
     have ir := I.mem_ofTerm_idRec.2 ⟨_, _, ht, _, ttp, B, by simp [Beq, sAeq],
       _, hM, _, hr, by simp [ttp, sr], _, ht, ttp, _, h1, by simp [ttp],
-        by rw! [ttp, PolymorphicIdElim.idRec_refl (I_eq := _)]⟩
+        by rw! [ttp, PolymorphicIdElim.idRec_refl (I_eq := _)]; rfl⟩
     ⟨_, hΓ, _, _, sM, _, ir, hr, sr⟩
   simp [Beq, ← Id_comp, sAeq, ttp]
 

HoTTLean/Model/Unstructured/UnstructuredUniverse.lean

@@ -320,12 +320,14 @@ lemma fst_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.ex
     S.fst (U0.substWk σ A σA eq ≫ B) (σ ≫ s) (by simp [s_tp, S.Sig_comp]) =
     σ ≫ S.fst B s s_tp := by
   rw! [(S.pair_fst_snd B s (by simp [s_tp])).symm, ← S.pair_comp, S.fst_pair, S.fst_pair]
+  rfl
 
 lemma snd_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.ext A ⟶ U1.Ty}
     (s : Γ ⟶ U2.Tm) (s_tp : s ≫ U2.tp = S.Sig B) :
     S.snd (U0.substWk σ A σA eq ≫ B) (σ ≫ s) (by simp [s_tp, S.Sig_comp]) =
     σ ≫ S.snd B s s_tp := by
   rw! [(S.pair_fst_snd B s (by simp [s_tp])).symm, ← S.pair_comp, S.snd_pair, S.snd_pair]
+  rfl
 
 end PolymorphicSigma
 
@@ -362,7 +364,7 @@ lemma unLam_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.
     P.unLam (U0.substWk σ A σA eq ≫ B) (σ ≫ f) (by simp [f_tp, P.Pi_comp]) =
     U0.substWk σ A σA eq ≫ P.unLam B f f_tp := by
   rw [← P.unLam_lam (U0.substWk σ A σA eq ≫ B) (U0.substWk σ A σA eq ≫ P.unLam B f f_tp)]
-  . rw! [P.lam_comp σ eq B, P.lam_unLam]
+  . rw! [P.lam_comp σ eq B, P.lam_unLam]; rfl
   . rw [Category.assoc, P.unLam_tp]
 
 /--

HoTTLean/Syntax/Axioms.lean

@@ -29,7 +29,7 @@ open Classical
 instance : LE (Axioms χ) where
   le E E' := ∀ ⦃c p⦄, (E c) = some p → (E' c) = some p
 
-instance : IsRefl (Axioms χ) (· ≤ ·) where
+instance : @Std.Refl (Axioms χ) (· ≤ ·) where
   refl _ _ _ := id
 
 instance : IsTrans (Axioms χ) (· ≤ ·) where