Proving set-related theorems using `aesop`

Stream: lean4

[Ilmārs Cīrulis]

My try.

import Mathlib

theorem my_theorem: ∀ (s : Set (ℕ × ℕ)) (fst: ℕ) (e1: ℕ),
    {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬x.2 = e1} = insert (fst, e1) {x | x ∈ s ∧ ¬x.2 = e1} → False := by
  intros s fst e1 H
  have H0 : (fst, e1) ∉ {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬ x.2 = e1} := by
    intros H1
    simp at H1
  have H1 : (fst, e1) ∈ insert (fst, e1) {x | x ∈ s ∧ ¬ x.2 = e1} := by
    simp
  aesop
 ```

[Ilmārs Cīrulis]

Anyway, this probably belongs to "new members" or maybe "general".

[Kim Morrison]

Assuming #29495 goes through, it becomes just:

theorem my_theorem (s : Set (ℕ × ℕ)) (fst : ℕ) (e1 : ℕ) :
    {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬x.2 = e1} ≠ insert (fst, e1) {x | x ∈ s ∧ ¬x.2 = e1} := by
  have H0 : (fst, e1) ∉ {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬ x.2 = e1} := by grind
  grind

[Robin Arnez]

(the discussion continued at #new members > Proving set-related theorems using `aesop`)