restore a proof

leanprover-community · Jun 8, 2023 · ae8d859 · ae8d859
1 parent b6e86a2
commit ae8d859
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/CategoryTheory/Sites/Plus.lean b/Mathlib/CategoryTheory/Sites/Plus.lean
@@ -57,6 +57,7 @@ def diagramPullback {X Y : C} (f : X ⟶ Y) : J.diagram P Y ⟶ (J.pullback f).o
   app S :=
     Multiequalizer.lift _ _ (fun I => Multiequalizer.ι (S.unop.index P) I.base) fun I =>
       Multiequalizer.condition (S.unop.index P) I.base
+  naturality S T f := Multiequalizer.hom_ext _ _ _ (fun I => by dsimp ; simp ; rfl)
 #align category_theory.grothendieck_topology.diagram_pullback CategoryTheory.GrothendieckTopology.diagramPullback
 
 /-- A natural transformation `P ⟶ Q` induces a natural transformation