doc: fix composition order in Presieve.pullback docstring (leanprover-community#41573)

This PR fixes the `Presieve.pullback` docstring, which said the pullback of `R` along `f : X ⟶ Y` consists of all `g : Z ⟶ X` such that `f ≫ g` is in `R`; the definition uses `R (g ≫ f)`, and `f ≫ g` is not even well-typed, so the docstring now says `g ≫ f`.

Follow-up to [leanprover-community#40527 (feat(CategoryTheory/Sites): pushforward and pullback of presieves)](leanprover-community#40527).

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -320,7 +320,7 @@ lemma pushforward_singleton {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   rw [← ofArrows_pUnit.{0}, pushforward_ofArrows, ofArrows_pUnit.{0}]
 
 /-- The pullback of a presieve `R` on `Y` along a morphism `f : X ⟶ Y` is the presieve on `X`
-given by all morphisms `g : Z ⟶ X` such that `f ≫ g` is in `R`. -/
+given by all morphisms `g : Z ⟶ X` such that `g ≫ f` is in `R`. -/
 def pullback {X Y : C} (f : X ⟶ Y) (R : Presieve Y) : Presieve X :=
   fun _ g ↦ R (g ≫ f)