exact? gives incorrect line-wrapping

Stream: mathlib4

[Nick_adfor]

I can never think of the reason is exact? gives

Try this:
  (expose_names;
        exact Subgroup.Normal.conj_mem' inst_1 h₁ hh₁ g')

But in fact it should be

Try this:
  (expose_names; exact Subgroup.Normal.conj_mem' inst_1 h₁ hh₁ g')

It's because of a line break issue, exact?gives a line break.

[Nick_adfor]

It's another disaster that lean will recommend me to gives a line break as

This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`

But (expose_names; exact Subgroup.Normal.conj_mem' inst_1 h₁ hh₁ g') cannot have any line break...

[Eric Wieser]

@Nick_adfor, can you move the issue about exact? to a new thread? edit your first post to give some context, now that I've moved this?

[Notification Bot]

3 messages were moved here from #mathlib4 > Define Quotient Group by Eric Wieser.

[Eric Wieser]

I think ultimately the problem is that "try this" doesn't know the difference between

have := by exact?

and

have := by
  exact?

since your substitution only works in the second case

[Nick_adfor]

Since it is a new definition about Quotient Group, the code might be long.

import Mathlib

suppress_compilation -- This makes some noncomputable def work.

variable {G : Type} [Group G] (H : Subgroup G) [H.Normal]

open Pointwise

structure QGroup : Type where
  carrier : Set G
  isCoset : ∃ g : G, carrier = g • H

namespace QGroup

variable {H}

instance : SetLike (QGroup H) G where
  coe C := C.carrier
  coe_injective' := by
    intro C D; cases C; cases D; simp

@[ext]
lemma ext {C D : QGroup H} (h : (C : Set G) = D) : C = D := by
  cases C; cases D; simp at h; simp [h]

def out (C : QGroup H) : G := Classical.choose C.isCoset

@[simp]
lemma out_spec (C : QGroup H) : C.out • H = (C : Set G) :=
  Classical.choose_spec C.isCoset |>.symm

lemma mem_iff_out (C : QGroup H) (g : G) : g ∈ C ↔ ∃ h ∈ H, g = C.out • h := by
  rw [← SetLike.mem_coe, ← C.out_spec, Set.mem_smul_set]
  tauto

variable (H) in
def gen (g : G) : QGroup H :=
  ⟨g • H, ⟨g, rfl⟩⟩


lemma gen_def (g : G) : (gen H g : Set G) = g • H := rfl

@[simp]
lemma mem_gen_iff (g : G) {x : G} : x ∈ gen H g ↔ ∃ h ∈ H, x = g * h := by
  rw [← SetLike.mem_coe, gen_def, Set.mem_smul_set]
  tauto

@[simp]
lemma gen_out (C : QGroup H) : gen H C.out = C := by
  ext g
  simp only [SetLike.mem_coe, mem_gen_iff]
  rw [C.mem_iff_out]
  rfl

@[simp]
lemma mem_out_gen (g : G) {x : G} : x ∈ ((gen H g).out • H : Set G) ↔ x ∈ (g • H : Set G) := by
  simp [Set.mem_smul_set, eq_comm]

@[elab_as_elim]
theorem gen_induction {P : QGroup H → Prop}
    (h : ∀ g : G, P (gen H g)) :
    ∀ C : QGroup H, P C := by
  intro C
  rw [← C.gen_out]
  tauto

@[simp]
theorem gen_eq_iff (g : G) (C : QGroup H) : gen H g = C ↔ g ∈ C := by
  constructor
  · rintro rfl
    simp
  · intro h
    rw [C.mem_iff_out] at h
    obtain ⟨x, hx, rfl⟩ := h
    ext y
    simp only [smul_eq_mul, SetLike.mem_coe, mem_gen_iff]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [C.mem_iff_out]
      use x * y, mul_mem hx hy
      simp [mul_assoc]
    · rw [C.mem_iff_out]
      rintro ⟨y, hy, rfl⟩
      use x⁻¹ * y, mul_mem (H.inv_mem hx) hy
      simp [mul_assoc]

instance : One (QGroup H) where
  one := ⟨H, ⟨1, by simp⟩⟩

lemma one_def : ((1 : QGroup H) : Set G) = H := rfl

@[simp]
lemma mem_one_iff {g : G} : g ∈ (1 : QGroup H) ↔ g ∈ H := Iff.rfl

@[simp]
lemma gen_one : gen H 1 = 1 := by
  ext g
  simp

instance : Mul (QGroup H) where
  mul C D := ⟨C.out • D.out • H, ⟨C.out * D.out, by simp [mul_smul, out_spec]⟩⟩

lemma mul_def (C D : QGroup H) :
    ((C * D : QGroup H) : Set G) = C.out • D.out • H := rfl

@[simp]
lemma gen_mul_gen (g g' : G) : gen H g * gen H g' = gen H (g * g') := by
  ext x
  simp only [SetLike.mem_coe, mul_def, gen_def, Set.mem_smul_set]
  constructor
  · rintro ⟨w, hw, rfl⟩
    obtain ⟨h₂, hh₂, rfl⟩ := hw
    have mem1 : (gen H g).out ∈ (gen H g).out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem1
    rw [Set.mem_smul_set] at mem1
    obtain ⟨h₁, hh₁, h_eq1⟩ := mem1
    have mem2 : (gen H g').out ∈ (gen H g').out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem2
    rw [Set.mem_smul_set] at mem2
    obtain ⟨k, hk, h_eq2⟩ := mem2
    rw [<-h_eq1, <-h_eq2]
    use (g'⁻¹ * h₁ * g') * (k * h₂)
    constructor
    · have hh₁' : h₁ ∈ H := hh₁
      have hk' : k ∈ H := hk
      have conj_mem : g'⁻¹ * h₁ * g' ∈ H := by exact?
      have mul_mem1 : k * h₂ ∈ H := by exact (Subgroup.mul_mem_cancel_right H hh₂).mpr hk
      exact mul_mem conj_mem mul_mem1
    · simp [mul_assoc]
  · sorry

[Eric Wieser]

I think this is lean4#10150

[Nick_adfor]

Eric Wieser said:

I think ultimately the problem is that "try this" doesn't know the difference between

have := by exact?

and

have := by
  exact?

since your substitution only works in the second case

Yes, if I write by and exact? in two lines, it will work.

      have conj_mem : g'⁻¹ * h₁ * g' ∈ H := by
        exact?

[Jovan Gerbscheid]

@Eric Wieser, isn't that issue about tacticSeq specifically? exact? suggests a tactic as far as I can see.

[Eric Wieser]

Indeed, but the last message before mine is actually about tactic

[Nick_adfor]

I'll give another example here.

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
            -- y 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
            -- y in s
            have h_y_in_s : y ∈ s := by
              have h_x1_in_s : x_1 ∈ s := by
                rw [Set.subset_def] at ht
                apply ?_
                have h_y_eq_xstar : ∀ (u : Set α), MeasurableSet u → (y ∈ u ↔ x_1 ∈ u) := by exact?
                have h_x1_iff_y : ∀ (u : Set α), MeasurableSet u → (x_1 ∈ u ↔ y ∈ u) := by exact?
                grind?
              have h_x1_iff_y : x_1 ∈ s ↔ y ∈ s := h_eqv_x1_y s hs_meas
              exact h_x1_iff_y.1 h_x1_in_s
            apply (h_eqv_x1_y s hs_meas).mpr h_y_in_s
        · intro h_eqv_x1_x
          -- calculation
          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
          -- calculation
          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)
          show_term 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)

  #print not_exists_infinite_countable_sigma_algebra._proof_1_9

[Jovan Gerbscheid]

To be clear, the posted example is equivalent to the following:

example (aaaaaaaaaaaaaaaaa b : Rat) : aaaaaaaaaaaaaaaaa + b = b + aaaaaaaaaaaaaaaaa := by exact?

which then produced this invalid proof:

example (aaaaaaaaaaaaaaaaa b : Rat) : aaaaaaaaaaaaaaaaa + b = b + aaaaaaaaaaaaaaaaa := by exact
  Rat.add_comm aaaaaaaaaaaaaaaaa b

[Nick_adfor]

Jovan Gerbscheid said:

To be clear, the posted example is equivalent to the following:

example (aaaaaaaaaaaaaaaaa b : Rat) : aaaaaaaaaaaaaaaaa + b = b + aaaaaaaaaaaaaaaaa := by exact?

which then produced this invalid proof:

example (aaaaaaaaaaaaaaaaa b : Rat) : aaaaaaaaaaaaaaaaa + b = b + aaaaaaaaaaaaaaaaa := by exact
  Rat.add_comm aaaaaaaaaaaaaaaaa b

So what happened to

have h_y_eq_xstar : ∀ (u : Set α), MeasurableSet u → (y ∈ u ↔ x_1 ∈ u) := by exact
                  fun u a => (fun {a b} => iff_comm.mp) (h_eqv_x1_y u a)

[Jovan Gerbscheid]

The issue is that we'd like exact? to realize that it should put the exact on the next line. I don't know how to fix this, but I don't think it is a big problem.

[Nick_adfor]

This is still about the line-breaking issue... exact? doesn’t generate content with automatic line breaks — I have to manually split by and exact onto two separate lines.

[Nick_adfor]

have h_y_eq_xstar : ∀ (u : Set α), MeasurableSet u → (y ∈ u ↔ x_1 ∈ u) := by exact
                  fun u a => (fun {a b} => iff_comm.mp) (h_eqv_x1_y u a)

should be

have h_y_eq_xstar : ∀ (u : Set α), MeasurableSet u → (y ∈ u ↔ x_1 ∈ u) := by
   exact fun u a => (fun {a b} => iff_comm.mp) (h_eqv_x1_y u a)

[Jovan Gerbscheid]

Another related item on the exact? TODO list is to remove the by and the exact if possible.

[Nick_adfor]

One more exact? problem here.

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]⟩
        -- The root of all evil is `ext`. `ext` generates an implicit variable `x✝`, and implicit variables like `x✝` cannot be included in the statement — expressions such as `eqv y x✝` are invalid. Therefore, it should be replaced with an explicit variable: `apply Set.ext; intro w`.
        apply Set.ext
        intro w
        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
            -- y 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 w holds, for any measurable set s, y ∈ s ↔ w ∈ s. Given that y ∈ s, it follows that w ∈ s.
            have h_eqv_y_x : ∀ s : Set α, MeasurableSet s → (y ∈ s ↔ ‹α› ∈ s) := by
              -- Since y and w 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
            -- y in s
            have h_y_in_s : y ∈ s := by
              -- Since eqv x_1 y holds, for any measurable set s, x_1 ∈ s ↔ y ∈ s. Given that x_1 ∈ s, it follows that y ∈ s.
              have h_eqv_y_w : eqv y w := (hy w).2 hx_mem
              -- Calculation
              have h_eqv_x1_w : eqv x_1 w := by
                intro s' hs'
                -- Calculation
                have h1 := h_eqv_x1_y s' hs'
                -- Calculation
                have h2 := h_eqv_y_w s' hs'
                constructor
                · intro hx1; exact h2.1 (h1.1 hx1)
                · intro hw; exact h1.2 (h2.2 hw)
              -- Calculation
              have h_x1_in_s : x_1 ∈ s := (h_eqv_x1_w s hs_meas).2 hx_in_s
              exact (h_eqv_x1_y s hs_meas).1 h_x1_in_s
            apply (h_eqv_x1_y s hs_meas).mpr h_y_in_s
        · intro h_eqv_x1_w
          -- Calculation
          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 x_1 y h_eqv_x1_y
          -- Calculation
          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)
          -- Calculation
          have h_eqv_y_w : eqv y w := h_trans y x_1 w h_eqv_y_x1 h_eqv_x1_w
          exact ((hy w).1 h_eqv_y_w)
      · -- 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?

  -- 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)

[Nick_adfor]

The following can work. Maybe exact? do not generate any implicit argument

  -- 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 _

[Jovan Gerbscheid]

Instead of pasting a large amount of code and expecting others to find which part to look at, could you post a small #mwe? This is what I did for your previous message.

[Nick_adfor]

Jovan Gerbscheid said:

Instead of pasting a large amount of code and expecting others to find which part to look at, could you post a small #mwe? This is what I did for your previous message.

It really cannot. Because this part is in the ending part of the proof of this theorem. So the mwe is nearly itself.

[Nick_adfor]

But if you can accept, I can admit one

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)

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by admit

  -- 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?

[Jovan Gerbscheid]

It would also be helpful if you described in your message what the current behaviour is, in addition to what you want it to be. I'm on mobile right now so I can't paste the code into the web editor.

[Nick_adfor]

exact? shows an ambiguous ⋃₀

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)

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by admit

  -- 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 Set.Finite.image (fun t => ⋃₀ t) h_subsets_finite

[Aaron Liu]

what's the error?

[Nick_adfor]

Nick_adfor said:

But if you can accept, I can admit one

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)

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by admit

  -- 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?

As one can see, this part exact? generate something cannot work.

[Aaron Liu]

what error do you get

[Aaron Liu]

what's the error message

[Kim Morrison]

You mean "cannot work, except if the user fixes some whitespace", I think? If that is the case, then this essentially has nothing to do with exact? itself, and is just known deficiencies in the pretty-printer that exact? relies on. The pretty-printer is currently being actively worked on, so we'll see if things get better with that.