[GOAL]
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : Set.Nonempty S
hSc : Set.Countable S
hS :
  (∀ (s : Set α), s ∈ S → p s) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : Set.Nonempty (range S)
hSc : Set.Countable (range S)
hS :
  (∀ (s : Set α), s ∈ range S → p s) ∧
    ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ range S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
use S
[GOAL]
case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : Set.Nonempty (range S)
hSc : Set.Countable (range S)
hS :
  (∀ (s : Set α), s ∈ range S → p s) ∧
    ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ range S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
simpa only [forall_range_iff] using hS
[GOAL]
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
rcases h.1 with ⟨S, hSc, hSq, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
refine ⟨⟨V '' S, hSc.image _, ball_image_iff.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
⊢ x = y
[PROOFSTEP]
refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
U : Set ↑t
hU : U ∈ S
⊢ { val := x, property := hx } ∈ U ↔ { val := y, property := hy } ∈ U
[PROOFSTEP]
rw [← hV U hU]
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
U : Set ↑t
hU : U ∈ S
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' V U ↔ { val := y, property := hy } ∈ Subtype.val ⁻¹' V U
[PROOFSTEP]
exact h _ (mem_image_of_mem _ hU)
[GOAL]
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ t, t ⊆ s ∧ Set.Subsingleton t ∧ t ∈ l
[PROOFSTEP]
rcases h.1 with ⟨S, hSc, hSp, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ t, t ⊆ s ∧ Set.Subsingleton t ∧ t ∈ l
[PROOFSTEP]
refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ ⊆ s
[PROOFSTEP]
exact fun _ h ↦ h.1.1
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ Set.Subsingleton (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ)
[PROOFSTEP]
intro x hx y hy
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y
[PROOFSTEP]
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy 
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
⊢ x = y
[PROOFSTEP]
refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
cases hl s (hSp s hsS) with
| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
x✝ : s ∈ l ∨ sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
cases hl s (hSp s hsS) with
| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2.inl
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : s ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]

| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
[GOAL]
case intro.intro.intro.refine_2.inl
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : s ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
[GOAL]
case intro.intro.intro.refine_2.inr
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]

| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2.inr
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_3
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ ∈ l
[PROOFSTEP]
exact
  inter_mem (inter_mem hs ((countable_sInter_mem (hSc.mono (inter_subset_left _ _))).2 fun _ h ↦ h.2))
    ((countable_bInter_mem hSc).2 fun U hU ↦ iInter_mem.2 id)
[GOAL]
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : Set.Subsingleton t
htl : t ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
[GOAL]
case intro.intro.intro.inl
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : Set.Subsingleton ∅
htl : ∅ ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩
[GOAL]
case intro.intro.intro.inr.intro
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : Set.Subsingleton {x}
htl : {x} ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
exact ⟨x, hts rfl, htl⟩
[GOAL]
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | hne
[GOAL]
case inl
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩
[GOAL]
case inr
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : Set.Nonempty s
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦ And.right
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
⊢ f =ᶠ[l] g
[PROOFSTEP]
rcases h'.1 with ⟨S, hSc, hSp, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : Set.Countable S
hSp : ∀ (s : Set β), s ∈ S → p s
hS : ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → (∀ (s : Set β), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ f =ᶠ[l] g
[PROOFSTEP]
have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s := (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : Set.Countable S
hSp : ∀ (s : Set β), s ∈ S → p s
hS : ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → (∀ (s : Set β), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
H : ∀ᶠ (x : α) in l, ∀ (s : Set β), s ∈ S → (f x ∈ s ↔ g x ∈ s)
⊢ f =ᶠ[l] g
[PROOFSTEP]
filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx
