From d6a22a31c74e658f4f43eba4386fc9571c4e76f6 Mon Sep 17 00:00:00 2001 From: euprunin Date: Sun, 15 Feb 2026 17:43:59 +0100 Subject: [PATCH] chore: golf proofs --- Mathlib/Combinatorics/Tiling/Tile.lean | 10 ++-------- Mathlib/Probability/Distributions/Fernique.lean | 4 +--- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/Mathlib/Combinatorics/Tiling/Tile.lean b/Mathlib/Combinatorics/Tiling/Tile.lean index 073b8316ce1185..52ebbe32c7f57e 100644 --- a/Mathlib/Combinatorics/Tiling/Tile.lean +++ b/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. -/ diff --git a/Mathlib/Probability/Distributions/Fernique.lean b/Mathlib/Probability/Distributions/Fernique.lean index bdb92e9b00de77..dd7117f55f6cca 100644 --- a/Mathlib/Probability/Distributions/Fernique.lean +++ b/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