awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
have refine : ∀ (i : Set α) (hi : i ∈ S), (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i
Tactic: refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i
have rw : (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
Tactic: rw [hst i hi]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
have h₁ : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ⊆ s i hi
Tactic: apply inter_subset_inter
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
h₁ : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ⊆ s i hi
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
have h₂ : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ t i hi
Tactic: apply inter_subset_inter
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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₂
⊢ CountableInterFilter (l₁ ⊔ l₂)
have refine_1 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₁
Tactic: refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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₂
refine_1 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₁
⊢ CountableInterFilter (l₁ ⊔ l₂)
have refine_2 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₂
Tactic: refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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 ∈ l₁
have refine_1 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₁
Tactic: refine (countable_sInter_mem hSc).2 fun s hs => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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 ∈ l₂
have refine_2 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₂
Tactic: refine (countable_sInter_mem hSc).2 fun s hs => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have mp : s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
mp : s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have mpr : (∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
have mp : ∀ (S : Set (Set α)), S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
Tactic: refine Exists.imp (fun S => ?_) ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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 α)
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
have mp : ∀ (w : Set (Set α)),
  S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
have mp₂ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S ⊆ g
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
have mp₃ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → S.Countable
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
have mp₄ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → ⋂₀ S ⊆ t
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s_1 → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t
have mp₅ : ∀ (w : Set (Set α)), S ⊆ g → w ⊆ g → S.Countable → ⋂₀ S ⊆ s_1 → w.Countable → ⋂₀ w ⊆ s_1 → ∀ ⦃a : α⦄, a ∈ ⋂₀ S → a ∈ t
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S
have 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
Tactic: choose T Tg Tct hT using ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S
have mp : ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ ⋂₀ S
Tactic: refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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 ⊆ ⋂₀ S
have mp : ∀ t' ∈ S, ⋂₀ ⋃ (s : Set α), ⋃ (H : s ∈ S), T s H ⊆ t'
Tactic: apply subset_sInter
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have mp : ∀ {s : Set α} (hs : s ∈ g), ∃ 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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have mp₁ : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ univ
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have mp₂ : ∀ {s t : Set α},
  CountableGenerateSets g s → s ⊆ t → ∀ (ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s), ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ t
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
have 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
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
have mpr : ∀ (S : Set (Set α)) (Sg : S ⊆ g) (Sct : S.Countable) (hS : ⋂₀ S ⊆ s), s ∈ countableGenerate g
Tactic: rcases h with ⟨S, Sg, Sct, hS⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
have mpr : ∀ s ∈ S, s ∈ countableGenerate g
Tactic: refine mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets
have mp : f ≤ countableGenerate g → g ⊆ f.sets
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
mp : f ≤ countableGenerate g → g ⊆ f.sets
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets
have mpr : g ⊆ f.sets → f ≤ countableGenerate g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
f : Filter α
inst : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f
have mpr : ∀ {s : Set α} (hs : s ∈ g), 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ s ∈ f
have mpr₁ : univ ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ s ∈ f
have mpr₂ : ∀ {s t : Set α}, CountableGenerateSets g s → ∀ (st : s ⊆ t) (ih : s ∈ f), t ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
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
⊢ s ∈ f
have mpr₃ : ∀ {S : Set (Set α)} (Sct : S.Countable), (∀ s ∈ S, CountableGenerateSets g s) → ∀ (ih : ∀ s ∈ S, 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
g : Set (Set α)
⊢ IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)
have refine : Membership.mem (γ := Set (Filter α)) (upperBounds {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets})
  (countableGenerate g)
Tactic: refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst : HasCountableSeparatingOn α p t
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
have 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
Tactic: rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
have 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
Tactic: rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩
Cleared hypotheses: S, hSne, hSc, hS
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
⊢ ∃ (S : ℕ → Set α), (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
have h : (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
Tactic: use S
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
⊢ HasCountableSeparatingOn α p t
have 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
Tactic: rcases h.1 with ⟨S, hSc, hSq, hS⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
⊢ HasCountableSeparatingOn α p t
have 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
Tactic: choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
have refine : ∀ (x : α) (hx : x ∈ t) (y : α) (hy : y ∈ t) (h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s), x = y
Tactic: refine ⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
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
have 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
Tactic: refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)