import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Finite
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.66} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iff, Set.ext_iff: ∀ {α : Type ?u.83} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
Set.ext_iff, Filter.mem_sets: ∀ {α : Type ?u.103} {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_gα: Type u_1
f, g: Filter α
f_eq_g: f = g
mp∀ (s : Set α), s ∈ f ↔ s ∈ g
    intro s: Set α
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.introα: 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} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
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
    (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)                           :=α: Type u_1
f, g: Filter α
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
f = g ↔ f.sets = g.setsfilter_eq_iff: ∀ {α : Type ?u.606} {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      :=α: Type u_1
f, g: Filter α
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g 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.621} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
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                :=α: Type u_1
f, g: Filter α
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙 simp_rw [α: Type u_1
f, g: Filter α
(∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ gFilter.mem_sets: ∀ {α : Type ?u.700} {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
    (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)                           :=α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ f.sets = g.setsfilter_eq_iff: ∀ {α : Type ?u.1056} {f g : Filter α}, f = g ↔ f.sets = g.sets
filter_eq_iffα: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (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      :=α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙 rw [α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (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.1071} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
Set.ext_iffα: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (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                :=α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g byGoals accomplished! 🐙
            conv_lhs =>α: Type u_1
f, g: Filter α
mem_sets_eq_mem: ∀ (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: ∀ (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: ∀ (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: ∀ (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: ∀ (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: ∀ (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: ∀ (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: ∀ (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 │        │ _auxLemma.1  │ (f = g) = (f.sets = g.sets)
4 │        │ _auxLemma.2  │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
5 │        │ x            │ ┌ Set α
6 │        │ _auxLemma.3  │ │ (x ∈ f.sets) = (x ∈ f)
7 │6       │ congrArg     │ │ Iff (x ∈ f.sets) = Iff (x ∈ f)
8 │        │ _auxLemma.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     │ (f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (a : Set α), a ∈ f ↔ a ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
15│        │ iff_self     │ ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
16│14,15   │ Eq.trans     │ (f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
17│16      │ of_eq_true   │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
18│0,1,2,17│ ∀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│        │ _auxLemma.3          │ │ (x ∈ f.sets) = (x ∈ f)
18│17      │ congrArg             │ │ Iff (x ∈ f.sets) = Iff (x ∈ f)
19│        │ _auxLemma.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             │ ((∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) =
  ((∀ (a : Set α), a ∈ f ↔ a ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
24│        │ iff_self             │ ((∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
25│23,24   │ Eq.trans             │ ((∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g) = True
26│25      │ of_eq_true           │ (∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
27│15,26   │ Trans.trans          │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
28│0,1,2,27│ ∀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)
12│           │ mem_sets_eq_mem      │ ┌ ∀ (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│           │ b                    │ │ │ ├ Prop
31│           │ e_b                  │ │ │ ├ b✝ = b
32│           │ Eq.refl              │ │ │ │ (a✝ ↔ b✝) = (a✝ ↔ b✝)
33│32,31      │ Eq.rec               │ │ │ │ (a✝ ↔ b✝) = (a✝ ↔ b)
34│29,30,31,33│ ∀I                   │ │ │ ∀ (b b_1 : Prop), b = b_1 → (a✝ ↔ b) = (a✝ ↔ b_1)
35│34,28      │ Eq.rec               │ │ │ ∀ (b b_1 : Prop), b = b_1 → (a✝ ↔ b) = (a ↔ b_1)
36│26,27,28,35│ ∀I                   │ │ ∀ (a a_1 : Prop), a = a_1 → ∀ (b b_1 : Prop), b = b_1 → (a ↔ b) = (a_1 ↔ b_1)
37│           │ x                    │ │ ┌ Set α
38│12         │ ∀E                   │ │ │ (x ∈ f.sets) = (x ∈ f)
39│38         │ congrArg             │ │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g.sets)
40│12         │ ∀E                   │ │ │ (x ∈ g.sets) = (x ∈ g)
41│40         │ congrArg             │ │ │ (x ∈ f ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
42│           │ Eq.refl              │ │ │ (x ∈ f ↔ x ∈ g) = (x ∈ f ↔ x ∈ g)
43│41,42      │ Eq.trans             │ │ │ (x ∈ f ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
44│39,43      │ Eq.trans             │ │ │ (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
45│37,44      │ ∀I                   │ │ ∀ (x : Set α), (x ∈ f.sets ↔ x ∈ g.sets) = (x ∈ f ↔ x ∈ g)
46│45         │ forall_congr         │ │ (∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets) = ∀ (a : Set α), a ∈ f ↔ a ∈ g
47│           │ Eq.refl              │ │ (∀ (x : Set α), x ∈ f ↔ x ∈ g) = ∀ (x : Set α), x ∈ f ↔ x ∈ g
48│36,46,47   │ ∀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)
49│48         │ 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)
50│           │ Iff.rfl              │ │ (∀ (x : Set α), x ∈ f ↔ x ∈ g) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
51│49,50      │ Eq.mpr               │ │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
52│25,51      │ Trans.trans          │ │ f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g
53│12,52      │ ∀I                   │ (∀ (fg : Filter α) (x : Set α), (x ∈ fg.sets) = (x ∈ fg)) →
  (f = g ↔ ∀ (x : Set α), x ∈ f ↔ x ∈ g)
54│11,53      │ letFun               │ f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
55│0,1,2,54   │ ∀I                   │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ 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.1247
Set.univ ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.1301} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff,α: Type ?u.1247
Set.univᶜ.Finite Set.compl_univ: ∀ {α : Type ?u.1323}, Set.univᶜ = ∅
Set.compl_univα: Type ?u.1247
∅.Finite]α: Type ?u.1247
∅.Finite
    exact Set.finite_empty: ∀ {α : Type ?u.1247}, ∅.Finite
Set.finite_emptyGoals accomplished! 🐙
  sets_of_superset := byGoals accomplished! 🐙
    intro s: Set α
s t: Set α
t «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite» «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.1247} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}]α: Type ?u.1247
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.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.1247} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite]α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite
    rw [α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite<-Set.compl_subset_compl: ∀ {α : Type ?u.1247} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
Set.compl_subset_complα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite]α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite at «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite
    exact Set.Finite.subset: ∀ {α : Type ?u.1247} {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 t: Set α
t «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite» «tᶜ is finite»: t ∈ {s | sᶜ.Finite}
«tᶜ is finite»α: Type ?u.1247
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.1247
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.1247} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.1247
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.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.1247
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.1482} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.1247
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.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.1247} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite]α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite
    rw [α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.FiniteSet.compl_inter: ∀ {α : Type ?u.1247} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_interα: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite]α: Type ?u.1247
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite
    exact Set.Finite.union: ∀ {α : Type ?u.1247} {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.1677} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff, Set.compl_univ: ∀ {α : Type ?u.1699}, Set.univᶜ = ∅
Set.compl_univ, Set.finite_empty: ∀ {α : Type ?u.1708}, ∅.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 [Set.mem_iff: ∀ {α : Type ?u.1801} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff, Set.compl_inter: ∀ {α : Type ?u.1825} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_inter, Set.Finite.union: ∀ {α : Type ?u.1840} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
Set.Finite.union]Goals accomplished! 🐙