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

set_option linter.unusedVariables false
set_option autoImplicit false

Note: This file is adapted from bridgekat/filter-game

namespace FilterGame
variable {α: Type ?u.2
α : Type _: Type (u_1 + 1)
Type _}

Filters

Given a type α, a filter is a collection of subsets of α which

contains the whole set (the universal set is a member of sets)
upward closed (supersets are members of sets)
closed under intersections (intersections are members of sets)

structure Filter: Type u_1 → Type u_1
Filter (α: Type u_1
α : Type _: Type (u_1 + 1)
Type _) where
  sets: {α : Type u_1} → Filter α → Set (Set α)
sets                    : Set: Type u_1 → Type u_1
Set (Set: Type u_1 → Type u_1
Set α: Type u_1
α)
  univ_mem_sets: ∀ {α : Type u_1} (self : Filter α), Set.univ ∈ self.sets
univ_mem_sets           : Set.univ: {α : Type u_1} → Set α
Set.univ ∈ sets: Set (Set α)
sets
  superset_mem_sets: ∀ {α : Type u_1} (self : Filter α) {s t : Set α}, s ∈ self.sets → s ⊆ t → t ∈ self.sets
superset_mem_sets {s: Set α
s t: Set α
t} : s: Set α
s ∈ sets: Set (Set α)
sets → s: Set α
s ⊆ t: Set α
t → t: Set α
t ∈ sets: Set (Set α)
sets
  inter_mem_sets: ∀ {α : Type u_1} (self : Filter α) {s t : Set α}, s ∈ self.sets → t ∈ self.sets → s ∩ t ∈ self.sets
inter_mem_sets {s: Set α
s t: Set α
t}    : s: Set α
s ∈ sets: Set (Set α)
sets → t: Set α
t ∈ sets: Set (Set α)
sets → s: Set α
s ∩ t: Set α
t ∈ sets: Set (Set α)
sets

Notation `s ∈ f`

If we have a filter f, it is more convenient to write s ∈ f for s ∈ f.sets.

To define the notation, we simply provide an instance for the typeclass Membership which has defined notation ∈ on it.

Providing an instance, is providing all fields of the class, some are data-like, some are function-like, and some are property-like.

We need to provide the data or function implementation for the first two kinds, prove the property for the last kind.

Here we only need to provide a function.

instance: {α : Type u_1} → Membership (Set α) (Filter α)
instance : Membership: outParam (Type u_1) → Type u_1 → Type u_1
Membership (Set: Type u_1 → Type u_1
Set α: Type u_1
α) (Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) := {
  mem := fun f: Filter α
f s: Set α
s ↦ s: Set α
s ∈ f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets
}

To simplify, we can surround the ordered fields with ⟨ and ⟩, seperated by ,.

instance: {α : Type u_1} → Membership (Set α) (Filter α)
instance : Membership: outParam (Type u_1) → Type u_1 → Type u_1
Membership (Set: Type u_1 → Type u_1
Set α: Type u_1
α) (Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) :=
  ⟨fun f: Filter α
f s: Set α
s ↦ s: Set α
s ∈ f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets⟩

Now that ∈ is defined.

We prove an obviously true statement.

example: ∀ {α : Type u_1} (f : Filter α) (s : Set α), s ∈ f ↔ s ∈ f
example (f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) (s: Set α
s : Set: Type u_1 → Type u_1
Set α: Type u_1
α) : s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ f: Filter α
f := byGoals accomplished! 🐙
  exact Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rflGoals accomplished! 🐙

We then prove its propositional equality, and make it available for simp.

@[simp]
theorem Filter.mem_def: ∀ {α : Type u_1} (f : Filter α) (s : Set α), s ∈ f ↔ s ∈ f.sets
Filter.mem_def (f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) (s: Set α
s : Set: Type u_1 → Type u_1
Set α: Type u_1
α) : s: Set α
s ∈ f: Filter α
f ↔ s: Set α
s ∈ f: Filter α
f.sets: {α : Type u_1} → Filter α → Set (Set α)
sets := byGoals accomplished! 🐙
  exact Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rflGoals accomplished! 🐙

The equality between filters

If f.sets and g.sets are equal, we consider f and g to be equal, too.

