chore(algebraic_geometry/pullbacks): replaced some simps by simp onlys (

#13258)

This PR optimizes the file `algebraic_geometry/pullbacks` by replacing some calls to `simp` by `simp only [⋯]`.

This file has a high [`sec/LOC` ratio](https://mathlib-bench.limperg.de/commit/5e98dc1cc915d3226ea293c118d2ff657b48b0dc) and is not very short, which makes it a good candidate for such optimizations attempts.

On my machine, these changes reduced the compile time from 2m30s to 1m20s.

src/algebraic_geometry/pullbacks.lean

@@ -58,25 +58,40 @@ end
 
 @[simp, reassoc]
 lemma t_fst_fst (i j : 𝒰.J) : t 𝒰 f g i j ≫ pullback.fst ≫ pullback.fst = pullback.snd :=
-by { delta t, simp }
+begin
+  delta t,
+  simp only [category.assoc, id.def, pullback_symmetry_hom_comp_fst_assoc,
+    pullback_assoc_hom_snd_fst, pullback.lift_fst_assoc, pullback_symmetry_hom_comp_snd,
+    pullback_assoc_inv_fst_fst, pullback_symmetry_hom_comp_fst],
+end
 
 @[simp, reassoc]
 lemma t_fst_snd (i j : 𝒰.J) :
   t 𝒰 f g i j ≫ pullback.fst ≫ pullback.snd = pullback.fst ≫ pullback.snd :=
-by { delta t, simp }
+begin
+  delta t,
+  simp only [pullback_symmetry_hom_comp_snd_assoc, category.comp_id, category.assoc, id.def,
+    pullback_symmetry_hom_comp_fst_assoc, pullback_assoc_hom_snd_snd, pullback.lift_snd,
+    pullback_assoc_inv_snd],
+end
 
 @[simp, reassoc]
 lemma t_snd (i j : 𝒰.J) :
   t 𝒰 f g i j ≫ pullback.snd = pullback.fst ≫ pullback.fst :=
-by { delta t, simp }
+begin
+  delta t,
+  simp only [pullback_symmetry_hom_comp_snd_assoc, category.assoc, id.def,
+    pullback_symmetry_hom_comp_snd, pullback_assoc_hom_fst, pullback.lift_fst_assoc,
+    pullback_symmetry_hom_comp_fst, pullback_assoc_inv_fst_snd],
+end
 
 lemma t_id (i : 𝒰.J) : t 𝒰 f g i i = 𝟙 _ :=
 begin
   apply pullback.hom_ext; rw category.id_comp,
   apply pullback.hom_ext,
-  { rw ← cancel_mono (𝒰.map i), simp [pullback.condition] },
-  { simp },
-  { rw ← cancel_mono (𝒰.map i), simp [pullback.condition] }
+  { rw ← cancel_mono (𝒰.map i), simp only [pullback.condition, category.assoc, t_fst_fst] },
+  { simp only [category.assoc, t_fst_snd]},
+  { rw ← cancel_mono (𝒰.map i),simp only [pullback.condition, t_snd, category.assoc] }
 end
 
 /-- The inclusion map of `V i j = (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ Uᵢ ×[Z] Y`-/
@@ -91,73 +106,106 @@ begin
   refine _ ≫ (pullback_symmetry _ _).hom,
   refine _ ≫ (pullback_right_pullback_fst_iso _ _ _).inv,
   refine pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) _ _,
-  { simp [← pullback.condition] },
-  { simp }
+  { simp only [←pullback.condition, category.comp_id, t_fst_fst_assoc] },
+  { simp only [category.comp_id, category.id_comp]}
 end
 
 section end
 
 @[simp, reassoc]
 lemma t'_fst_fst_fst (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.fst ≫ pullback.fst ≫ pullback.fst = pullback.fst ≫ pullback.snd :=
-by { delta t', simp }
+begin
+  delta t',
+  simp only [category.assoc, pullback_symmetry_hom_comp_fst_assoc,
+    pullback_right_pullback_fst_iso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 
 @[simp, reassoc]
 lemma t'_fst_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.fst ≫ pullback.fst ≫ pullback.snd =
     pullback.fst ≫ pullback.fst ≫ pullback.snd :=
-by { delta t', simp }
+begin
+  delta t',
+  simp only [category.assoc, pullback_symmetry_hom_comp_fst_assoc,
+    pullback_right_pullback_fst_iso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 
 @[simp, reassoc]
 lemma t'_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.fst ≫ pullback.snd = pullback.snd ≫ pullback.snd :=
-by { delta t', simp }
+begin
+  delta t',
+  simp only [category.comp_id, category.assoc, pullback_symmetry_hom_comp_fst_assoc,
+    pullback_right_pullback_fst_iso_inv_snd_snd, pullback.lift_snd,
+    pullback_right_pullback_fst_iso_hom_snd],
+end
 
 @[simp, reassoc]
 lemma t'_snd_fst_fst (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.snd ≫ pullback.fst ≫ pullback.fst = pullback.fst ≫ pullback.snd :=
-by { delta t', simp }
+begin
+  delta t',
+  simp only [category.assoc, pullback_symmetry_hom_comp_snd_assoc,
+    pullback_right_pullback_fst_iso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 
 @[simp, reassoc]
 lemma t'_snd_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.snd ≫ pullback.fst ≫ pullback.snd =
     pullback.fst ≫ pullback.fst ≫ pullback.snd :=
-by { delta t', simp }
+begin
+  delta t',
+  simp only [category.assoc, pullback_symmetry_hom_comp_snd_assoc,
+    pullback_right_pullback_fst_iso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 
 @[simp, reassoc]
 lemma t'_snd_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ pullback.snd ≫ pullback.snd = pullback.fst ≫ pullback.fst ≫ pullback.fst :=
-by { delta t', simp, }
+begin
+  delta t',
+  simp only [category.assoc, pullback_symmetry_hom_comp_snd_assoc,
+    pullback_right_pullback_fst_iso_inv_fst_assoc, pullback.lift_fst_assoc, t_snd,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 
 lemma cocycle_fst_fst_fst (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst ≫ pullback.fst ≫
   pullback.fst = pullback.fst ≫ pullback.fst ≫ pullback.fst :=
-by simp
+by simp only [t'_fst_fst_fst, t'_fst_snd, t'_snd_snd]
 
 lemma cocycle_fst_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst ≫ pullback.fst ≫
   pullback.snd = pullback.fst ≫ pullback.fst ≫ pullback.snd :=
-by simp
+by simp only [t'_fst_fst_snd]
 
 lemma cocycle_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst ≫ pullback.snd =
     pullback.fst ≫ pullback.snd :=
-by simp
+by simp only [t'_fst_snd, t'_snd_snd, t'_fst_fst_fst]
 
 lemma cocycle_snd_fst_fst (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd ≫ pullback.fst ≫
   pullback.fst = pullback.snd ≫ pullback.fst ≫ pullback.fst :=
-by { rw ← cancel_mono (𝒰.map i), simp [pullback.condition_assoc, pullback.condition] }
+begin
+  rw ← cancel_mono (𝒰.map i),
+  simp only [pullback.condition_assoc, t'_snd_fst_fst, t'_fst_snd, t'_snd_snd]
+end
 
 lemma cocycle_snd_fst_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd ≫ pullback.fst ≫
   pullback.snd = pullback.snd ≫ pullback.fst ≫ pullback.snd :=
-by { simp [pullback.condition_assoc, pullback.condition] }
+by simp only [pullback.condition_assoc, t'_snd_fst_snd]
 
 lemma cocycle_snd_snd (i j k : 𝒰.J) :
   t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd ≫ pullback.snd =
     pullback.snd ≫ pullback.snd :=
-by simp
+by simp only [t'_snd_snd, t'_fst_fst_fst, t'_fst_snd]
 
 -- `by tidy` should solve it, but it times out.
 lemma cocycle (i j k : 𝒰.J) :
@@ -250,20 +298,27 @@ begin
   { exact (pullback_symmetry _ _).hom ≫
       pullback.map _ _ _ _ (𝟙 _) s.snd f (category.id_comp _).symm s.condition },
   { simpa using pullback.condition },
-  { simp }
+  { simp only [category.comp_id, category.id_comp] }
 end
 
 @[reassoc]
 lemma glued_lift_pullback_map_fst (i j : 𝒰.J) :
   glued_lift_pullback_map 𝒰 f g s i j ≫ pullback.fst = pullback.fst ≫
     (pullback_symmetry _ _).hom ≫
       pullback.map _ _ _ _ (𝟙 _) s.snd f (category.id_comp _).symm s.condition :=
-by { delta glued_lift_pullback_map, simp }
-
+begin
+  delta glued_lift_pullback_map,
+  simp only [category.assoc, id.def, pullback.lift_fst,
+    pullback_right_pullback_fst_iso_hom_fst_assoc],
+end
 @[reassoc]
 lemma glued_lift_pullback_map_snd (i j : 𝒰.J) :
   glued_lift_pullback_map 𝒰 f g s i j ≫ pullback.snd = pullback.snd ≫ pullback.snd :=
-by { delta glued_lift_pullback_map, simp }
+begin
+  delta glued_lift_pullback_map,
+  simp only [category.assoc, category.comp_id, id.def, pullback.lift_snd,
+    pullback_right_pullback_fst_iso_hom_snd],
+end
 
 /--
 The lifted map `s.X ⟶ (gluing 𝒰 f g).glued` in order to show that `(gluing 𝒰 f g).glued` is
@@ -343,12 +398,19 @@ def pullback_fst_ι_to_V (i j : 𝒰.J) :
 
 @[simp, reassoc] lemma pullback_fst_ι_to_V_fst (i j : 𝒰.J) :
   pullback_fst_ι_to_V 𝒰 f g i j ≫ pullback.fst = pullback.snd :=
-by { delta pullback_fst_ι_to_V, simp }
+begin
+  delta pullback_fst_ι_to_V,
+  simp only [iso.trans_hom, pullback.congr_hom_hom, category.assoc, pullback.lift_fst,
+    category.comp_id, pullback_right_pullback_fst_iso_hom_fst, pullback_symmetry_hom_comp_fst],
+end
 
 @[simp, reassoc] lemma pullback_fst_ι_to_V_snd (i j : 𝒰.J) :
   pullback_fst_ι_to_V 𝒰 f g i j ≫ pullback.snd = pullback.fst ≫ pullback.snd :=
-by { delta pullback_fst_ι_to_V, simp }
-
+begin
+  delta pullback_fst_ι_to_V,
+  simp only [iso.trans_hom, pullback.congr_hom_hom, category.assoc, pullback.lift_snd,
+    category.comp_id, pullback_right_pullback_fst_iso_hom_snd, pullback_symmetry_hom_comp_snd_assoc]
+end
 /-- We show that the map `W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W` is the first projection, where the
 first map is given by the lift of `W ×[X] Uᵢ ⟶ Uᵢ` and `W ×[X] Uᵢ ⟶ W ⟶ Y`.
 
@@ -373,8 +435,8 @@ begin
   { rw [pullback.condition, ← category.assoc],
     congr' 1,
     apply pullback.hom_ext,
-    { simp },
-    { simp } }
+    { simp only [pullback_fst_ι_to_V_fst] },
+    { simp only [pullback_fst_ι_to_V_fst] } }
 end
 
 /-- The canonical isomorphism between `W ×[X] Uᵢ` and `Uᵢ ×[X] Y`. That is, the preimage of `Uᵢ` in
@@ -389,27 +451,28 @@ begin
     (by erw multicoequalizer.π_desc),
   { apply pullback.hom_ext,
     { simpa using lift_comp_ι 𝒰 f g i },
-    { simp } },
+    { simp only [category.assoc, pullback.lift_snd, pullback.lift_fst, category.id_comp] } },
   { apply pullback.hom_ext,
-    { simp },
-    { simp, erw multicoequalizer.π_desc } },
+    { simp only [category.assoc, pullback.lift_fst, pullback.lift_snd, category.id_comp] },
+    { simp only [category.assoc, pullback.lift_snd, pullback.lift_fst_assoc, category.id_comp],
+      erw multicoequalizer.π_desc } },
 end
 
 @[simp, reassoc] lemma pullback_p1_iso_hom_fst (i : 𝒰.J) :
   (pullback_p1_iso 𝒰 f g i).hom ≫ pullback.fst = pullback.snd :=
-by { delta pullback_p1_iso, simp }
+by { delta pullback_p1_iso, simp only [pullback.lift_fst] }
 
 @[simp, reassoc] lemma pullback_p1_iso_hom_snd (i : 𝒰.J) :
   (pullback_p1_iso 𝒰 f g i).hom ≫ pullback.snd = pullback.fst ≫ p2 𝒰 f g :=
-by { delta pullback_p1_iso, simp }
+by { delta pullback_p1_iso, simp only [pullback.lift_snd] }
 
 @[simp, reassoc] lemma pullback_p1_iso_inv_fst (i : 𝒰.J) :
   (pullback_p1_iso 𝒰 f g i).inv ≫ pullback.fst = (gluing 𝒰 f g).ι i :=
-by { delta pullback_p1_iso, simp }
+by { delta pullback_p1_iso, simp only [pullback.lift_fst] }
 
 @[simp, reassoc] lemma pullback_p1_iso_inv_snd (i : 𝒰.J) :
   (pullback_p1_iso 𝒰 f g i).inv ≫ pullback.snd = pullback.fst :=
-by { delta pullback_p1_iso, simp }
+by { delta pullback_p1_iso, simp only [pullback.lift_snd] }
 
 @[simp, reassoc]
 lemma pullback_p1_iso_hom_ι (i : 𝒰.J) :