chore: golf proofs

Mathlib/Combinatorics/Tiling/Tile.lean

@@ -139,7 +139,7 @@ variable (ps) in
 /-- A `PlacedTile ps` is an image of a tile in the protoset `p` under an element of the group `G`.
 This is represented using a quotient so that images under group elements differing only by a
 symmetry of the tile are equal. -/
-@[ext] structure PlacedTile where
+@[ext, grind ext] structure PlacedTile where
   /-- The index of the tile in the protoset. -/
   index : ιₚ
   /-- The group elements under which this tile is an image. -/
@@ -165,13 +165,7 @@ lemma ext_iff_of_exists {pt₁ pt₂ : PlacedTile ps} :
     simp only [and_self, true_and]
     refine ⟨pt₁.groupElts.out, ?_⟩
     rw [Quotient.out_eq]
-  · rcases pt₁ with ⟨i₁, g₁⟩
-    rcases pt₂ with ⟨i₂, g₂⟩
-    dsimp only at h
-    subst h
-    ext
-    · rfl
-    · exact heq_of_eq (hg₁.symm.trans hg₂)
+  · grind
 
 /-- An alternative extensionality principle for `PlacedTile` that avoids `HEq`, using equality of
 quotient preimages. -/

Mathlib/Probability/Distributions/Fernique.lean

@@ -421,9 +421,7 @@ lemma lintegral_exp_mul_sq_norm_le_mul [IsProbabilityMeasure μ]
       change μ {x | ¬ x ∈ closedBall 0 a} = 0
       rw [← ae_iff]
       filter_upwards [ha] with x hx using by simp [hx]
-    · refine measurable_to_prop ?_
-      rw [show (fun x : E ↦ ‖x‖ ≤ a) ⁻¹' {True} = {x : E | ‖x‖ ≤ a} by ext; simp]
-      exact measurableSet_le (by fun_prop) (by fun_prop)
+    · fun_prop
   -- So we can assume `μ {x | ‖x‖ ≤ a} < 1`, which implies `c' < 1`
   have ha_lt : μ {x | ‖x‖ ≤ a} < 1 := lt_of_le_of_ne prob_le_one ha
   have hc'_lt : c' < 1 := lt_of_le_of_lt hc' ha_lt