@[simp]
theorem Filter.eq_def: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ f.sets = g.sets
Filter.eq_def (f: Filter α
f g: Filter α
g : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : 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! 🐙
  apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introα: Type u_1
f, g: Filter α
mpf = g → f.sets = g.sets
α: Type u_1
f, g: Filter α
mprf.sets = g.sets → f = g
  .α: Type u_1
f, g: Filter α
mpf = g → f.sets = g.sets intro h: f = g
hα: Type u_1
f, g: Filter α
h: f = g
mpf.sets = g.sets
    rw [α: Type u_1
f, g: Filter α
h: f = g
mpf.sets = g.setsh: f = g
hα: Type u_1
f, g: Filter α
h: f = g
mpg.sets = g.sets]Goals accomplished! 🐙
  .α: Type u_1
f, g: Filter α
mprf.sets = g.sets → f = g intro h: f.sets = g.sets
hα: Type u_1
f, g: Filter α
h: f.sets = g.sets
mprf = g
    induction f: Filter α
fα: Type u_1
g: Filter α
sets✝: Set (Set α)
univ_mem_sets✝: Set.univ ∈ sets✝
superset_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h: { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }.sets =
  g.sets
mpr.mk{ sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
    inter_mem_sets := inter_mem_sets✝ } =
  g
    induction g: Filter α
gα: Type u_1
sets✝¹: Set (Set α)
univ_mem_sets✝¹: Set.univ ∈ sets✝¹
superset_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝: Set (Set α)
univ_mem_sets✝: Set.univ ∈ sets✝
superset_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h: { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mk{ sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
    inter_mem_sets := inter_mem_sets✝ }
    rw [α: Type u_1
sets✝¹: Set (Set α)
univ_mem_sets✝¹: Set.univ ∈ sets✝¹
superset_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝: Set (Set α)
univ_mem_sets✝: Set.univ ∈ sets✝
superset_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h: { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mk{ sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
    inter_mem_sets := inter_mem_sets✝ }mk.injEq: ∀ {α : Type ?u.1208} (sets : Set (Set α)) (univ_mem_sets : Set.univ ∈ sets)
  (superset_mem_sets : ∀ {s t : Set α}, s ∈ sets → s ⊆ t → t ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → s ∩ t ∈ sets) (sets_1 : Set (Set α))
  (univ_mem_sets_1 : Set.univ ∈ sets_1) (superset_mem_sets_1 : ∀ {s t : Set α}, s ∈ sets_1 → s ⊆ t → t ∈ sets_1)
  (inter_mem_sets_1 : ∀ {s t : Set α}, s ∈ sets_1 → t ∈ sets_1 → s ∩ t ∈ sets_1),
  ({ sets := sets, univ_mem_sets := univ_mem_sets, superset_mem_sets := superset_mem_sets,
        inter_mem_sets := inter_mem_sets } =
      { sets := sets_1, univ_mem_sets := univ_mem_sets_1, superset_mem_sets := superset_mem_sets_1,
        inter_mem_sets := inter_mem_sets_1 }) =
    (sets = sets_1)
mk.injEqα: Type u_1
sets✝¹: Set (Set α)
univ_mem_sets✝¹: Set.univ ∈ sets✝¹
superset_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝: Set (Set α)
univ_mem_sets✝: Set.univ ∈ sets✝
superset_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h: { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mksets✝¹ = sets✝]α: Type u_1
sets✝¹: Set (Set α)
univ_mem_sets✝¹: Set.univ ∈ sets✝¹
superset_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝: Set (Set α)
univ_mem_sets✝: Set.univ ∈ sets✝
superset_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h: { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mksets✝¹ = sets✝
    assumptionGoals accomplished! 🐙
    
theorem Filter.ext_iff₁: ∀ (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 [eq_def: ∀ {α : Type ?u.1375} (f g : Filter α), f = g ↔ f.sets = g.sets
eq_def, Set.ext_iff: ∀ {α : Type ?u.1392} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
Set.ext_iff, mem_def: ∀ {α : Type ?u.1410} (f : Filter α) (s : Set α), s ∈ f ↔ s ∈ f.sets
mem_def]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 = geq_def: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ f.sets = g.sets
eq_defα: 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₃: ∀ (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.setseq_def: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ f.sets = g.sets
eq_defα: 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.1923} {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                :=α: 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 ∈ gmem_def: ∀ {α : Type ?u.2004} (f : Filter α) (s : Set α), s ∈ f ↔ s ∈ f.sets
mem_defGoals accomplished! 🐙]Goals accomplished! 🐙

theorem Filter.ext_iff₄: ∀ (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)mem_def: ∀ {α : Type ?u.2172} (f : Filter α) (s : Set α), s ∈ f ↔ s ∈ f.sets
mem_defα: Type u_1
f, g, fg: Filter α
x: Set α
(x ∈ fg.sets) = (x ∈ fg.sets)]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.setseq_def: ∀ {α : Type u_1} (f g : Filter α), f = g ↔ f.sets = g.sets
eq_defα: 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.2378} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
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.2  │ (f = g) = (f.sets = g.sets)
4 │        │ _auxLemma.3  │ (f.sets = g.sets) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
5 │3,4     │ Eq.trans     │ (f = g) = ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets
6 │5       │ congrArg     │ Iff (f = g) = Iff (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets)
7 │        │ s            │ ┌ Set α
8 │        │ _auxLemma.1  │ │ (s ∈ f) = (s ∈ f.sets)
9 │8       │ congrArg     │ │ Iff (s ∈ f) = Iff (s ∈ f.sets)
10│        │ _auxLemma.1  │ │ (s ∈ g) = (s ∈ g.sets)
11│9,10    │ congr        │ │ (s ∈ f ↔ s ∈ g) = (s ∈ f.sets ↔ s ∈ g.sets)
12│7,11    │ ∀I           │ ∀ (s : Set α), (s ∈ f ↔ s ∈ g) = (s ∈ f.sets ↔ s ∈ g.sets)
13│12      │ forall_congr │ (∀ (a : Set α), a ∈ f ↔ a ∈ g) = ∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets
14│6,13    │ congr        │ (f = g ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ g) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets)
15│        │ iff_self     │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) = True
16│14,15   │ Eq.trans     │ (f = g ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ g) = True
17│16      │ of_eq_true   │ f = g ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ g
18│0,1,2,17│ ∀I           │ ∀ {α : Type u_1} (f g : Filter α), f = g ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ 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.eq_def │ │ 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.eq_def │ 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.1              │ │ (x ∈ f) = (x ∈ f.sets)
18│17      │ congrArg                 │ │ Iff (x ∈ f) = Iff (x ∈ f.sets)
19│        │ _auxLemma.1              │ │ (x ∈ g) = (x ∈ g.sets)
20│18,19   │ congr                    │ │ (x ∈ f ↔ x ∈ g) = (x ∈ f.sets ↔ x ∈ g.sets)
21│16,20   │ ∀I                       │ ∀ (x : Set α), (x ∈ f ↔ x ∈ g) = (x ∈ f.sets ↔ x ∈ g.sets)
22│21      │ forall_congr             │ (∀ (a : Set α), a ∈ f ↔ a ∈ g) = ∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets
23│22      │ congrArg                 │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ g) =
  ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (a : Set α), a ∈ f.sets ↔ a ∈ g.sets)
