awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁

Tactic:
(hS s hs).1

Premises used: And.left
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂

Tactic:
(hS s hs).2

Premises used: And.right
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁

Tactic:
exacts [(hS s hs).1, (hS s hs).2]

Premises used: And.right, And.left
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α_1 : Type u_2
β_1 : Type u_3
l_1 : Filter α_1
inst : CountableInterFilter l_1
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst_1 : CountableInterFilter l
inst_2 : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
simp_rw : ∀ (i : Set (α × β)) (hi : i ∈ S), i ∈ l.curry m
⊢ ⋂₀ S ∈ l.curry m

Tactic:
simp_rw [mem_curry_iff, mem_sInter, eventually_countable_ball (p := fun _ _ _ => (_, _) ∈ _) Sct,
    eventually_countable_ball (p := fun _ _ _ => ∀ᶠ (_ : β) in m, _)  Sct, ← mem_curry_iff]

Premises used: Filter.mem_curry_iff, eventually_countable_ball, Set.mem_sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α_1 : Type u_2
β_1 : Type u_3
l_1 : Filter α_1
inst : CountableInterFilter l_1
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst_1 : CountableInterFilter l
inst_2 : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ (i : Set (α × β)) (hi : i ∈ S), i ∈ l.curry m

Tactic:
hS
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α_1 : Type u_2
β_1 : Type u_3
l_1 : Filter α_1
inst : CountableInterFilter l_1
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst_1 : CountableInterFilter l
inst_2 : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ (i : Set (α × β)) (hi : i ∈ S), i ∈ l.curry m

Tactic:
exact hS
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
mp : s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
mpr : (∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g
⊢ s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 s : Set α
hs : s ∈ g
⊢ {s} ⊆ g ∧ Set.Countable (α := Set α) {s} ∧ ⋂₀ {s} ⊆ s

Tactic:
simp [hs, subset_refl]

Premises used: subset_refl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 s : Set α
hs : s ∈ g
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
exact ⟨{s}, by simp [hs, subset_refl]⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
⊢ ∅ ⊆ g ∧ Set.Countable.{u_2} (α := Set α) ∅ ∧ Subset.{u_2} (α := Set α) (⋂₀ ∅) univ

Tactic:
simp
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ univ

Tactic:
exact ⟨∅, by simp⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s s_1 t : Set α
h : CountableGenerateSets g s_1
h_1 : s_1 ⊆ t
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s_1
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ t

Tactic:
Exists.imp (fun S => ?_) ih

Premises used: Exists.imp
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s s_1 t : Set α
h : CountableGenerateSets g s_1
h_1 : s_1 ⊆ t
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s_1
mp : ∀ (S : Set (Set α)), S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ t

Tactic:
refine Exists.imp (fun S => ?_) ih

Premises used: Exists.imp
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s s_1 t : Set α
h : CountableGenerateSets g s_1
h_1 : s_1 ⊆ t
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s_1
S : Set (Set α)
mp mp₁ :
  ∀ (w : Set (Set α)),
    S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
mp₂ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S ⊆ g
mp₃ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S.Countable
mp₄ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → ⋂₀ S ⊆ t
mp₅ mp₆ mp₇ mp₈ mp₉ mp₁₀ mp₁₁ mp₁₂ :
  ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → ∀ ⦃a : α⦄, a ∈ ⋂₀ S → a ∈ t
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t

Tactic:
tauto
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
mp :
  ∀ (T : (s : Set α) → s ∈ S → Set (Set α)) (Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g)
    (Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable) (hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s),
    ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
simpa
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
mp : ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ ⋂₀ S
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
mp : ∀ t' ∈ S, ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ t'
⊢ ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ ⋂₀ S

Tactic:
apply subset_sInter

Premises used: Set.subset_sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ s

Tactic:
subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Premises used: Set.subset_iUnion₂, subset_trans, Set.sInter_subset_sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 : Set α
S : Set (Set α)
Sct : S.Countable
h : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ s

Tactic:
exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Premises used: Set.subset_iUnion₂, subset_trans, Set.sInter_subset_sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
mp₁ : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ univ
mp₂ :
  ∀ {s t : Set α},
    CountableGenerateSets g s → s ⊆ t → ∀ (ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s), ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ t
mp₃ :
  ∀ {S : Set (Set α)} (Sct : S.Countable),
    (∀ s ∈ S, CountableGenerateSets g s) →
      ∀ (ih : ∀ s ∈ S, ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s), ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
induction h with
    | @basic s hs => exact ⟨{s}, by simp [hs, subset_refl]⟩
    | univ => exact ⟨∅, by simp⟩
    | superset _ _ ih => refine Exists.imp (fun S => ?_) ih; tauto
    | @sInter S Sct _ ih =>
      choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
      apply subset_sInter
      intro s H
      exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Premises used: Set.univ, Set.subset_sInter, Set.sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
mpr : ∀ (S : Set (Set α)) (Sg : S ⊆ g) (Sct : S.Countable) (hS : ⋂₀ S ⊆ s), s ∈ countableGenerate g
⊢ s ∈ countableGenerate g

Tactic:
rcases h with ⟨S, Sg, Sct, hS⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g

Tactic:
mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS

Premises used: Iff.mpr, countable_sInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s
mpr : ∀ s ∈ S, s ∈ countableGenerate g
⊢ s ∈ countableGenerate g

Tactic:
refine mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS

Premises used: Iff.mpr, countable_sInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s_1
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g

Tactic:
CountableGenerateSets.basic (Sg H)

Premises used: Set.Mem, Filter.CountableGenerateSets.basic
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
s_1 : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s_1
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g

Tactic:
exact CountableGenerateSets.basic (Sg H)

Premises used: Filter.CountableGenerateSets.basic
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
mp : f ≤ countableGenerate g → g ⊆ f.sets
mpr : g ⊆ f.sets → f ≤ countableGenerate g
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

Tactic:
subset_trans (fun s => CountableGenerateSets.basic) h

Premises used: subset_trans, Filter.CountableGenerateSets.basic
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

Tactic:
exact subset_trans (fun s => CountableGenerateSets.basic) h

Premises used: subset_trans
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s s_1 : Set α
hs : s_1 ∈ g
⊢ s_1 ∈ f

Tactic:
h hs
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s s_1 : Set α
hs : s_1 ∈ g
⊢ s_1 ∈ f

Tactic:
exact h hs
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s s_1 t : Set α
h_1 : CountableGenerateSets g s_1
st : s_1 ⊆ t
ih : s_1 ∈ f
⊢ t ∈ f

Tactic:
mem_of_superset ih st

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s s_1 t : Set α
h_1 : CountableGenerateSets g s_1
st : s_1 ⊆ t
ih : s_1 ∈ f
⊢ t ∈ f

Tactic:
exact mem_of_superset ih st

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : S.Countable
h_1 : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, s ∈ f
⊢ ⋂₀ S ∈ f

Tactic:
(countable_sInter_mem Sct).mpr ih

Premises used: Iff.mpr, countable_sInter_mem
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : S.Countable
h_1 : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, s ∈ f
⊢ ⋂₀ S ∈ f

Tactic:
exact (countable_sInter_mem Sct).mpr ih

Premises used: Iff.mpr, countable_sInter_mem
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
mpr : ∀ {s : Set α} (hs : s ∈ g), s ∈ f
mpr₁ : univ ∈ f
mpr₂ : ∀ {s t : Set α}, CountableGenerateSets g s → ∀ (st : s ⊆ t) (ih : s ∈ f), t ∈ f
mpr₃ : ∀ {S : Set (Set α)} (Sct : S.Countable), (∀ s ∈ S, CountableGenerateSets g s) → ∀ (ih : ∀ s ∈ S, s ∈ f), ⋂₀ S ∈ f
⊢ s ∈ f

Tactic:
induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (countable_sInter_mem Sct).mpr ih

Premises used: Set.univ, Filter.univ_mem, Set.sInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
⊢ IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

Tactic:
⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩

Premises used: inferInstance, IsGreatest, And.intro, Filter.CountableGenerateSets.basic
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
refine :
  Membership.mem (γ := Set (Filter α)) (upperBounds {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets})
    (countableGenerate g)
⊢ IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

Tactic:
refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf rwa rwa₁ rwa₂ rwa₃ : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Tactic:
rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]

