chore: golf using grind and simp (leanprover-community#36380)

The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.

Trace profiling results (differences <30 ms considered measurement noise):
* `AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology`: unchanged 🎉
* `CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app`: unchanged 🎉
* `Finset.exists_subset_or_subset_of_two_mul_lt_card`: 210 ms before, 173 ms after  🎉

Profiled using `set_option trace.profiler true in`.

This PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR

Author: euprunin

Mathlib/AlgebraicGeometry/Sites/QuasiCompact.lean

@@ -217,15 +217,8 @@ lemma Cover.mem_propQCTopology {S : Scheme.{u}} (𝒰 : Cover.{u} (precoverage P
   rwa [presieve₀_mem_qcPrecoverage_iff]
 
 lemma zariskiTopology_le_propQCTopology [P.IsMultiplicative] [IsZariskiLocalAtSource P] :
-    zariskiTopology ≤ propQCTopology P := by
-  apply Precoverage.toGrothendieck_mono
-  rw [le_inf_iff]
-  refine ⟨?_, ?_⟩
-  · apply zariskiPrecoverage_le_qcPrecoverage
-  · rw [precoverage, precoverage]
-    gcongr
-    refine MorphismProperty.precoverage_monotone fun X Y h hf ↦
-      IsZariskiLocalAtSource.of_isOpenImmersion _
+    zariskiTopology ≤ propQCTopology P :=
+  Precoverage.toGrothendieck_mono zariskiPrecoverage_le_propQCPrecoverage
 
 end Property
 

Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

@@ -334,10 +334,7 @@ lemma shift_opShiftFunctorEquivalence_counitIso_inv_app
     shift_shiftFunctorCompIsoId_hom_app, op_comp, unop_comp, Quiver.Hom.unop_op,
     Functor.map_comp, Iso.inv_hom_id_app_assoc, Functor.op_obj]
   apply Quiver.Hom.unop_inj
-  dsimp
-  simp only [Category.assoc, ← Functor.map_comp_assoc, Iso.unop_hom_inv_id_app_assoc]
-  congr 3
-  exact (NatIso.naturality_1 (shiftFunctorCompIsoId C n (-n) (by lia)) _).symm
+  simp
 
 /-- Given objects `X` and `Y` in `Cᵒᵖ`, this is the bijection
 `(op (X.unop⟦n⟧) ⟶ Y) ≃ (X ⟶ Y⟦n⟧)` for any `n : ℤ`. -/

Mathlib/Data/Finset/Card.lean

@@ -656,11 +656,9 @@ theorem le_card_iff_exists_subset_card : n ≤ #s ↔ ∃ t ⊆ s, #t = n := by
 
 theorem exists_subset_or_subset_of_two_mul_lt_card [DecidableEq α] {X Y : Finset α} {n : ℕ}
     (hXY : 2 * n < #(X ∪ Y)) : ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := by
-  have h₁ : #(X ∩ (Y \ X)) = 0 := Finset.card_eq_zero.mpr (by grind)
-  have h₂ : #(X ∪ Y) = #X + #(Y \ X) := by grind
-  obtain h | h : n < #X ∨ n < #(Y \ X) := by lia
-  · exact ⟨X, by grind⟩
-  · exact ⟨Y \ X, by grind⟩
+  grind =>
+    have : #(X ∪ Y) = #X + #(Y \ X)
+    finish
 
 /-! ### Explicit description of a finset from its card -/