Proving Filter.ext_iff

Stream: lean4

[Utensil Song]

I was trying out https://github.com/bridgekat/filter-game and proving Filter.ext_iff in it, by following only the hints given by Lean and this tactics cheat sheet, I got the 2nd proof Filter.ext_iff'' in the following #mwe, it's much more verbose than the 1st simple proof:

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Order.Filter.Basic

theorem Filter.ext_iff₁ (f g : Filter α) : f = g ↔ (∀ s, s ∈ f ↔ s ∈ g) := by
  simp only [filter_eq_iff, Set.ext_iff, Filter.mem_sets]

theorem Filter.ext_iff₂ (f g : Filter α) : f = g ↔ (∀ s, s ∈ f ↔ s ∈ g) := by
  apply Iff.intro
  . intro f_eq_g
    intro s
    apply Iff.intro
    . intro s_mem_f
      rw [<-f_eq_g]
      exact s_mem_f
    . intro s_mem_g
      rw [f_eq_g]
      exact s_mem_g
  . intro set_mem_iff
    rw [filter_eq_iff]
    rw [Set.ext_iff]
    intro s
    specialize set_mem_iff s
    rw [Filter.mem_sets]
    exact set_mem_iff

My question is:

1. Is there somewhere between these 2 proofs that's idiomatic and also down to the basics?
2. How could I realize that the proof can be a simp only with a few lemmas when simp? made no progress? Can simp somehow give some hints about what shapes of the assumptions and goals it faced right before it gave up so that I might figure out the lemmas?

[Damiano Testa]

I am not sure about the Filter proof, since I never really worked with filters.

As for simp, when it fails, it means that it tried all simp lemmas and was able to apply none. This means that place where it was when it failed is exactly where you are.

The other question, about what lemmas to add, that is very dependent on context and if there were a good automation for that, more proof would be easier to formalize!

[Utensil Song]

Thanks for your answer~

I'm asking Q1 because I wonder how experts simplify their proofs in general. This is a simple proof which uses little knowledge about filters but lots of basics of Lean 4. So it could be a good example for discussion.

By Q2, I imagine simp (or other automation tactics, e.g. aesop) would know its search depth and evaluate the complexity of the remaining goals and can provide useful insight even in failure.

[Utensil Song]

I also would like to share my experience about places where I thought Lean 4 would help me (from my Lean 3 experience) but instead I was confused:

1. When I typed the first line of the theorem that ends with by, I got unexpected end of input; expected '{' but expected to feel normal inside the tactic mode
2. Whey I typed the dot after apply Iff.intro, I got the same error
3. When I typed the dot in a new line with the right indentation, I got 1 goal in Tactic State, and an error "unsolved goals" in "Messages", which is a duplication of the goal in Tactic State, then I need to collapse it to avoid visual influence
4. When I typed the first dot line such as . intro s_mem_f (which has 1 tactic and should leave unresolved goals) and enter, I got an indentation aligned with the dot, so that Lean is not giving me goals within the case after the tactic, so I have to figure out I need to indent to be back in the case to see the effect of the first line
5. When I typed exact s_mem_g and enter, I end up in a new line indented within the case, and Tactic State is saying "No gaols", but code has error underlines, I have to expand "All messages" (which usually contain duplicated messages, so I collapse them to avoid visual influence) to see the rest of goals. Again I realized that I need to un-indent to get hints back in Tactic State
6. When I'm after rw [filter_eq_iff], I have no idea how to proceed exactly, I know I need an iff from Set, but I have no hints from Lean if I typed rw [Set., so I have to guess it by name convetion
7. Whenever I want to intro with a single letter, the auto complete would always change my letter e.g. s into something that already existed like S, I have to click or hit Esc to avoid the change before I hit enter to change to the new line
8. When I typed specialize, Lean seemed to accept it with no argument, but it made no progress, I kind of hoped that I can have some hints for the arguments, but no, so I read the hover doc, and fill the 1st argument, then I really don't know what to do next, what kind of expression should I provide? No hints, I have to use my intro mind to fill the 2nd argument (Strangely, this time the autocomplete is not change my s)
9. Finally, when I'm at the end of the line exact set_mem_iff, I got no error but also I saw a "goal" in the infoview, I thought I haven't finished, but when I enter, the new line gives me a clean "No goals", I went back and realized that the goal is in the "Expected Type", it shadows me from seeing "No goals" in "Tactic state".

[Utensil Song]

With the help of #explode, I have managed to get somewhere in between:

theorem Filter.ext_iff₃ (f g : Filter α) : f = g ↔ (∀ s, s ∈ f ↔ s ∈ g) := by
  calc
    (f = g) ↔ (f.sets = g.sets)                           := by rw [filter_eq_iff]
          _ ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets      := by rw [Set.ext_iff]
          _ ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g                := by simp_rw [Filter.mem_sets]

However, I can't make simp_rw go away with more explicit form without increasing the "step count" in #explode, nor can I get "step count" close to 19 in an explicit form.

-- 19
#explode Filter.ext_iff₁

-- 38
#explode Filter.ext_iff₂

-- 31
#explode Filter.ext_iff₃

My attempts and the #explode tables can be view here . Any hint would be appreciated. :thank_you: