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

theorem Filter.ext_iff₁: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₁ (f: Filter α
f g: Filter α
g : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : f: Filter α
f = g: Filter α
g ↔ (∀ s: Set α
s, s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ g: Filter α
g) := byGoals accomplished! 🐙
  simp only [filter_eq_iff: ∀ {α : Type ?u.14} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iff, Set.ext_iff: ∀ {α : Type ?u.15} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
Set.ext_iff, Filter.mem_sets: ∀ {α : Type ?u.16} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
Filter.mem_sets]Goals accomplished! 🐙

theorem Filter.ext_iff₂: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₂ (f: Filter α
f g: Filter α
g : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : f: Filter α
f = g: Filter α
g ↔ (∀ s: Set α
s, s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ g: Filter α
g) := byGoals accomplished! 🐙
  apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introα: Type u_1
f, g: Filter α
mpf = g → ∀ (s : Set α), s ∈ f ↔ s ∈ g
α: Type u_1
f, g: Filter α
mpr(∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
  .α: Type u_1
f, g: Filter α
mpf = g → ∀ (s : Set α), s ∈ f ↔ s ∈ g intro f_eq_g: f = g
f_eq_gWarning: Try this: intro f_eq_g s
α: Type u_1
f, g: Filter α
f_eq_g: f = g
mp∀ (s : Set α), s ∈ f ↔ s ∈ g
    intro s: Set α
sWarning: Try this: intro f_eq_g s
α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
mps ∈ f ↔ s ∈ g
    apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introWarning: Try this: intro f_eq_g s
α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
mp.mps ∈ f → s ∈ g
α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
mp.mprs ∈ g → s ∈ f
    .α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
mp.mps ∈ f → s ∈ g intro s_mem_f: s ∈ f
s_mem_fα: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_f: s ∈ f
mp.mps ∈ g
      rw [α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_f: s ∈ f
mp.mps ∈ g<-f_eq_g: f = g
f_eq_gα: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_f: s ∈ f
mp.mps ∈ f]α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_f: s ∈ f
mp.mps ∈ f
      exact s_mem_f: s ∈ f
s_mem_fGoals accomplished! 🐙
    .α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
mp.mprs ∈ g → s ∈ f intro s_mem_g: s ∈ g
s_mem_gα: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_g: s ∈ g
mp.mprs ∈ f
      rw [α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_g: s ∈ g
mp.mprs ∈ ff_eq_g: f = g
f_eq_gα: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_g: s ∈ g
mp.mprs ∈ g]α: Type u_1
f, g: Filter α
f_eq_g: f = g
s: Set α
s_mem_g: s ∈ g
mp.mprs ∈ g
      exact s_mem_g: s ∈ g
s_mem_gGoals accomplished! 🐙
  .α: Type u_1
f, g: Filter α
mpr(∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g intro set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
set_mem_iffα: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mprf = g
    rw [α: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mprf = gfilter_eq_iff: ∀ {α : Type u_1} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iffα: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mprf.sets = g.sets]α: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mprf.sets = g.sets
    rw [α: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mprf.sets = g.setsSet.ext_iff: ∀ {α : Type u_1} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
Set.ext_iffα: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mpr∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets]α: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
mpr∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
    intro s: Set α
sα: Type u_1
f, g: Filter α
set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
s: Set α
mprs ∈ f.sets ↔ s ∈ g.sets
    specialize set_mem_iff: ∀ (s : Set α), s ∈ f ↔ s ∈ g
set_mem_iff s: Set α
sα: Type u_1
f, g: Filter α
s: Set α
set_mem_iff: s ∈ f ↔ s ∈ g
mprs ∈ f.sets ↔ s ∈ g.sets
    exact set_mem_iff: s ∈ f ↔ s ∈ g
set_mem_iffGoals accomplished! 🐙

theorem Filter.ext_iff₃: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₃ (f: Filter α
f g: Filter α
g : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : f: Filter α
f = g: Filter α
g ↔ (∀ s: Set α
s, s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ g: Filter α
g) := byGoals accomplished! 🐙
  calcα: Type u_1
f, g: Filter α
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
    (f: Filter α
f = g: Filter α
g) ↔ (f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets = g: Filter α
g.sets: {α : Type u_1} → Filter α → Set (Set α)
sets)                           := byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
f = g ↔ f.sets = g.setsfilter_eq_iff: ∀ {α : Type u_1} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iffα: Type u_1
f, g: Filter α
f.sets = g.sets ↔ f.sets = g.sets]Goals accomplished! 🐙
          _: Prop_: Prop
_ ↔ ∀ (x: Set α
x : Set: Type u_1 → Type u_1
Set α: Type u_1
α), x: Set α
x ∈ f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets ↔ x: Set α
x ∈ g: Filter α
g.sets: {α : Type u_1} → Filter α → Set (Set α)
sets      := byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.setsSet.ext_iff: ∀ {α : Type u_1} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
Set.ext_iffα: Type u_1
f, g: Filter α
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets]Goals accomplished! 🐙
          _: Prop_: Prop
_ ↔ ∀ (x: Set α
x : Set: Type u_1 → Type u_1
Set α: Type u_1
α), x: Set α
x ∈ f: Filter α
f ↔ x: Set α
x ∈ g: Filter α
g                := byGoals accomplished! 🐙 simp_rwα: Type u_1
f, g: Filter α
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g [α: Type u_1
f, g: Filter α
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ gFilter.mem_sets: ∀ {α : Type ?u.44} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
Filter.mem_setsGoals accomplished! 🐙]Goals accomplished! 🐙

theorem Filter.ext_iff₄: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₄ (f: Filter α
f g: Filter α
g : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : f: Filter α
f = g: Filter α
g ↔ (∀ s: Set α
s, s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ g: Filter α
g) := byGoals accomplished! 🐙
  have mem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
mem_sets_eq_mem: ∀ (fg: Filter α
fg : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) (x: Set α
x : Set: Type u_1 → Type u_1
Set α: Type u_1
α), (x: Set α
x ∈ fg: Filter α
fg.sets: {α : Type u_1} → Filter α → Set (Set α)
sets) = (x: Set α
x ∈ fg: Filter α
fg) :=α: Type u_1
f, g: Filter α
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙
    intros fg: Filter α
fg x: Set α
xα: Type u_1
f, g, fg: Filter α
x: Set α
(x ∈ fg.sets) = (x ∈ fg)
    rw [α: Type u_1
f, g, fg: Filter α
x: Set α
(x ∈ fg.sets) = (x ∈ fg)Filter.mem_sets: ∀ {α : Type u_1} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
Filter.mem_setsα: Type u_1
f, g, fg: Filter α
x: Set α
(x ∈ fg) = (x ∈ fg)]Goals accomplished! 🐙
  calcα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
    (f: Filter α
f = g: Filter α
g) ↔ (f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets = g: Filter α
g.sets: {α : Type u_1} → Filter α → Set (Set α)
sets)                           := byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ f.sets = g.setsfilter_eq_iff: ∀ {α : Type u_1} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iffα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f.sets = g.sets ↔ f.sets = g.sets]Goals accomplished! 🐙
          _: Prop_: Prop
_ ↔ ∀ (x: Set α
x : Set: Type u_1 → Type u_1
Set α: Type u_1
α), x: Set α
x ∈ f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets ↔ x: Set α
x ∈ g: Filter α
g.sets: {α : Type u_1} → Filter α → Set (Set α)
sets      := byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.setsSet.ext_iff: ∀ {α : Type u_1} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
Set.ext_iffα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets]Goals accomplished! 🐙
          _: Prop_: Prop
_ ↔ ∀ (x: Set α
x : Set: Type u_1 → Type u_1
Set α: Type u_1
α), x: Set α
x ∈ f: Filter α
f ↔ x: Set α
x ∈ g: Filter α
g                := byGoals accomplished! 🐙
            conv_lhs =>α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
              intro xα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f.sets ↔ x ∈ g.sets
              rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f.sets ↔ x ∈ g.setsmem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
mem_sets_eq_mem f: Filter α
fα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f ↔ x ∈ g.sets]α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f ↔ x ∈ g.sets
              rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f ↔ x ∈ g.setsmem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
mem_sets_eq_mem g: Filter α
gα: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f ↔ x ∈ g]α: Type u_1
f, g: Filter α
mem_sets_eq_mem:= fun fg x => Eq.mpr (id (congrArg (fun _a => _a = (x ∈ fg)) (propext Filter.mem_sets))) (Eq.refl (x ∈ fg)): ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
x: Set α
x ∈ f ↔ x ∈ g