24│        │ iff_self                 │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔
    ∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) =
  True
25│23,24   │ Eq.trans                 │ ((∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ g) = True
26│25      │ of_eq_true               │ (∀ (x : Set α), x ∈ f.sets ↔ x ∈ g.sets) ↔ ∀ (a : Set α), a ∈ f ↔ a ∈ 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_def │ │ x ∈ fg ↔ x ∈ fg.sets
6 │5          │ propext                   │ │ (x ∈ fg) = (x ∈ fg.sets)
7 │6          │ congrArg                  │ │ ((x ∈ fg.sets) = (x ∈ fg)) = ((x ∈ fg.sets) = (x ∈ fg.sets))
8 │7          │ id                        │ │ ((x ∈ fg.sets) = (x ∈ fg)) = ((x ∈ fg.sets) = (x ∈ fg.sets))
9 │           │ Eq.refl                   │ │ (x ∈ fg.sets) = (x ∈ fg.sets)
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.eq_def  │ │ 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



def f: α → α
fWarning: declaration uses 'sorry' : α: Type u_1
α → α: Type u_1
α :=
  fun f: α
f =>
    let s: ℕ
s := 1: ℕ
1
    sorry: α
sorry

Trivial lemmas

These lemmas directly follow from the definiton of the filters:

theorem Filter.univ_mem: ∀ {α : Type u_1} (f : Filter α), Set.univ ∈ f
Filter.univ_mem (f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α) : Set.univ: {α : Type u_1} → Set α
Set.univ ∈ f: Filter α
f := byGoals accomplished! 🐙
  exact f: Filter α
f.univ_mem_sets: ∀ {α : Type u_1} (self : Filter α), Set.univ ∈ self.sets
univ_mem_setsGoals accomplished! 🐙

theorem Filter.superset_mem: ∀ {α : Type u_1} {f : Filter α} {s t : Set α}, s ∈ f → s ⊆ t → t ∈ f
Filter.superset_mem {f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α} {s: Set α
s t: Set α
t : Set: Type u_1 → Type u_1
Set α: Type u_1
α} (hs: s ∈ f
hs : s: Set α
s ∈ f: Filter α
f) (h: s ⊆ t
h : s: Set α
s ⊆ t: Set α
t) : t: Set α
t ∈ f: Filter α
f := byGoals accomplished! 🐙
  exact f: Filter α
f.superset_mem_sets: ∀ {α : Type u_1} (self : Filter α) {s t : Set α}, s ∈ self.sets → s ⊆ t → t ∈ self.sets
superset_mem_sets hs: s ∈ f
hs h: s ⊆ t
hGoals accomplished! 🐙

theorem Filter.inter_mem: ∀ {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
Filter.inter_mem {f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α} {s: Set α
s t: Set α
t : Set: Type u_1 → Type u_1
Set α: Type u_1
α} (hs: s ∈ f
hs : s: Set α
s ∈ f: Filter α
f) (ht: t ∈ f
ht : t: Set α
t ∈ f: Filter α
f) : s: Set α
s ∩ t: Set α
t ∈ f: Filter α
f := byGoals accomplished! 🐙
  exact f: Filter α
f.inter_mem_sets: ∀ {α : Type u_1} (self : Filter α) {s t : Set α}, s ∈ self.sets → t ∈ self.sets → s ∩ t ∈ self.sets
inter_mem_sets hs: s ∈ f
hs ht: t ∈ f
htGoals accomplished! 🐙

theorem Filter.inter_mem₁: ∀ {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
Filter.inter_mem₁ {f: Filter α
f : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α} {s: Set α
s t: Set α
t : Set: Type u_1 → Type u_1
Set α: Type u_1
α} (hs: s ∈ f
hs : s: Set α
s ∈ f: Filter α
f) (ht: t ∈ f
ht : t: Set α
t ∈ f: Filter α
f) : s: Set α
s ∩ t: Set α
t ∈ f: Filter α
f := f: Filter α
f.inter_mem_sets: ∀ {α : Type u_1} (self : Filter α) {s t : Set α}, s ∈ self.sets → t ∈ self.sets → s ∩ t ∈ self.sets
inter_mem_sets hs: s ∈ f
hs ht: t ∈ f
ht

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! 🐙

/-！

## Examples of filters

-/

example : Filter α := {
  sets := Set.univ
  univ_mem_sets := byGoals accomplished! 🐙
    exact Set.mem_univ: ∀ {α : Type ?u.3162} (x : α), x ∈ Set.univ
Set.mem_univ Set.univ: {α : Type ?u.3162} → Set α
Set.univGoals accomplished! 🐙
  superset_mem_sets := byGoals accomplished! 🐙
    intros s: Set α
s t: Set α
tα: Type ?u.3162
s, t: Set α
s ∈ Set.univ → s ⊆ t → t ∈ Set.univ
    intros «s ∈ univ»: s ∈ Set.univ
«s ∈ univ» «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.3162
s, t: Set α
«s ∈ univ»: s ∈ Set.univ
«s ⊆ t»: s ⊆ t
t ∈ Set.univ
    exact Set.mem_univ: ∀ {α : Type ?u.3162} (x : α), x ∈ Set.univ
Set.mem_univ t: Set α
tGoals accomplished! 🐙
  inter_mem_sets := byGoals accomplished! 🐙
    intros s: Set α
s t: Set α
tα: Type ?u.3162
s, t: Set α
s ∈ Set.univ → t ∈ Set.univ → s ∩ t ∈ Set.univ
    intros «s ∈ univ»: s ∈ Set.univ
«s ∈ univ» «t ∈ univ»: t ∈ Set.univ
«t ∈ univ»α: Type ?u.3162
s, t: Set α
«s ∈ univ»: s ∈ Set.univ
«t ∈ univ»: t ∈ Set.univ
s ∩ t ∈ Set.univ
    exact Set.mem_univ: ∀ {α : Type ?u.3162} (x : α), x ∈ Set.univ
Set.mem_univ (s: Set α
s ∩ t: Set α
t)Goals accomplished! 🐙
}

/-！

or, succinctly:

-/

example: {α : Type u_1} → Filter α
example : Filter: Type u_1 → Type u_1
Filter α: Type u_1
α := {
  sets := Set.univ: {α : Type u_1} → Set α
Set.univ
  univ_mem_sets := byGoals accomplished! 🐙
    apply Set.mem_univ: ∀ {α : Type ?u.3230} (x : α), x ∈ Set.univ
Set.mem_univGoals accomplished! 🐙
  superset_mem_sets := byGoals accomplished! 🐙
    introsα: Type ?u.3230
s✝, t✝: Set α
a✝¹: s✝ ∈ Set.univ
a✝: s✝ ⊆ t✝
t✝ ∈ Set.univ
    apply Set.mem_univ: ∀ {α : Type ?u.3230} (x : α), x ∈ Set.univ
Set.mem_univGoals accomplished! 🐙
  inter_mem_sets := byGoals accomplished! 🐙
    introsα: Type ?u.3230
s✝, t✝: Set α
a✝¹: s✝ ∈ Set.univ
a✝: t✝ ∈ Set.univ
s✝ ∩ t✝ ∈ Set.univ
    apply Set.mem_univ: ∀ {α : Type ?u.3230} (x : α), x ∈ Set.univ
Set.mem_univGoals accomplished! 🐙
}

Hint: rw using Set.mem_iff to unfold the set-builder notation. Mathlib lemmas Set.univ_subset_iff and Set.inter_self can be useful here.

Use simp? rw? exact? apply? aesop? to get hints.

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
α | s: Set α
s = Set.univ: {α : Type u_1} → Set α
Set.univ}
  univ_mem_sets := byGoals accomplished! 🐙
    rw [α: Type ?u.3290
Set.univ ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.3290} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3290
Set.univ = Set.univ]Goals accomplished! 🐙
  superset_mem_sets := byGoals accomplished! 🐙
    simp_rw [α: Type ?u.3290
∀ {s t : Set α}, s ∈ {s | s = Set.univ} → s ⊆ t → t ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.3460} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3290
∀ {s t : Set α}, s = Set.univ → s ⊆ t → t = Set.univ]α: Type ?u.3290
∀ {s t : Set α}, s = Set.univ → s ⊆ t → t = Set.univ
    intros s: Set α
