fix

Author: joelriou

Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

@@ -598,7 +598,7 @@ noncomputable def fullyFaithfulToDescentData [F.IsPrestack J] (hf : Sieve.ofArro
       isPrestackFor_iff_isSheafFor]
     intro M N
     refine ((isSheaf_iff_isSheaf_of_type _ _).1
-      (IsPrestack.isSheaf J M N)).isSheafFor _ _ ?_
+      (IsPrestack.isSheaf J M N)).isSheafFor _ ?_
     rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply])
 
 lemma isPrestackFor [F.IsPrestack J] {S : C} (R : Presieve S) (hR : Sieve.generate R ∈ J S) :

Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean

@@ -234,21 +234,21 @@ is a prestack and `f'` a covering family, this is the morphism `D₁.obj i ⟶ D
 that is deduced from `φ` by gluing. -/
 noncomputable def hom (i : ι) : D₁.obj i ⟶ D₂.obj i :=
   F.presheafHomObjHomEquiv.symm
-    (Presieve.IsSheafFor.amalgamate (Presieve.IsSheaf.isSheafFor _
-    ((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)) _
-      (by simpa using sieve_mem _ hf' i)) _
-        (compatible_familyOfElements w φ i))
+    (Presieve.IsSheafFor.amalgamate
+      (((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)).isSheafFor _
+        (by simpa using sieve_mem _ hf' i)) _
+          (compatible_familyOfElements w φ i))
 
 lemma map_hom ⦃i : ι⦄ ⦃Y : C⦄ (q : Y ⟶ X i) ⦃j : ι'⦄
     (a : Y ⟶ X' j) (fac : a ≫ f' j = q ≫ f i := by cat_disch) :
     (F.map q.op.toLoc).toFunctor.map (hom w hf' φ i) = mor w φ q a fac := by
-  let s := Presieve.IsSheafFor.amalgamate (Presieve.IsSheaf.isSheafFor _
-    ((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)) _
+  let s := Presieve.IsSheafFor.amalgamate
+    (((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)).isSheafFor _
       (by simpa using sieve_mem _ hf' i)) _
         (compatible_familyOfElements w φ i)
   have hs : (familyOfElements w φ i).IsAmalgamation s :=
-    Presieve.IsSheafFor.isAmalgamation (Presieve.IsSheaf.isSheafFor _
-      ((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)) _
+    Presieve.IsSheafFor.isAmalgamation
+      (((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)).isSheafFor _
         (by simpa using sieve_mem _ hf' i)) (compatible_familyOfElements w φ i)
   simpa [hom, familyOfElements_eq w φ (Z := Over.mk q) _ a fac,
     presheafHomObjHomEquiv, pullHom, mapComp'_id_comp_hom_app,

Mathlib/CategoryTheory/Sites/Types.lean

@@ -87,10 +87,10 @@ open Presieve
 `(α → S(*)) → S(α)` that is inverse to `eval`. -/
 noncomputable def typesGlue (S : Type uᵒᵖ ⥤ Type u) (hs : IsSheaf typesGrothendieckTopology S)
     (α : Type u) (f : α → S.obj (op PUnit)) : S.obj (op α) :=
-  (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).amalgamate
+  (hs.isSheafFor _ (generate_discretePresieve_mem α)).amalgamate
     (fun _ g hg => S.map (↾fun _ => PUnit.unit).op <| f <| g <| Classical.choose hg)
     fun β γ δ g₁ g₂ f₁ f₂ hf₁ hf₂ h =>
-    (hs.isSheafFor _ _ (generate_discretePresieve_mem δ)).isSeparatedFor.ext fun ε g ⟨x, _⟩ => by
+    (hs.isSheafFor _ (generate_discretePresieve_mem δ)).isSeparatedFor.ext fun ε g ⟨x, _⟩ => by
       have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
         Classical.choose_spec hf₁ (g₁ <| g x) ▸
           Classical.choose_spec hf₂ (g₂ <| g x) ▸ congr_fun h _
@@ -103,7 +103,7 @@ theorem eval_typesGlue {S hs α} (f) : eval.{u} S α (typesGlue S hs α f) = f :
   convert FunctorToTypes.map_id_apply S _
 
 theorem typesGlue_eval {S hs α} (s) : typesGlue.{u} S hs α (eval S α s) = s := by
-  apply (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
+  apply (hs.isSheafFor _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
   intro β f hf
   apply (IsSheafFor.valid_glue _ _ _ hf).trans
   apply (FunctorToTypes.map_comp_apply _ _ _ _).symm.trans