What `grind` does?

Stream: general

[Nick_adfor]

I have a piece of code. But I'm wondering what grind does. grind? does not like aesop that will generate simp and refine, grind? can only generate grind only, which still makes me confusing what grind do. I hope I can check it in a simp or refine way.

import Mathlib


/--
There does not exist an infinite σ-algebra that contains only countably many members.

This theorem states that it is impossible to have a σ-algebra that is both infinite
and countable. The proof proceeds by contradiction, showing that any infinite σ-algebra
must contain at least continuum many sets.
-/
theorem not_exists_infinite_countable_sigma_algebra :
    ¬ ∃ (α : Type) (i : MeasurableSpace α),
      Set.Countable {s : Set α | @MeasurableSet α i s} ∧
      Set.Infinite {s : Set α | @MeasurableSet α i s} := by
  -- Assume by contradiction that such a σ-algebra exists
  by_contra h_contra
  obtain ⟨α, i, h_countable, h_infinite⟩ := h_contra

  -- Define an equivalence relation: x ~ y if they belong to the same measurable sets
  set eqv : α → α → Prop := fun x y => ∀ s : Set α, MeasurableSet s → (x ∈ s ↔ y ∈ s)

  -- Each equivalence class is measurable (can be expressed as countable intersections)
  have h_partition : ∀ x : α, MeasurableSet {y : α | eqv x y} := by
    intro x
    -- Express the equivalence class as an intersection over measurable sets containing x
    -- and complements of measurable sets not containing x
    have h_eqv_class : {y : α | eqv x y} = ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x ∈ s}, s ∩ ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x∉s}, sᶜ := by
      ext y; aesop (config := {warnOnNonterminal := false})
      specialize a sᶜ; aesop (config := {warnOnNonterminal := false})
    rw [h_eqv_class]
    -- The intersection is measurable since it's over countably many measurable sets
    refine' MeasurableSet.biInter _ _ <;> aesop (config := {warnOnNonterminal := false})
    exact h_countable.mono fun s hs => hs.1
    -- Countability of the indexing set for complements
    have h_countable_inter : Set.Countable {s : Set α | MeasurableSet s ∧ x∉s} := by
      exact h_countable.mono fun s hs => hs.1
    exact MeasurableSet.inter left (MeasurableSet.biInter h_countable_inter fun s hs => MeasurableSet.compl hs.1)

  -- The σ-algebra is generated by the equivalence classes
  have h_sigma_gen : ∀ s : Set α, MeasurableSet s ↔ ∃ t : Set (Set α), t ⊆ { {y : α | eqv x y} | x : α } ∧ s = ⋃₀ t := by
    aesop (config := {warnOnNonterminal := false})
    · -- Forward direction: every measurable set is a union of equivalence classes
      use { { y : α | eqv x y } | x ∈ s }
      aesop (config := {warnOnNonterminal := false})
    · -- Reverse direction: any union of equivalence classes is measurable
      have h_measurable_w : ∀ s ∈ w, MeasurableSet s := by
        intro s hs
        specialize left hs
        aesop (config := {warnOnNonterminal := false})
      -- Countability of the indexing set
      have h_countable_w : w.Countable := by
        exact h_countable.mono h_measurable_w
      exact MeasurableSet.sUnion h_countable_w h_measurable_w

  -- The set of equivalence classes must be finite
  have h_eq_classes_finite : Set.Finite { {y : α | eqv x y} | x : α } := by
    by_cases h_eq_classes_infinite : Set.Infinite { {y : α | eqv x y} | x : α }
    · -- If equivalence classes were infinite, the power set would be uncountable
      have h_power_set_uncountable : ¬Set.Countable (Set.powerset { {y : α | eqv x y} | x : α }) := by
        intro h_power_set_countable
        -- Show that the power set has cardinality at least continuum
        have h_power_set_card : Cardinal.mk (Set.powerset { {y : α | eqv x y} | x : α }) ≤ Cardinal.aleph0 := by
          exact Cardinal.mk_le_aleph0_iff.mpr h_power_set_countable.to_subtype
        simp [*] at *
        -- Cantor's theorem gives contradiction with countability
        have h_card_ge_aleph0 : Cardinal.mk { {y : α | eqv x y} | x : α } ≥ Cardinal.aleph0 := by
          exact Cardinal.aleph0_le_mk_iff.mpr (h_eq_classes_infinite.to_subtype)
        exact h_power_set_card.not_gt (lt_of_lt_of_le (Cardinal.cantor _) (Cardinal.power_le_power_left two_ne_zero h_card_ge_aleph0))
      -- But the power set injects into our σ-algebra, contradicting countability
      apply_mod_cast False.elim <| h_power_set_uncountable <| Set.Countable.mono _ <| h_countable.image _
      use fun s => { t | ∃ x ∈ s, { y | eqv x y } = t }
      intro t ht
      use ⋃₀ t
      simp_all [Set.ext_iff]
      refine' ⟨⟨t, ht, fun x => Iff.rfl⟩, fun x => ⟨fun hx => _, fun hx => _⟩⟩
      · -- Show x is in the appropriate equivalence class
        obtain ⟨y, ⟨z, hz, hyz⟩, hy⟩ := hx
        convert hz
        obtain ⟨x_1, hx_1⟩ : ∃ x_1 : α, z = {y | eqv x_1 y} := by
          obtain ⟨x_1, hx_1⟩ := ht hz
          exact ⟨x_1, by ext; simp [hx_1]⟩
        ext
        simp [hx_1]
        -- Calculation
        have h_eqv_x1_y : eqv x_1 y := by
          exact hx_1.subset hyz
        constructor
        · intro hx_mem s hs_meas
          constructor
          · intro hx1_in_s
            have h_y_in_s : y ∈ s := by
              -- Since $x_1$ and $y$ are equivalent, by definition of $eqv$, we have $x_1 \in s \leftrightarrow y \in s$.
              have hy_in_s : x_1 ∈ s ↔ y ∈ s := by
                apply h_eqv_x1_y s hs_meas;
              -- Apply the equivalence from hy_in_s to hx1_in_s to conclude y is in s.
              apply hy_in_s.mp hx1_in_s
            -- Since eqv y x✝ holds, for any measurable set s, y ∈ s ↔ x✝ ∈ s. Given that y ∈ s, it follows that x✝ ∈ s.
            have h_eqv_y_x : ∀ s : Set α, MeasurableSet s → (y ∈ s ↔ ‹α› ∈ s) := by
              -- Since y and x✝ are in the same equivalence class under eqv, by definition of eqv, this equivalence holds for all measurable sets s.
              intros s hs_meas; exact (hy ‹_›).mpr hx_mem s hs_meas;
            exact h_eqv_y_x s hs_meas |>.1 h_y_in_s
          · intro hx_in_s
            have h_y_in_s : y ∈ s := by
              have hy_in_s : x_1 ∈ s ↔ y ∈ s := by
                apply h_eqv_x1_y s hs_meas;
              grind +ring
            apply (h_eqv_x1_y s hs_meas).mpr h_y_in_s
        · intro h_eqv_x1_x
          have h_eqv_y_x1 : eqv y x_1 := by
            -- Since eqv is symmetric, if eqv x_1 y holds, then eqv y x_1 must also hold.
            have h_symm : ∀ x y, eqv x y → eqv y x := by
              -- Since eqv is symmetric, if eqv x y holds, then eqv y x must also hold. This follows directly from the definition of eqv.
              intros x y h_eqv_xy
              intro s hs
              rw [h_eqv_xy s hs];
            exact h_symm _ _ h_eqv_x1_y
          have h_trans : ∀ a b c, eqv a b → eqv b c → eqv a c := by
            intro a b c hab hbc s hs_meas
            constructor
            · intro ha_in
              exact (hbc s hs_meas).1 ((hab s hs_meas).1 ha_in)
            · intro hc_in
              exact (hab s hs_meas).2 ((hbc s hs_meas).2 hc_in)
          grind

      · -- Show the reverse inclusion
        obtain ⟨y, hy⟩ := ht hx
        simp +zetaDelta at *;
        exact ⟨ y, ⟨ x, hx, by simpa using hy y ⟩, fun z => by simpa [ eq_comm ] using hy z ⟩;
    · -- Case when equivalence classes are finite
      exact Classical.not_not.mp h_eq_classes_infinite

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by
    exact Set.Finite.subset (Set.Finite.powerset h_eq_classes_finite) fun t ht => ht

  -- Therefore the σ-algebra (unions of subsets) is finite
  have h_measurable_finite : Set.Finite (Set.image (fun t : Set (Set α) => ⋃₀ t) {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }}) := by
    exact h_subsets_finite.image _

  -- This contradicts the assumption that the σ-algebra is infinite
  exact h_infinite (h_measurable_finite.subset fun s hs => by
    obtain ⟨t, ht, rfl⟩ := h_sigma_gen s |>.1 hs
    exact Set.mem_image_of_mem _ ht)

[Julian Berman]

I think when asking this question it's probably important that you continue to include the context that you are (presumably) trying to backport this proof to early versions of Lean as you mentioned elsewhere. In particular, grind is a tactic, and a shiny new one that's doing a bunch of different things which are not going to be easily representable using other tactics in a drop-in way.

[Nick_adfor]

So it's hard to express it in a simp or refine way : (

[Julian Berman]

Correct. grind can do lots more than that as evidenced by all the pull requests which golf long pieces of proofs with short single calls to grind.

[Kim Morrison]

There is a section of the reference manual about what grind is doing. Please read it and let us know if you have suggestions for improvement!

May I ask why you are trying to backport something to an earlier toolchain version?

[Matt Diamond]

@Kim Morrison this thread has some background:
#new members > Chebyshev polynomial @ 💬