s t: Set α
t «s = univ»: s = Set.univ
«s = univ» «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«s ⊆ t»: s ⊆ t
t = Set.univ
    apply Set.univ_subset_iff: ∀ {α : Type ?u.3290} {s : Set α}, Set.univ ⊆ s ↔ s = Set.univ
Set.univ_subset_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mpα: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«s ⊆ t»: s ⊆ t
Set.univ ⊆ t
    rw [α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«s ⊆ t»: s ⊆ t
Set.univ ⊆ t<-«s = univ»: s = Set.univ
«s = univ»α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«s ⊆ t»: s ⊆ t
s ⊆ t]α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«s ⊆ t»: s ⊆ t
s ⊆ t
    exact «s ⊆ t»: s ⊆ t
«s ⊆ t»Goals accomplished! 🐙
  inter_mem_sets := byGoals accomplished! 🐙
    simp_rw [α: Type ?u.3290
∀ {s t : Set α}, s ∈ {s | s = Set.univ} → t ∈ {s | s = Set.univ} → s ∩ t ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.3779} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.3290
∀ {s t : Set α}, s = Set.univ → t = Set.univ → s ∩ t = Set.univ]α: Type ?u.3290
∀ {s t : Set α}, s = Set.univ → t = Set.univ → s ∩ t = Set.univ
    intros s: Set α
s t: Set α
t «s = univ»: s = Set.univ
«s = univ» «t = univ»: t = Set.univ
«t = univ»α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«t = univ»: t = Set.univ
s ∩ t = Set.univ
    rw [α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«t = univ»: t = Set.univ
s ∩ t = Set.univ«s = univ»: s = Set.univ
«s = univ»,α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«t = univ»: t = Set.univ
Set.univ ∩ t = Set.univ «t = univ»: t = Set.univ
«t = univ»α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«t = univ»: t = Set.univ
Set.univ ∩ Set.univ = Set.univ]α: Type ?u.3290
s, t: Set α
«s = univ»: s = Set.univ
«t = univ»: t = Set.univ
Set.univ ∩ Set.univ = Set.univ
    exact Set.inter_self: ∀ {α : Type ?u.3290} (a : Set α), a ∩ a = a
Set.inter_self Set.univ: {α : Type ?u.3290} → Set α
Set.univGoals accomplished! 🐙
}

/-！

or, succinctly:

-/

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
α | s: Set α
s = Set.univ: {α : Type u_1} → Set α
Set.univ}
  univ_mem_sets := byGoals accomplished! 🐙
    rw [α: Type ?u.4032
Set.univ ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.4032} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4032
Set.univ = Set.univ]Goals accomplished! 🐙
  superset_mem_sets := byGoals accomplished! 🐙
    simp_rw [α: Type ?u.4032
∀ {s t : Set α}, s ∈ {s | s = Set.univ} → s ⊆ t → t ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.4202} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4032
∀ {s t : Set α}, s = Set.univ → s ⊆ t → t = Set.univ]α: Type ?u.4032
∀ {s t : Set α}, s = Set.univ → s ⊆ t → t = Set.univ
    introsα: Type ?u.4032