-- 19
#explode Filter.ext_iff₁: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₁Filter.ext_iff₁ : ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g

0 │        │ α                       ├ Type u_1
1 │        │ f                       ├ Filter α
2 │        │ g                       ├ Filter α
3 │        │ Filter.ext_iff₁._simp_1 │ (f = g) = (f.sets = g.sets)
4 │        │ Filter.ext_iff₁._simp_2 │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
5 │        │ x                       │ ┌ Set α
6 │        │ Filter.ext_iff₁._simp_3 │ │ (x ∈ f.sets) = (x ∈ f)
7 │6       │ congrArg                │ │ Iff (x ∈ f.sets) = Iff (x ∈ f)
8 │        │ Filter.ext_iff₁._simp_3 │ │ (x ∈ g.sets) = (x ∈ g)
9 │7,8     │ congr                   │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
10│5,9     │ ∀I                      │ ∀ (x : Set α), (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
11│10      │ forall_congr            │ (∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
12│4,11    │ Eq.trans                │ (f.sets = g.sets) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
13│3,12    │ Eq.trans                │ (f = g) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
14│13      │ congrArg                │ Iff (f = g) = Iff (∀ (x : Set α), x ∈ f ↔ x ∈ g)
15│14      │ congrFun'               │ (f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
16│        │ iff_self                │ ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
17│15,16   │ Eq.trans                │ (f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
18│17      │ of_eq_true              │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
19│0,1,2,18│ ∀I                      │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g



-- 38
#explode Filter.ext_iff₂: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₂Filter.ext_iff₂ : ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g

0 │        │ α                    ├ Type u_1
1 │        │ f                    ├ Filter α
2 │        │ g                    ├ Filter α
3 │        │ f_eq_g               │ ┌ f = g
4 │        │ s                    │ ├ Set α
5 │        │ s_mem_f              │ │ ┌ s ∈ f
6 │3       │ Eq.symm              │ │ │ g = f
7 │6       │ congrArg             │ │ │ (s ∈ g) = (s ∈ f)
8 │7       │ id                   │ │ │ (s ∈ g) = (s ∈ f)
9 │8,5     │ Eq.mpr               │ │ │ s ∈ g
10│5,9     │ ∀I                   │ │ s ∈ f → s ∈ g
11│        │ s_mem_g              │ │ ┌ s ∈ g
12│3       │ congrArg             │ │ │ (s ∈ f) = (s ∈ g)
13│12      │ id                   │ │ │ (s ∈ f) = (s ∈ g)
14│13,11   │ Eq.mpr               │ │ │ s ∈ f
15│11,14   │ ∀I                   │ │ s ∈ g → s ∈ f
16│10,15   │ Iff.intro            │ │ s ∈ f ↔ s ∈ g
17│3,4,16  │ ∀I                   │ f = g → ∀ (s : Set α), s ∈ f ↔ s ∈ g
18│        │ set_mem_iff          │ ┌ ∀ (s : Set α), s ∈ f ↔ s ∈ g
19│        │ Filter.filter_eq_iff │ │ f = g ↔ f.sets = g.sets
20│19      │ propext              │ │ (f = g) = (f.sets = g.sets)
21│20      │ congrArg             │ │ (f = g) = (f.sets = g.sets)
22│21      │ id                   │ │ (f = g) = (f.sets = g.sets)
23│        │ Set.ext_iff          │ │ f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
24│23      │ propext              │ │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
25│24      │ congrArg             │ │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
26│25      │ id                   │ │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
27│        │ s                    │ │ ┌ Set α
28│18      │ ∀E                   │ │ │ s ∈ f ↔ s ∈ g
29│27,28   │ ∀I                   │ │ ∀ (s : Set α), s ∈ f ↔ s ∈ g
30│26,29   │ Eq.mpr               │ │ f.sets = g.sets
31│22,30   │ Eq.mpr               │ │ f = g
32│18,31   │ ∀I                   │ (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
33│17,32   │ Iff.intro            │ f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
34│0,1,2,33│ ∀I                   │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g



-- 31
#explode Filter.ext_iff₃: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₃Filter.ext_iff₃ : ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g

0 │        │ α                       ├ Type u_1
1 │        │ f                       ├ Filter α
2 │        │ g                       ├ Filter α
3 │        │ Filter.filter_eq_iff    │ f = g ↔ f.sets = g.sets
4 │3       │ propext                 │ (f = g) = (f.sets = g.sets)
5 │4       │ congrArg                │ (f = g ↔ f.sets = g.sets) = (f.sets = g.sets ↔ f.sets = g.sets)
6 │5       │ id                      │ (f = g ↔ f.sets = g.sets) = (f.sets = g.sets ↔ f.sets = g.sets)
7 │        │ Iff.rfl                 │ f.sets = g.sets ↔ f.sets = g.sets
8 │6,7     │ Eq.mpr                  │ f = g ↔ f.sets = g.sets
9 │        │ Set.ext_iff             │ f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
10│9       │ propext                 │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
11│10      │ congrArg                │ (f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets)
12│11      │ id                      │ (f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets)
13│        │ Iff.rfl                 │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
14│12,13   │ Eq.mpr                  │ f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
15│8,14    │ Trans.trans             │ f = g ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
16│        │ x                       │ ┌ Set α
17│        │ Filter.ext_iff₁._simp_3 │ │ (x ∈ f.sets) = (x ∈ f)
18│17      │ congrArg                │ │ Iff (x ∈ f.sets) = Iff (x ∈ f)
19│        │ Filter.ext_iff₁._simp_3 │ │ (x ∈ g.sets) = (x ∈ g)
20│18,19   │ congr                   │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
21│16,20   │ ∀I                      │ ∀ (x : Set α), (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
22│21      │ forall_congr            │ (∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
23│22      │ congrArg                │ Iff (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) = Iff (∀ (x : Set α), x ∈ f ↔ x ∈ g)
24│23      │ congrFun'               │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
25│        │ iff_self                │ ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
26│24,25   │ Eq.trans                │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
27│26      │ of_eq_true              │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
28│15,27   │ Trans.trans             │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
29│0,1,2,28│ ∀I                      │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g



-- 60
#explode Filter.ext_iff₄: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff₄Filter.ext_iff₄ : ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g

0 │           │ α                    ├ Type u_1
1 │           │ f                    ├ Filter α
2 │           │ g                    ├ Filter α
3 │           │ fg                   │ ┌ Filter α
4 │           │ x                    │ ├ Set α
5 │           │ Filter.mem_sets      │ │ x ∈ fg.sets ↔ x ∈ fg
6 │5          │ propext              │ │ (x ∈ fg.sets) = (x ∈ fg)
7 │6          │ congrArg             │ │ ((x ∈ fg.sets) = (x ∈ fg)) = ((x ∈ fg) = (x ∈ fg))
8 │7          │ id                   │ │ ((x ∈ fg.sets) = (x ∈ fg)) = ((x ∈ fg) = (x ∈ fg))
9 │           │ Eq.refl              │ │ (x ∈ fg) = (x ∈ fg)
10│8,9        │ Eq.mpr               │ │ (x ∈ fg.sets) = (x ∈ fg)
11│3,4,10     │ ∀I                   │ ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
13│           │ Filter.filter_eq_iff │ f = g ↔ f.sets = g.sets
14│13         │ propext              │ (f = g) = (f.sets = g.sets)
15│14         │ congrArg             │ (f = g ↔ f.sets = g.sets) = (f.sets = g.sets ↔ f.sets = g.sets)
16│15         │ id                   │ (f = g ↔ f.sets = g.sets) = (f.sets = g.sets ↔ f.sets = g.sets)
17│           │ Iff.rfl              │ f.sets = g.sets ↔ f.sets = g.sets
18│16,17      │ Eq.mpr               │ f = g ↔ f.sets = g.sets
19│           │ Set.ext_iff          │ f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
20│19         │ propext              │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
21│20         │ congrArg             │ (f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets)
22│21         │ id                   │ (f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets)
23│           │ Iff.rfl              │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
24│22,23      │ Eq.mpr               │ f.sets = g.sets ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
25│18,24      │ Trans.trans          │ f = g ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
26│           │ a✝                   │ ┌ Prop
27│           │ a                    │ ├ Prop
28│           │ e_a                  │ ├ a✝ = a
29│           │ b                    │ │ ┌ Prop
30│           │ Eq.refl              │ │ │ (a✝ ↔ b) = (a✝ ↔ b)
31│29,30      │ ∀I                   │ │ ∀ (b : Prop), (a✝ ↔ b) = (a✝ ↔ b)
32│31,28      │ Eq.rec               │ │ ∀ (b : Prop), (a✝ ↔ b) = (a ↔ b)
33│26,27,28,32│ ∀I                   │ ∀ (a a_1 : Prop), a = a_1 → ∀ (b : Prop), (a ↔ b) = (a_1 ↔ b)
34│           │ x                    │ ┌ Set α
35│11         │ ∀E                   │ │ (x ∈ f.sets) = (x ∈ f)
36│35         │ congrArg             │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g.sets)
37│11         │ ∀E                   │ │ (x ∈ g.sets) = (x ∈ g)
38│37         │ congrArg             │ │ (x ∈ f ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
39│           │ Eq.refl              │ │ (x ∈ f ↔ x ∈ g) = (x ∈ f ↔ x ∈ g)
40│38,39      │ Eq.trans             │ │ (x ∈ f ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
41│36,40      │ Eq.trans             │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
42│34,41      │ ∀I                   │ ∀ (x : Set α), (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
43│42         │ forall_congr         │ (∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
44│33,43      │ ∀E                   │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
45│44         │ id                   │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
46│           │ Iff.rfl              │ (∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
47│45,46      │ Eq.mpr               │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
48│25,47      │ Trans.trans          │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
49│0,1,2,48   │ ∀I                   │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g



theorem Set.mem_iff: ∀ {α : Type u_1} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff (p: α → Prop
p : α: Type u_1
α → Prop: Type
Prop) (y: α
y : α: Type u_1
α) : y: α
y ∈ {x: α
x : α: Type u_1
α | p: α → Prop
p x: α
x} ↔ p: α → Prop
p y: α
y := byGoals accomplished! 🐙
  exact Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rflGoals accomplished! 🐙

example: {α : Type u_1} → Filter α
example : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α := {
  sets := {s: Set α
s : Set: Type u_1 → Type u_1
Set α: Type u_1
α | Set.Finite: {α : Type u_1} → Set α → Prop
Set.Finite s: Set α
sᶜ}
  univ_sets := byGoals accomplished! 🐙
    rw [α: Type ?u.3
Set.univ ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff,α: Type ?u.3
Set.univᶜ.Finite Set.compl_univ: ∀ {α : Type ?u.3}, Set.univᶜ = ∅
Set.compl_univα: Type ?u.3
∅.Finite]α: Type ?u.3
∅.Finite
    exact Set.finite_empty: ∀ {α : Type ?u.3}, ∅.Finite
Set.finite_emptyGoals accomplished! 🐙
  sets_of_superset := byGoals accomplished! 🐙
    intro s: Set α
sα: Type ?u.3
s: Set α
∀ {y : Set α}, s ∈ {s | sᶜ.Finite} → s ⊆ y → y ∈ {s | sᶜ.Finite} t: Set α
tα: Type ?u.3
s, t: Set α
s ∈ {s | sᶜ.Finite} → s ⊆ t → t ∈ {s | sᶜ.Finite} «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
s ⊆ t → t ∈ {s | sᶜ.Finite} «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite} at «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite<-Set.compl_subset_compl: ∀ {α : Type ?u.3} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
Set.compl_subset_complα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite at «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite
    exact Set.Finite.subset: ∀ {α : Type ?u.3} {s : Set α}, s.Finite → ∀ {t : Set α}, t ⊆ s → t.Finite
Set.Finite.subset «sᶜ is finite»: sᶜ.Finite
«sᶜ is finite» «s ⊆ t»: tᶜ ⊆ sᶜ
«s ⊆ t»Goals accomplished! 🐙
  inter_sets := byGoals accomplished! 🐙
    intro s: Set α
sα: Type ?u.3
s: Set α
∀ {y : Set α}, s ∈ {s | sᶜ.Finite} → y ∈ {s | sᶜ.Finite} → s ∩ y ∈ {s | sᶜ.Finite} t: Set α
tα: Type ?u.3
s, t: Set α
s ∈ {s | sᶜ.Finite} → t ∈ {s | sᶜ.Finite} → s ∩ t ∈ {s | sᶜ.Finite} «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
t ∈ {s | sᶜ.Finite} → s ∩ t ∈ {s | sᶜ.Finite} «tᶜ is finite»: t ∈ {s | sᶜ.Finite}
«tᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite} at «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite} at «tᶜ is finite»: t ∈ {s | sᶜ.Finite}
«tᶜ is finite»α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.3} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite
    rw [α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.FiniteSet.compl_inter: ∀ {α : Type ?u.3} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_interα: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite]α: Type ?u.3
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite
    exact Set.Finite.union: ∀ {α : Type ?u.3} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
Set.Finite.union «sᶜ is finite»: sᶜ.Finite
«sᶜ is finite» «tᶜ is finite»: tᶜ.Finite
«tᶜ is finite»Goals accomplished! 🐙
}

example: {α : Type u_1} → Filter α
example : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α where
  sets := {s: Set α
s : Set: Type u_1 → Type u_1
Set α: Type u_1
α | Set.Finite: {α : Type u_1} → Set α → Prop
Set.Finite s: Set α
sᶜ}
  univ_sets := byGoals accomplished! 🐙
    simp only [Set.mem_iff: ∀ {α : Type ?u.17} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff, Set.compl_univ: ∀ {α : Type ?u.18}, Set.univᶜ = ∅
Set.compl_univ, Set.finite_empty: ∀ {α : Type ?u.16}, ∅.Finite
Set.finite_empty]Goals accomplished! 🐙
  sets_of_superset «sᶜ is finite»: x✝ ∈ {s | sᶜ.Finite}
«sᶜ is finite» «s ⊆ t»: x✝ ⊆ y✝
«s ⊆ t» :=
    «sᶜ is finite»: x✝ ∈ {s | sᶜ.Finite}
«sᶜ is finite».subset: ∀ {α : Type u_1} {s : Set α}, s.Finite → ∀ {t : Set α}, t ⊆ s → t.Finite
subset <| Set.compl_subset_compl: ∀ {α : Type u_1} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
Set.compl_subset_compl.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr «s ⊆ t»: x✝ ⊆ y✝
«s ⊆ t»
  -- equivelent to:
  -- sets_of_superset := by
  --   intros s t «sᶜ is finite» «s ⊆ t»
  --   have «tᶜ ⊆ sᶜ» := Set.compl_subset_compl.mpr «s ⊆ t»
  --   exact Set.Finite.subset «sᶜ is finite» «tᶜ ⊆ sᶜ»
  -- hint: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Filter.cofinite#doc
  inter_sets := byGoals accomplished! 🐙
    simp_all [α: Type ?u.3
∀ {x y : Set α}, x ∈ {s | sᶜ.Finite} → y ∈ {s | sᶜ.Finite} → x ∩ y ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.20} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffWarning: This simp argument is unused:
  Set.mem_iff

Hint: Omit it from the simp argument list.
  simp_all [Set.m̵e̵m̵_̵i̵f̵f̵,̵ ̵S̵e̵t̵.̵compl_inter, Set.Finite.union]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
α: Type ?u.3
∀ {x y : Set α}, x ∈ {s | sᶜ.Finite} → y ∈ {s | sᶜ.Finite} → x ∩ y ∈ {s | sᶜ.Finite}, Set.compl_inter: ∀ {α : Type ?u.24} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_inter,α: Type ?u.3
∀ {x y : Set α}, x ∈ {s | sᶜ.Finite} → y ∈ {s | sᶜ.Finite} → x ∩ y ∈ {s | sᶜ.Finite} Set.Finite.union: ∀ {α : Type ?u.25} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
Set.Finite.unionWarning: This simp argument is unused:
  Set.Finite.union

Hint: Omit it from the simp argument list.
  simp_all [Set.mem_iff, Set.compl_inter,̵ ̵S̵e̵t̵.̵F̵i̵n̵i̵t̵e̵.̵u̵n̵i̵o̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
α: Type ?u.3
∀ {x y : Set α}, x ∈ {s | sᶜ.Finite} → y ∈ {s | sᶜ.Finite} → x ∩ y ∈ {s | sᶜ.Finite}]Goals accomplished! 🐙