Premises used: Filter.le_countableGenerate_iff_of_countableInterFilter
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
⊢ ∃ (S : Set (Set α)), S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
h.1

Premises used: HasCountableSeparatingOn.exists_countable_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
⊢ ∃ (S : Set (Set α)), S.Nonempty ∧ S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
let ⟨S, hSc, hSp, hSt⟩ := exists_countable_separating α p t
  ⟨insert s₀ S, insert_nonempty _ _, hSc.insert _, forall_insert_of_forall hSp hp,
    fun x hx y hy hxy ↦ hSt x hx y hy <| forall_of_forall_insert hxy⟩

Premises used: Set.insert_nonempty, exists_countable_separating, Exists, Insert.insert, Set.forall_insert_of_forall, And, Set.Nonempty, And.intro, Set.Countable.insert, Exists.intro, _private.0.exists_nonempty_countable_separating.match_1, Set.forall_of_forall_insert, Set.Countable
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
rcases :
  ∀ (S : Set (Set α)) (hSne : S.Nonempty) (hSc : S.Countable)
    (hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
    ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩

Premises used: exists_nonempty_countable_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : S.Nonempty
hSc : S.Countable
hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
rcases :
  ∀ (S : ℕ → Set α) (hSne : (range S).Nonempty) (hSc : (range S).Countable)
    (hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y),
    ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩

Premises used: Set.Countable.exists_eq_range, rfl
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
h : (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
use S
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
simpa only [forall_mem_range] using hS

Premises used: Set.forall_mem_range
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h : 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
rcases :
  ∀ (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),
    HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn α p t

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

Premises used: HasCountableSeparatingOn.exists_countable_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h : 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
choose! :
  ∀ (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),
    HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn α p t

Tactic:
choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h : 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
⊢ HasCountableSeparatingOn α p t

Tactic:
⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩

Premises used: Iff.mpr, Set.Countable.image, And.intro, HasCountableSeparatingOn.mk, Exists.intro, Set.image, Set.forall_mem_image
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h : 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
refine : ∀ (x : α) (hx : x ∈ t) (y : α) (hy : y ∈ t) (h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s), x = y
⊢ HasCountableSeparatingOn α p t

Tactic:
refine ⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
-- 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
⊢ x = y

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

Premises used: trivial, Subtype.mk, congr_arg, Subtype.val