s✝, t✝: Set α
a✝¹: s✝ = Set.univ
a✝: s✝ ⊆ t✝
t✝ = Set.univ
    simp_all only [Set.univ_subset_iff: ∀ {α : Type ?u.4415} {s : Set α}, Set.univ ⊆ s ↔ s = Set.univ
Set.univ_subset_iff]Goals accomplished! 🐙
  inter_mem_sets := byGoals accomplished! 🐙
    simp_rw [α: Type ?u.4032
∀ {s t : Set α}, s ∈ {s | s = Set.univ} → t ∈ {s | s = Set.univ} → s ∩ t ∈ {s | s = Set.univ}Set.mem_iff: ∀ {α : Type ?u.4590} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4032
∀ {s t : Set α}, s = Set.univ → t = Set.univ → s ∩ t = Set.univ]α: Type ?u.4032
∀ {s t : Set α}, s = Set.univ → t = Set.univ → s ∩ t = Set.univ
    introsα: Type ?u.4032
s✝, t✝: Set α
a✝¹: s✝ = Set.univ
a✝: t✝ = Set.univ
s✝ ∩ t✝ = Set.univ
    simp_all only [Set.inter_self: ∀ {α : Type ?u.4814} (a : Set α), a ∩ a = a
Set.inter_self]Goals accomplished! 🐙
}


/-！

The cofinite filter consists of subsets whose complements are finite.

-/
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_mem_sets := byGoals accomplished! 🐙
    rw [α: Type ?u.4865
Set.univ ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.4926} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff,α: Type ?u.4865
Set.univᶜ.Finite Set.compl_univ: ∀ {α : Type ?u.4865}, Set.univᶜ = ∅
Set.compl_univα: Type ?u.4865
∅.Finite]α: Type ?u.4865
∅.Finite
    exact Set.finite_empty: ∀ {α : Type ?u.4865}, ∅.Finite
Set.finite_emptyGoals accomplished! 🐙
  superset_mem_sets := byGoals accomplished! 🐙
    intros s: Set α
s t: Set α
tα: Type ?u.4865
s, t: Set α
s ∈ {s | sᶜ.Finite} → s ⊆ t → t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.4865
s, t: Set α
s ∈ {s | sᶜ.Finite} → s ⊆ t → t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.4865} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4865
s, t: Set α
sᶜ.Finite → s ⊆ t → t ∈ {s | sᶜ.Finite}]α: Type ?u.4865
s, t: Set α
sᶜ.Finite → s ⊆ t → t ∈ {s | sᶜ.Finite}
    intro «sᶜ is finite»: sᶜ.Finite
«sᶜ is finite» «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.4865} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite]α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite
    rw [α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: s ⊆ t
tᶜ.Finite<-Set.compl_subset_compl: ∀ {α : Type ?u.4865} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
Set.compl_subset_complα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite]α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite at «s ⊆ t»: s ⊆ t
«s ⊆ t»α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«s ⊆ t»: tᶜ ⊆ sᶜ
tᶜ.Finite
    exact Set.Finite.subset: ∀ {α : Type ?u.4865} {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_mem_sets := byGoals accomplished! 🐙
    intros s: Set α
s t: Set α
tα: Type ?u.4865
s, t: Set α
s ∈ {s | sᶜ.Finite} → t ∈ {s | sᶜ.Finite} → s ∩ t ∈ {s | sᶜ.Finite}
    intro «sᶜ is finite»: s ∈ {s | sᶜ.Finite}
«sᶜ is finite» «tᶜ is finite»: t ∈ {s | sᶜ.Finite}
«tᶜ is finite»α: Type ?u.4865
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.4865
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.5078} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.4865
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.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: t ∈ {s | sᶜ.Finite}
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.4865
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.4865} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}]α: Type ?u.4865
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.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}
    rw [α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
s ∩ t ∈ {s | sᶜ.Finite}Set.mem_iff: ∀ {α : Type ?u.4865} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iffα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite]α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.Finite
    rw [α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(s ∩ t)ᶜ.FiniteSet.compl_inter: ∀ {α : Type ?u.5153} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_interα: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite]α: Type ?u.4865
s, t: Set α
«sᶜ is finite»: sᶜ.Finite
«tᶜ is finite»: tᶜ.Finite
(sᶜ ∪ tᶜ).Finite
    exact Set.Finite.union: ∀ {α : Type ?u.4865} {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! 🐙
}

/-！

or, succinctly:

-/

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_mem_sets := byGoals accomplished! 🐙
    simp only [Set.mem_iff: ∀ {α : Type ?u.5307} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff, Set.compl_univ: ∀ {α : Type ?u.5329}, Set.univᶜ = ∅
Set.compl_univ, Set.finite_empty: ∀ {α : Type ?u.5338}, ∅.Finite
Set.finite_empty]Goals accomplished! 🐙
  superset_mem_sets «sᶜ is finite»: s✝ ∈ {s | sᶜ.Finite}
