diff --git a/HoTTLean/ForMathlib.lean b/HoTTLean/ForMathlib.lean
index 0d1cd8c9..af5a7bd2 100644
--- a/HoTTLean/ForMathlib.lean
+++ b/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
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean b/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean
index 3f256088..05b5a28d 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean
+++ b/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)
diff --git a/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean b/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean
index e853e0c4..8c6c9147 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean
+++ b/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
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean b/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean
deleted file mode 100644
index 0f73aff6..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.CategoryTheory.Groupoid
-import Mathlib.CategoryTheory.MorphismProperty.Basic
-
-namespace CategoryTheory
-
-open MorphismProperty in
-lemma isGroupoid_iff_isomorphisms_eq_top (C : Type*) [Category C] :
-    IsGroupoid C ↔ isomorphisms C = ⊤ := by
-  constructor
-  · rw [eq_top_iff]
-    intro _ _
-    simp only [isomorphisms.iff, top_apply]
-    infer_instance
-  · intro h
-    exact ⟨of_eq_top h⟩
-
-end CategoryTheory
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean b/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean
deleted file mode 100644
index 70dc3771..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-import Mathlib.CategoryTheory.Localization.Predicate
-
-import HoTTLean.ForMathlib.CategoryTheory.Groupoid
-import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.Basic
-
-noncomputable section
-
-namespace CategoryTheory.Localization
-open Category Functor
-
-variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) (W : MorphismProperty C) (E : Type*)
-  [Category E]
-
-variable {D₁ D₂ : Type _} [Category D₁] [Category D₂] (L₁ : C ⥤ D₁) (L₂ : C ⥤ D₂)
-  (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W']
-
-lemma morphismProperty_eq_top [L.IsLocalization W] (P : MorphismProperty D) [P.RespectsIso]
-    [P.IsMultiplicative] (h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f))
-    (h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv) :
-    P = ⊤ := by
-  let P' : MorphismProperty W.Localization :=
-    P.inverseImage (Construction.lift L Functor.IsLocalization.inverts)
-  have hP' : P' = ⊤ := by
-    apply Construction.morphismProperty_is_top
-    · intros
-      simp only [MorphismProperty.inverseImage_iff, Construction.lift_obj, ← Functor.comp_map,
-        Functor.congr_hom (Construction.fac L Functor.IsLocalization.inverts), Functor.comp_obj,
-        eqToHom_refl, Category.comp_id, Category.id_comp, h₁, P']
-    · intro X Y w hw
-      simp only [P', MorphismProperty.inverseImage_iff]
-      convert h₂ w hw
-      convert Functor.map_inv (Construction.lift L Functor.IsLocalization.inverts)
-        (Construction.wIso w hw).hom
-      · simp
-      · have : (Construction.wIso w hw).hom = W.Q.map w := rfl
-        simp only [this, ← Functor.comp_map,
-          Functor.congr_hom (Construction.fac L Functor.IsLocalization.inverts)]
-        simp [isoOfHom]
-  have : P'.map _ = P := MorphismProperty.map_inverseImage_eq_of_isEquivalence ..
-  simp [← this, hP']
-
-lemma isGroupoid [L.IsLocalization ⊤] :
-    IsGroupoid D := by
-  rw [isGroupoid_iff_isomorphisms_eq_top]
-  exact morphismProperty_eq_top L ⊤ _
-    (fun _ _ f ↦ inverts L ⊤ _ (by simp))
-    (fun _ _ f hf ↦ Iso.isIso_inv _)
-
-instance : IsGroupoid (⊤ : MorphismProperty C).Localization :=
-  isGroupoid <| MorphismProperty.Q ⊤
-
-/-- Localization of a category with respect to all morphisms results in a groupoid. -/
-def groupoid : Groupoid (⊤ : MorphismProperty C).Localization :=
-  Groupoid.ofIsGroupoid
-
-end CategoryTheory.Localization
diff --git a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean
deleted file mode 100644
index 8773745c..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import Mathlib.CategoryTheory.MorphismProperty.Basic
-
-universe u v
-
-namespace CategoryTheory.MorphismProperty
-
-variable {C : Type u} [Category.{v} C] {D : Type*} [Category D]
-
-@[simp]
-lemma map_top_eq_top_of_essSurj_of_full (F : C ⥤ D) [F.EssSurj] [F.Full] :
-    (⊤ : MorphismProperty C).map F = ⊤ := by
-  rw [eq_top_iff]
-  intro X Y f _
-  refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
-  · exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv
-  · exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
-      (by simp)
-
-end CategoryTheory.MorphismProperty
diff --git a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean b/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean
index aee6e9a4..d8697466 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean
+++ b/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₃
diff --git a/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean b/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean
index acffbd24..49174775 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean
+++ b/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
 
 /-!
diff --git a/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean b/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean
index d03c7c5b..2c4b7d1b 100644
--- a/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean
+++ b/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 }
 
diff --git a/HoTTLean/ForPoly.lean b/HoTTLean/ForPoly.lean
index b9a44a91..72f1fdb6 100644
--- a/HoTTLean/ForPoly.lean
+++ b/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'}
diff --git a/HoTTLean/Model/Natural/NaturalModel.lean b/HoTTLean/Model/Natural/NaturalModel.lean
index 3671be69..57659ea2 100644
--- a/HoTTLean/Model/Natural/NaturalModel.lean
+++ 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
diff --git a/HoTTLean/Model/Unstructured/Interpretation.lean b/HoTTLean/Model/Unstructured/Interpretation.lean
index 521e84d3..346a7c30 100644
--- a/HoTTLean/Model/Unstructured/Interpretation.lean
+++ b/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]
 
diff --git a/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean b/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean
index 5e57936b..eed87d11 100644
--- a/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean
+++ b/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]
 
 /--
diff --git a/HoTTLean/Syntax/Axioms.lean b/HoTTLean/Syntax/Axioms.lean
index a7056c45..0555add7 100644
--- a/HoTTLean/Syntax/Axioms.lean
+++ b/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
diff --git a/lake-manifest.json b/lake-manifest.json
index 930c29a9..c0035dca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,21 +11,21 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/sinhp/Poly",
+  {"url": "https://github.com/Vtec234/Poly",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aedee22f07d681d845bcbe4a1fb9aa10f95c9977",
+   "rev": "c26e710a750cb9d769ee51d0b1b737f9eb437700",
    "name": "Poly",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "bump/v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818",
+   "rev": "b8dad038b1b3a05b77d6884b15b8db03ec01dca1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8864a73bf79aad549e34eff972c606343935106d",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
+   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.77",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca",
+   "rev": "100083c18750b6a9b7553c65f6b052c0a2f6bcb4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0-rc2",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "hottlean",
diff --git a/lakefile.lean b/lakefile.lean
index 2807a875..5a075793 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,13 +1,13 @@
 import Lake
 open Lake DSL
 
-require Poly from git "https://github.com/sinhp/Poly" @ "master"
+require Poly from git "https://github.com/Vtec234/Poly" @ "bump/v4.28.0-rc1"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.25.0-rc2"
+  "https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1"
 
 package hottlean where
   -- Settings applied to both builds and interactive editing
diff --git a/lean-toolchain b/lean-toolchain
index 137937a3..3e9b4e15 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.28.0-rc1
\ No newline at end of file