chore: golf using grind (and add four supporting grind annotations) (leanprover-community#34154)

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

Trace profiling results (shown if ≥10 ms before or after):
* `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`: 311 ms before, 284 ms after  🎉
* `UV.compression_self`: 29 ms before, 19 ms after  🎉
* `IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C`: 405 ms before, 291 ms after  🎉
* `InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero`: 425 ms before, 309 ms after 🎉

This golfing 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/Algebra/Polynomial/Degree/Defs.lean

@@ -210,11 +210,11 @@ theorem degree_C_mul_X_pow_le (n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n :=
 theorem degree_C_mul_X_le (a : R) : degree (C a * X) ≤ 1 := by
   simpa only [pow_one] using degree_C_mul_X_pow_le 1 a
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_C_mul_X_pow (n : ℕ) (a : R) (ha : a ≠ 0) : natDegree (C a * X ^ n) = n :=
   natDegree_eq_of_degree_eq_some (degree_C_mul_X_pow n ha)
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_C_mul_X (a : R) (ha : a ≠ 0) : natDegree (C a * X) = 1 := by
   simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha
 

Mathlib/Algebra/Polynomial/Degree/Operations.lean

@@ -200,7 +200,7 @@ theorem natDegree_add_eq_right_of_natDegree_lt (h : natDegree p < natDegree q) :
 theorem degree_add_C (hp : 0 < degree p) : degree (p + C a) = degree p :=
   add_comm (C a) p ▸ degree_add_eq_right_of_degree_lt <| lt_of_le_of_lt degree_C_le hp
 
-@[simp] theorem natDegree_add_C {a : R} : (p + C a).natDegree = p.natDegree := by
+@[simp, grind =] theorem natDegree_add_C {a : R} : (p + C a).natDegree = p.natDegree := by
   rcases eq_or_ne p 0 with rfl | hp
   · simp
   by_cases! hpd : p.degree ≤ 0

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

@@ -392,11 +392,7 @@ theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) :
         mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
         real_inner_self_eq_norm_sq]
       exact this
-    rintro ⟨ha, hb⟩
-    have hx' : 0 < ‖x‖ := by simpa using hx
-    have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity)
-    have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb
-    exact (SameRay.sameRay_nonneg_smul_right x ha').add_right <| by simp [hb']
+    simp_all
   · intro h
     obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
     simp only [inner_smul_right, real_inner_self_eq_norm_sq, map_smulₛₗ, areaForm_apply_self,

Mathlib/Combinatorics/SetFamily/Compression/UV.lean

@@ -92,7 +92,7 @@ theorem compress_of_disjoint_of_le' (hva : Disjoint v a) (hua : u ≤ a) :
       (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩),
     sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right]
 
-@[simp]
+@[simp, grind =]
 theorem compress_self (u a : α) : compress u u a = a := by
   unfold compress
   split_ifs with h
@@ -153,14 +153,7 @@ protected theorem IsCompressed.eq (h : IsCompressed u v s) : 𝓒 u v s = s := h
 
 @[simp]
 theorem compression_self (u : α) (s : Finset α) : 𝓒 u u s = s := by
-  unfold compression
-  convert union_empty s
-  · ext a
-    rw [mem_filter, compress_self, and_self_iff]
-  · refine eq_empty_of_forall_notMem fun a ha ↦ ?_
-    simp_rw [mem_filter, mem_image, compress_self] at ha
-    obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha
-    exact hb' hb
+  grind [mem_compression]
 
 /-- Any family is compressed along two identical elements. -/
 theorem isCompressed_self (u : α) (s : Finset α) : IsCompressed u u s := compression_self u s

Mathlib/FieldTheory/IsSepClosed.lean

@@ -104,18 +104,12 @@ theorem exists_root_C_mul_X_pow_add_C_mul_X_add_C
     [IsSepClosed k] {n : ℕ} (a b c : k) (hn : (n : k) = 0) (hn' : 2 ≤ n) (hb : b ≠ 0) :
     ∃ x, a * x ^ n + b * x + c = 0 := by
   let f : k[X] := C a * X ^ n + C b * X + C c
-  have hdeg : f.degree ≠ 0 := degree_ne_of_natDegree_ne <| by
+  -- Specify `n := 0` below, otherwise Lean unfolds `0` to `Zero.zero`.
+  have hdeg : f.degree ≠ 0 := degree_ne_of_natDegree_ne (n := 0) <| by
+    have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind
     by_cases ha : a = 0
-    · suffices f.natDegree = 1 from this ▸ one_ne_zero
-      simp_rw [f, ha, map_zero, zero_mul, zero_add]
-      compute_degree!
-    · suffices f.natDegree = n from this ▸ (lt_of_lt_of_le zero_lt_two hn').ne'
-      simp_rw [f]
-      have h0 : n ≠ 0 := by linarith only [hn']
-      have h1 : n ≠ 1 := by linarith only [hn']
-      have : 1 ≤ n := le_trans one_le_two hn'
-      compute_degree!
-      simp [h0, h1, ha]
+    · grind [zero_add]
+    · grind [natDegree_add_eq_left_of_natDegree_lt]
   have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit
   obtain ⟨x, hx⟩ := exists_root f hdeg hsep
   exact ⟨x, by simpa [f] using hx⟩

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

@@ -276,13 +276,8 @@ theorem norm_sub_eq_add_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y 
 if and only the angle between the two vectors is 0. -/
 theorem norm_add_eq_add_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
     ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0 := by
-  refine ⟨fun h => ?_, norm_add_eq_add_norm_of_angle_eq_zero⟩
-  rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]
-  obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)
-  rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_add_pow_two_real] at h
-  calc
-    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
-    _ = ‖x‖ * ‖y‖ := by ring
+  refine ⟨?_, norm_add_eq_add_norm_of_angle_eq_zero⟩
+  grind [inner_eq_mul_norm_iff_angle_eq_zero hx hy, norm_add_pow_two_real]
 
 /-- The norm of the difference of two non-zero vectors equals the absolute value
 of the difference of their norms if and only the angle between the two vectors is 0. -/