«sᶜ is finite» «s ⊆ t»: s✝ ⊆ t✝
«s ⊆ t» :=
    «sᶜ is finite»: s✝ ∈ {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»: s✝ ⊆ t✝
«s ⊆ t»
  inter_mem_sets := byGoals accomplished! 🐙
    simp_all [Set.mem_iff: ∀ {α : Type ?u.5431} (p : α → Prop) (y : α), y ∈ {x | p x} ↔ p y
Set.mem_iff, Set.compl_inter: ∀ {α : Type ?u.5455} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
Set.compl_inter, Set.Finite.union: ∀ {α : Type ?u.5470} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
Set.Finite.union]Goals accomplished! 🐙

Filter bases

Given a type α, a filter basis is a collection of subsets of α which:

contains at least one subset (the sets collection is nonempty),
intersections of two member subsets include some member subset of the collection (intersections include members of sets).

We represent it in Lean as a new type, which "packages" the collection of subsets, along with all the properties it should have.

structure Basis: Type u_1 → Type u_1
Basis (α: Type u_1
α : Type _: Type (u_1 + 1)
Type _) where
  sets: {α : Type u_1} → Basis α → Set (Set α)
sets                 : Set: Type u_1 → Type u_1
Set (Set: Type u_1 → Type u_1
Set α: Type u_1
α)
  sets_nonempty: ∀ {α : Type u_1} (self : Basis α), ∃ s, s ∈ self.sets
sets_nonempty        : ∃ s: Set α
s, s: Set α
s ∈ sets: Set (Set α)
sets
  inter_mem_sets: ∀ {α : Type u_1} (self : Basis α) {s t : Set α}, s ∈ self.sets → t ∈ self.sets → ∃ u ∈ self.sets, u ⊆ s ∩ t
inter_mem_sets {s: Set α
s t: Set α
t} : s: Set α
s ∈ sets: Set (Set α)
sets → t: Set α
t ∈ sets: Set (Set α)
sets → ∃ u: Set α
u ∈ sets: Set (Set α)
sets, u: Set α
u ⊆ s: Set α
s ∩ t: Set α
t

If we have a filter basis b, it is more convenient to write s ∈ b for s ∈ b.sets. We now define this notation.

instance: {α : Type u_1} → Membership (Set α) (Basis α)
instance : Membership: outParam (Type u_1) → Type u_1 → Type u_1
Membership (Set: Type u_1 → Type u_1
Set α: Type u_1
α) (Basis: Type u_1 → Type u_1
Basis α: Type u_1
α) :=
  ⟨fun b: Basis α
b s: Set α
s ↦ s: Set α
s ∈ b: Basis α
b.sets: {α : Type u_1} → Basis α → Set (Set α)
sets⟩

The definition of ∈.

@[simp]
theorem Basis.mem_def: ∀ {α : Type u_1} (b : Basis α) (s : Set α), s ∈ b ↔ s ∈ b.sets
Basis.mem_def (b: Basis α
b : Basis: Type u_1 → Type u_1
Basis α: Type u_1
α) (s: Set α
s : Set: Type u_1 → Type u_1
Set α: Type u_1
α) : s: Set α
s ∈ b: Basis α
b ↔ s: Set α
s ∈ b: Basis α
b.sets: {α : Type u_1} → Basis α → Set (Set α)
sets := byGoals accomplished! 🐙
  exact Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rflGoals accomplished! 🐙

The definition of equality between filter bases.

@[simp]
theorem Basis.eq_def: ∀ (b c : Basis α), b = c ↔ b.sets = c.sets
Basis.eq_def (b: Basis α
b c: Basis α
c : Basis: Type u_1 → Type u_1
Basis α: Type u_1
α) : b: Basis α
b = c: Basis α
c ↔ b: Basis α
b.sets: {α : Type u_1} → Basis α → Set (Set α)
sets = c: Basis α
c.sets: {α : Type u_1} → Basis α → Set (Set α)
sets := byGoals accomplished! 🐙
  apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introα: Type u_1
b, c: Basis α
mpb = c → b.sets = c.sets
α: Type u_1
b, c: Basis α
mprb.sets = c.sets → b = c
  .α: Type u_1
b, c: Basis α
mpb = c → b.sets = c.sets intro «b = c»: b = c
«b = c»α: Type u_1
b, c: Basis α
«b = c»: b = c
mpb.sets = c.sets
    rw [α: Type u_1
b, c: Basis α
«b = c»: b = c
mpb.sets = c.sets«b = c»: b = c
«b = c»α: Type u_1
b, c: Basis α
«b = c»: b = c
mpc.sets = c.sets]Goals accomplished! 🐙
  .α: Type u_1
b, c: Basis α
mprb.sets = c.sets → b = c intro «b.sets = c.sets»: b.sets = c.sets
«b.sets = c.sets»α: Type u_1
b, c: Basis α
«b.sets = c.sets»: b.sets = c.sets
mprb = c
    cases b: Basis α
bα: Type u_1
c: Basis α
sets✝: Set (Set α)
sets_nonempty✝: ∃ s, s ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
«b.sets = c.sets»: { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
mpr.mk{ sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
    cases c: Basis α
cα: Type u_1
sets✝¹: Set (Set α)
sets_nonempty✝¹: ∃ s, s ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → ∃ u ∈ sets✝¹, u ⊆ s ∩ t
sets✝: Set (Set α)
sets_nonempty✝: ∃ s, s ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
«b.sets = c.sets»: { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mk{ sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
    congrGoals accomplished! 🐙

-- 46
#explode Basis.eq_def: ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets
Basis.eq_defBasis.eq_def : ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets

0 │              │ α                        ├ Type u_1
1 │              │ b                        ├ Basis α
2 │              │ c                        ├ Basis α
3 │              │ «b = c»                  │ ┌ b = c
4 │3             │ congrArg                 │ │ (b.sets = c.sets) = (c.sets = c.sets)
5 │4             │ id                       │ │ (b.sets = c.sets) = (c.sets = c.sets)
6 │              │ Eq.refl                  │ │ c.sets = c.sets
7 │5,6           │ Eq.mpr                   │ │ b.sets = c.sets
8 │3,7           │ ∀I                       │ b = c → b.sets = c.sets
9 │              │ «b.sets = c.sets»        │ ┌ b.sets = c.sets
10│              │ sets✝                    │ │ ┌ Set (Set α)
11│              │ sets_nonempty✝           │ │ ├ ∃ s, s ∈ sets✝
12│              │ inter_mem_sets✝          │ │ ├ ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
13│              │ h✝                       │ │ ├ b =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
14│              │ «b.sets = c.sets»        │ │ │ ┌ { sets := sets✝, sets_nonempty := sets_nonempty✝,
      inter_mem_sets := inter_mem_sets✝ }.sets =
  c.sets
15│              │ sets✝                    │ │ │ │ ┌ Set (Set α)
16│              │ sets_nonempty✝           │ │ │ │ ├ ∃ s, s ∈ sets✝
17│              │ inter_mem_sets✝          │ │ │ │ ├ ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
18│              │ h✝                       │ │ │ │ ├ c =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
19│              │ «b.sets = c.sets»        │ │ │ │ │ ┌ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
20│              │ α                        │ │ │ │ │ │ ┌ Type u_1
21│              │ sets✝                    │ │ │ │ │ │ ├ Set (Set α)
22│              │ sets                     │ │ │ │ │ │ ├ Set (Set α)
23│              │ e_sets                   │ │ │ │ │ │ ├ sets✝ = sets
24│              │ sets_nonempty            │ │ │ │ │ │ │ ┌ ∃ s, s ∈ sets✝
25│              │ inter_mem_sets           │ │ │ │ │ │ │ ├ ∀ {s t : Set α},
  s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
26│              │ Eq.refl                  │ │ │ │ │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty,
    inter_mem_sets := inter_mem_sets } =
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets }
27│24,25,26      │ ∀I                       │ │ │ │ │ │ │ ∀ (sets_nonempty : ∃ s, s ∈ sets✝)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t),
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets }
28│27,23         │ Eq.rec                   │ │ │ │ │ │ │ ∀ (sets_nonempty : ∃ s, s ∈ sets✝)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t),
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
29│20,21,22,23,28│ ∀I                       │ │ │ │ │ │ ∀ {α : Type u_1} (sets sets_1 : Set (Set α))
  (e_sets : sets = sets_1) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets_1, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
