From b9d8d954f76047b674ba41bbeebc408b03782afd Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sun, 24 May 2026 07:43:14 -0400 Subject: [PATCH] chore(Topology): squeeze when grind? fails --- Mathlib/Topology/Compactness/CountablyCompact.lean | 8 ++++++-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 13 +++++++++---- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean | 3 ++- Mathlib/Topology/Order/Basic.lean | 3 ++- Mathlib/Topology/Order/IsLUB.lean | 3 ++- Mathlib/Topology/Order/WithTop.lean | 8 +++++--- Mathlib/Topology/Path.lean | 3 ++- Mathlib/Topology/Sets/VietorisTopology.lean | 8 +++++--- Mathlib/Topology/Sheaves/Flasque.lean | 3 ++- 9 files changed, 35 insertions(+), 17 deletions(-) diff --git a/Mathlib/Topology/Compactness/CountablyCompact.lean b/Mathlib/Topology/Compactness/CountablyCompact.lean index df37e4a99cfc55..833d7d0b94d04b 100644 --- a/Mathlib/Topology/Compactness/CountablyCompact.lean +++ b/Mathlib/Topology/Compactness/CountablyCompact.lean @@ -324,6 +324,7 @@ theorem IsCountablyCompact.exists_accPt_of_infinite ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite · exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2 +set_option linter.tacticAnalysis.verifyGrindOnly false in /-- In a `T₁` space, a set is countably compact if and only if every infinite subset has an accumulation point in the set. -/ theorem isCountablyCompact_iff_infinite_subset_has_accPt [T1Space E] {A : Set E} : @@ -340,10 +341,13 @@ theorem isCountablyCompact_iff_infinite_subset_has_accPt [T1Space E] {A : Set E} · -- Case 2: Infinite range obtain ⟨a, haA, hacc⟩ := h (Set.range x ∩ A) inter_subset_right <| by rw [eventually_iff, mem_cofinite, compl_setOf] at hx - exact hfin.inter_of_finite_diff (hx.image x |>.subset (by grind)) + refine hfin.inter_of_finite_diff (hx.image x |>.subset ?_) + simp only [diff_subset_iff] + grind refine ⟨a, haA, ?_⟩ simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite] - exact fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono (by grind) |>.of_image x + refine fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono ?_ |>.of_image x + grind only [= subset_def, = mem_inter_iff, = mem_image, = mem_range, usr mem_setOf_eq] /-- A countably compact Lindelöf set is compact. -/ theorem IsLindelof.isCompact (hA : IsCountablyCompact A) (hl : IsLindelof A) : diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean index ac16ca16607048..61927353a3f3c2 100644 --- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean +++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean @@ -251,6 +251,7 @@ theorem _root_.BoundedVariationOn.sub_le {f : α → ℝ} {s : Set α} (h : Boun rw [← Real.dist_eq] exact h.dist_le hx hy +set_option linter.tacticAnalysis.verifyGrindOnly false in /-- Consider a monotone function `u` parameterizing some points of a set `s`. Given `x ∈ s`, then one can find another monotone function `v` parameterizing the same points as `u`, with `x` added. In particular, the variation of a function along `u` is bounded by its variation along `v`. -/ @@ -261,7 +262,7 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) := by rcases le_or_gt (u n) x with (h | h) · let v i := if i ≤ n then u i else x - refine ⟨v, n + 2, by grind [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩ + refine ⟨v, n + 2, by grind only [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩ calc (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr] @@ -327,6 +328,7 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ _ = ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> grind +set_option linter.tacticAnalysis.verifyGrindOnly false in /-- The variation of a function on the union of two sets `s` and `t`, with `s` to the left of `t`, bounds the sum of the variations along `s` and `t`. -/ theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : @@ -363,7 +365,8 @@ theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t abel _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by rw [← Finset.sum_union] - · gcongr; grind + · gcongr + grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_range, = Finset.mem_Ico] · exact Finset.disjoint_left.2 (by grind) _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (by grind) @@ -505,6 +508,7 @@ end Monotone /-! ### Left and right limits of bounded variation functions -/ +set_option linter.tacticAnalysis.verifyGrindOnly false in /-- If a function is continuous on the left at a point `a`, then its variations on `Iio a` and on `Iic a` coincide. We give a version relative to a set `s`. -/ lemma eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt @@ -544,8 +548,9 @@ lemma eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true, Finset.sum_insert] congr 1 <;> grind [Finset.sum_congr] - _ ≤ eVariationOn f (s ∩ Iio a) := - sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind [StrictMonoOn]) + _ ≤ eVariationOn f (s ∩ Iio a) := by + refine sum_le_of_monotoneOn_Iic ?_ (by grind [StrictMonoOn]) + grind only [StrictMonoOn, mem_Iic, mem_inter_iff, mem_Ioo, MonotoneOn] /-- If a function is continuous on the right at a point `a`, then its variations on `Ioi a` and on `Ici a` coincide. We give a version relative to a set `s`. -/ diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean index 068df13358486f..9e38a83e04a892 100644 --- a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean +++ b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean @@ -1155,8 +1155,9 @@ theorem Real.Icc_eq_closedBall (x y : ℝ) : Icc x y = closedBall ((x + y) / 2) rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two, ← add_div, add_assoc, add_sub_cancel, add_self_div_two] +set_option linter.tacticAnalysis.verifyGrindOnly false in lemma Real.sphere_eq_pair (x : ℝ) {r : ℝ} (hr : 0 ≤ r) : sphere x r = {x - r, x + r} := by - ext; simp [dist_eq]; grind + ext; simp [dist_eq]; grind only [= abs, = max_def] theorem Metric.uniformity_eq_comap_nhds_zero : 𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ)) := by diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 8fee46ee739770..ff2ae512ed931d 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -153,6 +153,7 @@ instance tendstoIocClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioc ( instance tendstoIooClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) := tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self +set_option linter.tacticAnalysis.verifyGrindOnly false in variable (α) in /-- In a second countable topological space with the order topology, the topology is generated by half-infinite open intervals with endpoints in a countable set. -/ @@ -174,7 +175,7 @@ lemma exists_countable_generateFrom_Ioi_Iio grind [isOpen_Iio', isOpen_Ioi'] · rw [ht] apply generateFrom_anti - grind + grind only [= subset_def, usr mem_setOf_eq, = mem_image] /-- If a topology is generated by half-open intervals with endpoints in a set `c`, then the sets formed by intersecting finitely many of these intervals form a topological basis. -/ diff --git a/Mathlib/Topology/Order/IsLUB.lean b/Mathlib/Topology/Order/IsLUB.lean index 842814ea083a85..8507d7f3e39529 100644 --- a/Mathlib/Topology/Order/IsLUB.lean +++ b/Mathlib/Topology/Order/IsLUB.lean @@ -219,7 +219,8 @@ theorem Dense.ciSup' {α : Type*} [TopologicalSpace α] simpa [← Function.comp_def, range_comp] using hf.range_subset_closure_image_dense hS · suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h] contrapose h - grind [h.mono] + apply h.mono + grind /-- This is an analogue of `Dense.continuous_inf` for functions taking values in a conditionally complete linear order. The assumption of `BddBelow (range f)` is not needed in this theorem. -/ diff --git a/Mathlib/Topology/Order/WithTop.lean b/Mathlib/Topology/Order/WithTop.lean index 4ab8d877149915..e458df0c4eb91a 100644 --- a/Mathlib/Topology/Order/WithTop.lean +++ b/Mathlib/Topology/Order/WithTop.lean @@ -29,6 +29,7 @@ instance [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithTop ι instance [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithTop ι) := ⟨rfl⟩ +set_option linter.tacticAnalysis.verifyGrindOnly false in instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] : SecondCountableTopology (WithTop ι) := by classical @@ -56,15 +57,16 @@ instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopo #adaptation_note /-- Before leanprover/lean4#13166, this was just `grind`. The new canonicalizer using `isDefEq` less, and so does not unify as many of the conditions that `grind` wants to case split on. - Alternatively `ext; simp; grind` work here. -/ - grind (splits := 12) + One way to solve this is via `grind (splits := 12)` or alternatively `ext; simp; grind` + We squeeze here so that `grind?` also works. -/ + grind only [= mem_setOf_eq, = mem_union, = mem_image] rw [this] exact (d_count.image _).union (d_count.image _) -- We should check the easy direction that all the elements in our generating set are open. -- This is trivial as these are all intervals. apply le_antisymm · apply le_generateFrom_iff_subset_isOpen.2 - grind [isOpen_Iio', isOpen_Ioi'] + grind only [= setOf_subset_setOf, isOpen_Ioi', isOpen_Iio'] /- Now, let us check that our sets indeed generates the topology. As the topology is generated by the open half-infinite intervals by definition, we should check that open half-infinite intervals are covered by finite intersections of our sets. -/ diff --git a/Mathlib/Topology/Path.lean b/Mathlib/Topology/Path.lean index 13bbc3699273fe..8dc953b6c81cbc 100644 --- a/Mathlib/Topology/Path.lean +++ b/Mathlib/Topology/Path.lean @@ -473,10 +473,11 @@ theorem prod_coe (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t) := rfl +set_option linter.tacticAnalysis.verifyGrindOnly false in /-- Path composition commutes with products -/ theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂) := by - grind + grind only [= trans_apply, = prod_coe] end Prod diff --git a/Mathlib/Topology/Sets/VietorisTopology.lean b/Mathlib/Topology/Sets/VietorisTopology.lean index 0eaa904aa1b3e1..9eca784108e21b 100644 --- a/Mathlib/Topology/Sets/VietorisTopology.lean +++ b/Mathlib/Topology/Sets/VietorisTopology.lean @@ -489,14 +489,16 @@ instance [T2Space α] : T2Space (Compacts α) where rw [SetLike.not_le_iff_exists] at h' obtain ⟨x, hx₁, hx₂⟩ := h' obtain ⟨U, V, hU, hV, hU', hV', hUV⟩ := K₂.isCompact.separation_of_notMem hx₂ + have := @not_disjoint_iff_nonempty_inter α exact ⟨_, _, isOpen_inter_nonempty_of_isOpen hV, isOpen_subsets_of_isOpen hU, ⟨x, hx₁, hV'⟩, - hU', by grind [Set.Nonempty]⟩ + hU', by grind⟩ @[simp] theorem t2Space_iff : T2Space (Compacts α) ↔ T2Space α := ⟨fun _ => isEmbedding_singleton.t2Space, fun _ => inferInstance⟩ instance [RegularSpace α] : RegularSpace (Compacts α) := by + have := @not_disjoint_iff_nonempty_inter α simp_rw [regularSpace_generateFrom induced_generateFrom_eq, image_union, image_image, powerset, preimage_setOf_eq, Filter.disjoint_iff] rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩) K hK @@ -504,7 +506,7 @@ instance [RegularSpace α] : RegularSpace (Compacts α) := by SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl (disjoint_compl_right_iff_subset.mpr hK) refine ⟨{K | (↑K ∩ W).Nonempty}, ?_, {K | ↑K ⊆ V}, - (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind [Set.Nonempty]⟩ + (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind⟩ simp_rw [(isOpen_inter_nonempty_of_isOpen hW).mem_nhdsSet, compl_setOf, ← inter_compl_nonempty_iff] grw [hUW] @@ -512,7 +514,7 @@ instance [RegularSpace α] : RegularSpace (Compacts α) := by obtain ⟨V, W, hV, hW, hxV, hUW, hVW⟩ := SeparatedNhds.of_isCompact_isClosed (isCompact_singleton (x := x)) hU.isClosed_compl (by simpa) - refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩ + refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind⟩ · simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_setOf, not_nonempty_iff_eq_empty, ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right] gcongr diff --git a/Mathlib/Topology/Sheaves/Flasque.lean b/Mathlib/Topology/Sheaves/Flasque.lean index 0373d0092eaa2f..9622df3f242909 100644 --- a/Mathlib/Topology/Sheaves/Flasque.lean +++ b/Mathlib/Topology/Sheaves/Flasque.lean @@ -80,6 +80,7 @@ an open `V` and a section of `F(V)` that maps to `s |_ V` via `g`. -/ abbrev Under := StructuredArrow ⟨op U, s⟩ (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat.{u})).mapElements +set_option linter.tacticAnalysis.verifyGrindOnly false in set_option backward.isDefEq.respectTransparency false in /- The next lemma proves that the relation `fun x y ↦ Nonempty (y ⟶ x)` on `Under g s` satisfies the requirements for applying Zorn's lemma -/ @@ -89,7 +90,7 @@ lemma structured_arrows_elements_sheaf_chains_bounded (c : Set (Under g s)) obtain ⟨t, ht, _⟩ : ∃! s_1, IsGluing F.obj f (fun x => x.val.right.2) s_1 := by refine Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_) obtain (rfl | h₁ | h₁) : i = j ∨ Nonempty (i.val ⟶ j.val) ∨ Nonempty (j.val ⟶ i.val) := by - grind [Subtype.ext_iff, h i.property j.property] + grind only [Subtype.ext_iff, h i.property j.property] · rfl all_goals rw [← CategoryOfElements.map_snd h₁.some.2]