feat(CategoryTheory): IsIso.comp_isIso with explicit arguments (#15678

)

Often when one wants to prove that a composition is an isomorphism, one proves that each component is. The instance `IsIso.comp_isIso` can be annoying to because of its instance arguments, this PR adds a lemma `IsIso.comp_isIso'` which is exactly the same as the instance, but with explicit arguments.

This avoids having to guess the correct number of underscores in `@IsIso.comp_isIso` or doing `apply ( config := { allowSynthFailures := true } ) IsIso.comp_isIso` 

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -441,7 +441,7 @@ def basicOpenSectionsToAffine :
 instance basicOpenSectionsToAffine_isIso :
     IsIso (basicOpenSectionsToAffine hU f) := by
   delta basicOpenSectionsToAffine
-  apply (config := { allowSynthFailures := true }) IsIso.comp_isIso
+  refine IsIso.comp_isIso' ?_ inferInstance
   apply PresheafedSpace.IsOpenImmersion.isIso_of_subset
   rw [hU.range_fromSpec]
   exact RingedSpace.basicOpen_le _ _

Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

@@ -127,7 +127,7 @@ lemma isAffine_of_isAffineOpen_basicOpen (s : Set Γ(X, ⊤))
     exact hs₂ _ i.2
   · simp only [Functor.comp_obj, Functor.rightOp_obj, Scheme.Γ_obj, Scheme.Spec_obj, id_eq,
       eq_mpr_eq_cast, Functor.id_obj, Opens.map_top, morphismRestrict_app]
-    apply (config := { allowSynthFailures := true }) IsIso.comp_isIso
+    refine IsIso.comp_isIso' ?_ inferInstance
     convert isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0
     refine congr(IsIso ((ΓSpec.adjunction.unit.app X).app $(?_)))
     rw [Opens.openEmbedding_obj_top]

Mathlib/AlgebraicGeometry/Spec.lean

@@ -306,8 +306,7 @@ theorem Spec_map_localization_isIso (R : CommRingCat.{u}) (M : Submonoid R)
   erw [← localRingHom_comp_stalkIso]
   -- Porting note: replaced `apply (config := { instances := false })`.
   -- See https://github.com/leanprover/lean4/issues/2273
-  refine @IsIso.comp_isIso _ _ _ _ _ _ _ _ (?_)
-  refine @IsIso.comp_isIso _ _ _ _ _ _ _ (?_) _
+  refine IsIso.comp_isIso' inferInstance (IsIso.comp_isIso' ?_ inferInstance)
   /- I do not know why this is defeq to the goal, but I'm happy to accept that it is. -/
   show
     IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M

Mathlib/CategoryTheory/Iso.lean

@@ -344,6 +344,12 @@ because `f.hom` is defeq to `(fun x ↦ x) ≫ f.hom`, triggering a loop. -/
 instance (priority := 900) comp_isIso [IsIso f] [IsIso h] : IsIso (f ≫ h) :=
   (asIso f ≪≫ asIso h).isIso_hom
 
+/--
+The composition of isomorphisms is an isomorphism. Here the arguments of type `IsIso` are
+explicit, to make this easier to use with the `refine` tactic, for instance.
+-/
+lemma comp_isIso' (_ : IsIso f) (_ : IsIso h) : IsIso (f ≫ h) := inferInstance
+
 @[simp]
 theorem inv_id : inv (𝟙 X) = 𝟙 X := by
   apply inv_eq_of_hom_inv_id

Mathlib/CategoryTheory/Sites/Plus.lean

@@ -246,7 +246,7 @@ theorem isIso_toPlus_of_isSheaf (hP : Presheaf.IsSheaf J P) : IsIso (J.toPlus P)
   rw [Presheaf.isSheaf_iff_multiequalizer] at hP
   suffices ∀ X, IsIso ((J.toPlus P).app X) from NatIso.isIso_of_isIso_app _
   intro X
-  suffices IsIso (colimit.ι (J.diagram P X.unop) (op ⊤)) from IsIso.comp_isIso
+  refine IsIso.comp_isIso' inferInstance ?_
   suffices ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f) from
     isIso_ι_of_isInitial (initialOpOfTerminal isTerminalTop) _
   intro S T e

Mathlib/CategoryTheory/Sites/Preserves.lean

@@ -148,7 +148,7 @@ def preservesProductOfIsSheafFor
   have : HasCoproduct X := ⟨⟨c, hc⟩⟩
   refine @PreservesProduct.ofIsoComparison _ _ _ _ F _ (fun x ↦ op (X x)) _ _ ?_
   rw [piComparison_fac (hc := hc)]
-  refine @IsIso.comp_isIso _ _ _ _ _ _ _ inferInstance ?_
+  refine IsIso.comp_isIso' inferInstance ?_
   rw [isIso_iff_bijective, Function.bijective_iff_existsUnique]
   rw [Equalizer.Presieve.Arrows.sheaf_condition, Limits.Types.type_equalizer_iff_unique] at hF'
   exact fun b ↦ hF' b (congr_fun (firstMap_eq_secondMap F hF hI c hd) b)

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -152,7 +152,7 @@ instance comp {Z : PresheafedSpace C} (g : Y ⟶ Z) [hg : IsOpenImmersion g] :
     generalize_proofs h
     dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
       Opens.map_comp_obj]
-    apply (config := { allowSynthFailures := true }) IsIso.comp_isIso
+    apply IsIso.comp_isIso'
     · exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)
     · apply c_iso' f U
       ext1
@@ -738,7 +738,7 @@ theorem of_stalk_iso {X Y : SheafedSpace C} (f : X ⟶ Y) (hf : OpenEmbedding f.
       delta PresheafedSpace.Hom.stalkMap at H
       haveI H' :=
         TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_openEmbedding C hf X.presheaf y
-      have := @IsIso.comp_isIso _ _ _ _ _ _ _ H (@IsIso.inv_isIso _ _ _ _ _ H')
+      have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')
       rwa [Category.assoc, IsIso.hom_inv_id, Category.comp_id] at this }
 
 end OfStalkIso
@@ -1086,7 +1086,7 @@ theorem pullback_snd_isIso_of_range_subset (H' : Set.range g.1.base ⊆ Set.rang
   erw [← PreservesPullback.iso_hom_snd
       (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]
   -- Porting note: was `inferInstance`
-  exact @IsIso.comp_isIso _ _ _ _ _ _ _ _ <|
+  exact IsIso.comp_isIso' inferInstance <|
     PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'
 
 /-- The universal property of open immersions: