awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h_1 : HasCountableSeparatingOn (↑t : Type u_1) q univ
hpq : ∀ (U : Set (↑t : Type u_1)), q U → ∃ (V : Set α), p V ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V = U
S : Set (Set (↑t : Type u_1))
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)), Membership.mem (γ := Set (↑t : Type u_1)) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : (s : Set (↑t : Type u_1)) → Set α
hpV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), p (V s)
hV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
refine :
  ∀ (U : Set (↑t : Type u_1)) (hU : U ∈ S),
    Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ U ↔ Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy ∈ U
⊢ x = y

Tactic:
refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)

Premises used: trivial, Subtype.mk, congr_arg, Subtype.val
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h_1 : HasCountableSeparatingOn (↑t : Type u_1) q univ
hpq : ∀ (U : Set (↑t : Type u_1)), q U → ∃ (V : Set α), p V ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V = U
S : Set (Set (↑t : Type u_1))
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)), Membership.mem (γ := Set (↑t : Type u_1)) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : (s : Set (↑t : Type u_1)) → Set α
hpV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), p (V s)
hV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set (↑t : Type u_1)
hU : U ∈ S
rw :
  Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx) ↔
    Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ U ↔ Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy ∈ U

Tactic:
rw [← hV U hU]
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h_1 : HasCountableSeparatingOn (↑t : Type u_1) q univ
hpq : ∀ (U : Set (↑t : Type u_1)), q U → ∃ (V : Set α), p V ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V = U
S : Set (Set (↑t : Type u_1))
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)), Membership.mem (γ := Set (↑t : Type u_1)) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : (s : Set (↑t : Type u_1)) → Set α
hpV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), p (V s)
hV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set (↑t : Type u_1)
hU : U ∈ S
⊢ Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx) ↔
    Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy)

Tactic:
h _ (mem_image_of_mem _ hU)

Premises used: Set.Mem, setOf, Set.preimage, Set.mem_image_of_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h_1 : HasCountableSeparatingOn (↑t : Type u_1) q univ
hpq : ∀ (U : Set (↑t : Type u_1)), q U → ∃ (V : Set α), p V ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V = U
S : Set (Set (↑t : Type u_1))
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)), Membership.mem (γ := Set (↑t : Type u_1)) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : (s : Set (↑t : Type u_1)) → Set α
hpV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), p (V s)
hV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set (↑t : Type u_1)
hU : U ∈ S
⊢ Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx) ↔
    Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy)

Tactic:
exact h _ (mem_image_of_mem _ hU)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
mp :
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ →
    HasCountableSeparatingOn α p t
mpr :
  HasCountableSeparatingOn α p t →
    HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ ↔
    HasCountableSeparatingOn α p t

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
h :
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

Tactic:
h.of_subtype <| fun s ↦ id

Premises used: id, HasCountableSeparatingOn.of_subtype
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
h :
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

Tactic:
exact h.of_subtype <| fun s ↦ id

Premises used: id, HasCountableSeparatingOn.of_subtype
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
mpr :
  ∀ (S : Set (Set α)) (Sct : S.Countable) (Sp : ∀ s ∈ S, p s) (hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
    HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ

Tactic:
rcases h with ⟨S, Sct, Sp, hS⟩
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
left :
  ∀ (s : Set (↑t : Type u_1)),
    Membership.mem (γ := Set (Set (↑t : Type u_1)))
        {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
      ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = s
right :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)),
        Membership.mem (γ := Set (↑t : Type u_1)) univ y →
          (∀ (s : Set (↑t : Type u_1)),
              Membership.mem (γ := Set (Set (↑t : Type u_1)))
                  {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
                (x ∈ s ↔ y ∈ s)) →
            x = y
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ

Tactic:
use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_

Premises used: Set.Countable.image, Subtype.val
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t_1 : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t_1, ∀ y ∈ t_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
t : Set α
tS : t ∈ S
⊢ ∃ (v : Set α),
    p v ∧
      Eq (α := Set (↑t_1 : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t_1) ⁻¹' v)
        (Subtype.val (p := fun (x : α) ↦ x ∈ t_1) ⁻¹' t)

Tactic:
⟨t, Sp _ tS, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t_1 : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t_1, ∀ y ∈ t_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
t : Set α
tS : t ∈ S
⊢ ∃ (v : Set α),
    p v ∧
      Eq (α := Set (↑t_1 : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t_1) ⁻¹' v)
        (Subtype.val (p := fun (x : α) ↦ x ∈ t_1) ⁻¹' t)

Tactic:
exact ⟨t, Sp _ tS, rfl⟩
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : (↑t : Type u_1)
hxy :
  ∀ (s : Set (↑t : Type u_1)),
    Membership.mem (γ := Set (Set (↑t : Type u_1)))
        {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
      (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
Subtype.val_injective <| hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
    fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩

Premises used: Subtype.coe_prop, Subtype.val_injective, Set.preimage, And.intro, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : (↑t : Type u_1)
hxy :
  ∀ (s : Set (↑t : Type u_1)),
    Membership.mem (γ := Set (Set (↑t : Type u_1)))
        {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
      (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
exact Subtype.val_injective <| hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
    fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩

Premises used: Subtype.coe_prop, Subtype.val_injective, Set.preimage, And.intro, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
rcases :
  ∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : ∀ s ∈ S, p s)
    (hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y), ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
rcases h.1 with ⟨S, hSc, hSp, hS⟩

Premises used: HasCountableSeparatingOn.exists_countable_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩

Premises used: Set.iInter, Compl.compl, Filter.sets, Inter.inter, And.intro, Exists.intro, Set.sInter
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
refine_1 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s
refine_2 : (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton
refine_3 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s

Tactic:
fun _ h ↦ h.1.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s

Tactic:
exact fun _ h ↦ h.1.1
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
⊢ (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i

Tactic:
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy

Premises used: Set.mem_inter_iff, Set.mem_iInter, Set.mem_sInter, Set.mem_compl_iff
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
hx₁ : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
⊢ (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i

Tactic:
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy

Premises used: Set.mem_inter_iff, Set.mem_iInter, Set.mem_sInter, Set.mem_compl_iff
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ 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_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
⊢ x = y

Tactic:
hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)

Premises used: And.left
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ 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_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
refine_2 : ∀ (s : Set α) (hsS : s ∈ S), x ∈ s ↔ y ∈ s
⊢ x = y

Tactic:
refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)

Premises used: And.left
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s_1 : Set α
h : HasCountableSeparatingOn α p s_1
hs : s_1 ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
s : Set α
hsS : s ∈ S
hsl : s ∈ l
⊢ x ∈ s ↔ y ∈ s

Tactic:
simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s_1 : Set α
h : HasCountableSeparatingOn α p s_1
hs : s_1 ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s

Tactic:
simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]

Premises used: And.right
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s_1 : Set α
h : HasCountableSeparatingOn α p s_1
hs : s_1 ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
s : Set α
hsS : s ∈ S
⊢ s ∈ l ∨ sᶜ ∈ l

Tactic:
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]
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l

Tactic:
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)

Premises used: countable_bInter_mem, Iff.mpr, Filter.inter_mem, id, Set.inter_subset_left, And.right, Set.Countable.mono, Filter.iInter_mem', countable_sInter_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
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 : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l

Tactic:
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)

Premises used: countable_bInter_mem, Iff.mpr, Filter.inter_mem, id, Set.inter_subset_left, And.right, Set.Countable.mono, Filter.iInter_mem', countable_sInter_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
rcases : ∀ (t : Set α) (hts : t ⊆ s) (ht : t.Subsingleton) (htl : t ∈ l), ∃ a ∈ s, {a} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩

Premises used: Filter.exists_subset_subsingleton_mem_of_forall_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
inl : ∀ (hts : ∅ ⊆ s) (ht : Set.Subsingleton.{u_1} (α := α) ∅) (htl : ∅ ∈ l), ∃ a ∈ s, {a} ∈ l
inr : ∀ (x : α) (hts : {x} ⊆ s) (ht : Set.Subsingleton (α := α) {x}) (htl : {x} ∈ l), ∃ a ∈ s, {a} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : Set.Subsingleton.{u_1} (α := α) ∅
htl : ∅ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩

Premises used: Exists.imp, And.intro, Set.empty_subset, Singleton.singleton, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : Set.Subsingleton.{u_1} (α := α) ∅
htl : ∅ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩

Premises used: Exists.imp
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : Set.Subsingleton (α := α) {x}
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
⟨x, hts rfl, htl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : Set.Subsingleton (α := α) {x}
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
exact ⟨x, hts rfl, htl⟩
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
s : Set α
inst_2 : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inl : ∀ [HasCountableSeparatingOn α p ∅] (hs : ∅ ∈ l), ∃ (a : α), {a} ∈ l
inr : ∀ (hne : s.Nonempty), ∃ (a : α), {a} ∈ l
⊢ ∃ (a : α), {a} ∈ l

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst_2 : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ (a : α), {a} ∈ l

Tactic:
‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩

Premises used: Nonempty.elim, Set.empty_subset, Exists.intro, Singleton.singleton, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst_2 : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ (a : α), {a} ∈ l

Tactic:
exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩

Premises used: Nonempty.elim