30│29,19,11,12   │ ∀E                       │ │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
31│19,30         │ ∀I                       │ │ │ │ │ ∀
  («b.sets = c.sets» :
    { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
      { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets),
  { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
32│18            │ Eq.symm                  │ │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  c
33│31,32,14      │ Eq.ndrec                 │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  c
34│15,16,17,18,33│ ∀I                       │ │ │ │ ∀ (sets : Set (Set α)) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  c = { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } →
    { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } = c
35│              │ Eq.refl                  │ │ │ │ c = c
36│34,35         │ Basis.casesOn │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  c
37│14,36         │ ∀I                       │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    c.sets →
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
38│13            │ Eq.symm                  │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  b
39│37,38,9       │ Eq.ndrec                 │ │ │ b = c
40│10,11,12,13,39│ ∀I                       │ │ ∀ (sets : Set (Set α)) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  b = { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } → b = c
41│              │ Eq.refl                  │ │ b = b
42│40,41         │ Basis.casesOn │ │ b = c
43│9,42          │ ∀I                       │ b.sets = c.sets → b = c
44│8,43          │ Iff.intro                │ b = c ↔ b.sets = c.sets
45│0,1,2,44      │ ∀I                       │ ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets



theorem Basis.eq_def₁: ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets
Basis.eq_def₁ (b: Basis α
b c: Basis α
c : Basis: Type u_1 → Type u_1
Basis α: Type u_1
α) : b: Basis α
b = c: Basis α
c ↔ b: Basis α
b.sets: {α : Type u_1} → Basis α → Set (Set α)
sets = c: Basis α
c.sets: {α : Type u_1} → Basis α → Set (Set α)
sets := byGoals accomplished! 🐙
  apply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introα: Type u_1
b, c: Basis α
mpb = c → b.sets = c.sets
α: Type u_1
b, c: Basis α
mprb.sets = c.sets → b = c
  .α: Type u_1
b, c: Basis α
mpb = c → b.sets = c.sets intro «b = c»: b = c
«b = c»α: Type u_1
b, c: Basis α
«b = c»: b = c
mpb.sets = c.sets
    rw [α: Type u_1
b, c: Basis α
«b = c»: b = c
mpb.sets = c.sets«b = c»: b = c
«b = c»α: Type u_1
b, c: Basis α
«b = c»: b = c
mpc.sets = c.sets]Goals accomplished! 🐙
  .α: Type u_1
b, c: Basis α
mprb.sets = c.sets → b = c intro «b.sets = c.sets»: b.sets = c.sets
«b.sets = c.sets»α: Type u_1
b, c: Basis α
«b.sets = c.sets»: b.sets = c.sets
mprb = c
    cases b: Basis α
bα: Type u_1
c: Basis α
sets✝: Set (Set α)
sets_nonempty✝: ∃ s, s ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
«b.sets = c.sets»: { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
mpr.mk{ sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
    cases c: Basis α
cα: Type u_1
sets✝¹: Set (Set α)
sets_nonempty✝¹: ∃ s, s ∈ sets✝¹
inter_mem_sets✝¹: ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → ∃ u ∈ sets✝¹, u ⊆ s ∩ t
sets✝: Set (Set α)
sets_nonempty✝: ∃ s, s ∈ sets✝
inter_mem_sets✝: ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
«b.sets = c.sets»: { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
mpr.mk.mk{ sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
    simp_all onlyGoals accomplished! 🐙

-- 53
#explode Basis.eq_def₁: ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets
Basis.eq_def₁Basis.eq_def₁ : ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets

0 │              │ α                        ├ Type u_1
1 │              │ b                        ├ Basis α
2 │              │ c                        ├ Basis α
3 │              │ «b = c»                  │ ┌ b = c
4 │3             │ congrArg                 │ │ (b.sets = c.sets) = (c.sets = c.sets)
5 │4             │ id                       │ │ (b.sets = c.sets) = (c.sets = c.sets)
6 │              │ Eq.refl                  │ │ c.sets = c.sets
7 │5,6           │ Eq.mpr                   │ │ b.sets = c.sets
8 │3,7           │ ∀I                       │ b = c → b.sets = c.sets
9 │              │ «b.sets = c.sets»        │ ┌ b.sets = c.sets
10│              │ sets✝                    │ │ ┌ Set (Set α)
11│              │ sets_nonempty✝           │ │ ├ ∃ s, s ∈ sets✝
12│              │ inter_mem_sets✝          │ │ ├ ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
13│              │ h✝                       │ │ ├ b =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
14│              │ «b.sets = c.sets»        │ │ │ ┌ { sets := sets✝, sets_nonempty := sets_nonempty✝,
      inter_mem_sets := inter_mem_sets✝ }.sets =
  c.sets
15│              │ sets✝                    │ │ │ │ ┌ Set (Set α)
16│              │ sets_nonempty✝           │ │ │ │ ├ ∃ s, s ∈ sets✝
17│              │ inter_mem_sets✝          │ │ │ │ ├ ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
18│              │ h✝                       │ │ │ │ ├ c =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
19│              │ «b.sets = c.sets»        │ │ │ │ │ ┌ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
      inter_mem_sets := inter_mem_sets✝¹ }.sets =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
20│              │ α                        │ │ │ │ │ │ ┌ Type u_1
21│              │ sets✝                    │ │ │ │ │ │ ├ Set (Set α)
22│              │ sets                     │ │ │ │ │ │ ├ Set (Set α)
23│              │ e_sets                   │ │ │ │ │ │ ├ sets✝ = sets
24│              │ sets_nonempty            │ │ │ │ │ │ │ ┌ ∃ s, s ∈ sets✝
25│              │ inter_mem_sets           │ │ │ │ │ │ │ ├ ∀ {s t : Set α},
  s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t
26│              │ Eq.refl                  │ │ │ │ │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty,
    inter_mem_sets := inter_mem_sets } =
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets }
27│24,25,26      │ ∀I                       │ │ │ │ │ │ │ ∀ (sets_nonempty : ∃ s, s ∈ sets✝)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t),
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets }
28│27,23         │ Eq.rec                   │ │ │ │ │ │ │ ∀ (sets_nonempty : ∃ s, s ∈ sets✝)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u ∈ sets✝, u ⊆ s ∩ t),
  { sets := sets✝, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
29│20,21,22,23,28│ ∀I                       │ │ │ │ │ │ ∀ {α : Type u_1} (sets sets_1 : Set (Set α))
  (e_sets : sets = sets_1) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } =
    { sets := sets_1, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
30│19            │ id                       │ │ │ │ │ │ sets✝¹ = sets✝
31│30            │ id                       │ │ │ │ │ │ sets✝¹ = sets✝
32│29,31,11,12   │ ∀E                       │ │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ }
33│32            │ congrArg                 │ │ │ │ │ │ ({ sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }) =
  ({ sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ })
34│              │ eq_self                  │ │ │ │ │ │ ({ sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ } =
    { sets := sets✝, sets_nonempty := ⋯, inter_mem_sets := ⋯ }) =
  True
35│33,34         │ Eq.trans                 │ │ │ │ │ │ ({ sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }) =
  True
36│35            │ of_eq_true               │ │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
37│19,36         │ ∀I                       │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets →
  { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
38│18            │ Eq.symm                  │ │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  c
39│37,38,14      │ Eq.ndrec                 │ │ │ │ │ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹,
    inter_mem_sets := inter_mem_sets✝¹ } =
  c
40│15,16,17,18,39│ ∀I                       │ │ │ │ ∀ (sets : Set (Set α)) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  c = { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } →
    { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } = c
41│              │ Eq.refl                  │ │ │ │ c = c
42│40,41         │ Basis.casesOn │ │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  c
43│14,42         │ ∀I                       │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    c.sets →
  { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
44│13            │ Eq.symm                  │ │ │ { sets := sets✝, sets_nonempty := sets_nonempty✝,
    inter_mem_sets := inter_mem_sets✝ } =
  b
45│43,44,9       │ Eq.ndrec                 │ │ │ b = c
46│10,11,12,13,45│ ∀I                       │ │ ∀ (sets : Set (Set α)) (sets_nonempty : ∃ s, s ∈ sets)
  (inter_mem_sets : ∀ {s t : Set α}, s ∈ sets → t ∈ sets → ∃ u ∈ sets, u ⊆ s ∩ t),
  b = { sets := sets, sets_nonempty := sets_nonempty, inter_mem_sets := inter_mem_sets } → b = c
47│              │ Eq.refl                  │ │ b = b
48│46,47         │ Basis.casesOn │ │ b = c
49│9,48          │ ∀I                       │ b.sets = c.sets → b = c
50│8,49          │ Iff.intro                │ b = c ↔ b.sets = c.sets
51│0,1,2,50      │ ∀I                       │ ∀ {α : Type u_1} (b c : Basis α), b = c ↔ b.sets = c.sets

Filters

Notation s ∈ f

The equality between filters

Trivial lemmas

Filter bases

Notation `s ∈ f`