awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
haveI :
  ∀ (this : Encodable (↑S : Type u_4)),
    ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
haveI := hS.toEncodable
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable (↑S : Type u_4)
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
EventuallyLE.countable_iInter fun i => h i i.2

Premises used: Filter.EventuallyLE.countable_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable (↑S : Type u_4)
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
exact EventuallyLE.countable_iInter fun i => h i i.2
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
⊢ ⋂ (i : ι), ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

Tactic:
(EventuallyLE.countable_bInter hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.countable_bInter hS fun i hi => (h i hi).symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.countable_bInter, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
⊢ CountableInterFilter (ofCountableInter l hl h_mono)

Tactic:
⟨hl⟩

Premises used: CountableInterFilter.mk
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Set (Set α)
hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s : Set α
⊢ s ∈ ofCountableInter l hl h_mono ↔ s ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
refine_1 :
  ∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : S ⊆ {s : Set α | sᶜ ∈ l}),
    Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
refine_2 :
  ∀ (s t : Set α) (ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s) (hsub : s ⊆ t),
    Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t
⊢ Filter α

Tactic:
refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
refine_1 : ⋃₀ (compl '' S) ∈ l
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)

Tactic:
rw [mem_setOf_eq, compl_sInter]

Premises used: Set.compl_sInter, Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
refine_1 : ∀ s ∈ compl '' S, s ∈ l
⊢ ⋃₀ (compl '' S) ∈ l

Tactic:
apply hUnion (compl '' S) (hSc.image _)

Premises used: Compl.compl, Set.Countable.image, Set.image
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : s ∈ compl '' S
⊢ ∃ x ∈ S, xᶜ = s

Tactic:
rw [mem_image] at hs

Premises used: Set.mem_image
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
refine_1 : ∀ (t : Set α) (ht : t ∈ S), tᶜ ∈ l
⊢ s ∈ l

Tactic:
rcases hs with ⟨t, ht, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
t : Set α
ht : t ∈ S
⊢ tᶜ ∈ l

Tactic:
apply hSp ht
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
refine_2 : tᶜ ∈ l
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t

Tactic:
rw [mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
⊢ tᶜ ⊆ sᶜ

Tactic:
rw [← compl_subset_compl] at hsub

Premises used: Set.compl_subset_compl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
hmono sᶜ ht tᶜ hsub

Premises used: Compl.compl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
exact hmono sᶜ ht tᶜ hsub

Premises used: Compl.compl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
h₁ : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ CountableInterFilter (ofCountableUnion l h₁ h₂)

Tactic:
countableInter_ofCountableInter ..

Premises used: Filter.countableInter_ofCountableInter, Filter.ofCountableUnion
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Set (Set α)
hunion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s : Set α
⊢ s ∈ ofCountableUnion l hunion hmono ↔ l sᶜ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
s : Set α
⊢ CountableInterFilter (𝓟 s)

Tactic:
⟨fun _ _ hS => subset_sInter hS⟩

Premises used: Set.subset_sInter, CountableInterFilter.mk
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
rw : CountableInterFilter.{u_2} (α := α) (𝓟 ∅)
⊢ CountableInterFilter.{u_2} (α := α) ⊥

Tactic:
rw [← principal_empty]

Premises used: Filter.principal_empty
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
⊢ CountableInterFilter.{u_2} (α := α) (𝓟 ∅)

Tactic:
apply countableInterFilter_principal

Premises used: countableInterFilter_principal
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
rw : CountableInterFilter.{u_2} (α := α) (𝓟 univ)
⊢ CountableInterFilter.{u_2} (α := α) ⊤

Tactic:
rw [← principal_univ]

Premises used: Filter.principal_univ
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
⊢ CountableInterFilter.{u_2} (α := α) (𝓟 univ)

Tactic:
apply countableInterFilter_principal

Premises used: countableInterFilter_principal
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)

Tactic:
⟨fun S hSc hS => ?_⟩

Premises used: CountableInterFilter.mk
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
refine : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ comap f l), ⋂₀ S ∈ comap f l
⊢ CountableInterFilter (comap f l)

Tactic:
refine ⟨fun S hSc hS => ?_⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ comap f l
choose! : ∀ (t : (s : Set α) → Set β) (htl : ∀ s ∈ S, t s ∈ l) (ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s), ⋂₀ S ∈ comap f l
⊢ ⋂₀ S ∈ comap f l

Tactic:
choose! t htl ht using hS
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ⋂ s ∈ S, t s ∈ l

Tactic:
have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ ⋂₀ S ∈ comap f l

Tactic:
⟨_, this, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
refine : f ⁻¹' ⋂ s ∈ S, t s ⊆ ⋂₀ S
⊢ ⋂₀ S ∈ comap f l

Tactic:
refine ⟨_, this, ?_⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ f ⁻¹' ⋂ s ∈ S, t s ⊆ ⋂₀ S

Tactic:
simpa [preimage_iInter] using iInter₂_mono ht

Premises used: Set.iInter₂_mono, Set.preimage_iInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)

Tactic:
⟨fun S hSc hS => ?_⟩

Premises used: CountableInterFilter.mk
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
refine : ∀ (S : Set (Set β)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ map f l), ⋂₀ S ∈ map f l
⊢ CountableInterFilter (map f l)

Tactic:
refine ⟨fun S hSc hS => ?_⟩
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ map f l
simp : ∀ (hS : ∀ s ∈ S, f ⁻¹' s ∈ l), ⋂ i ∈ S, f ⁻¹' i ∈ l
⊢ ⋂₀ S ∈ map f l

Tactic:
simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢

Premises used: Set.sInter_eq_biInter, Set.preimage_iInter₂, Filter.mem_map
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l

Tactic:
(countable_bInter_mem hSc).2 hS

Premises used: countable_bInter_mem, Iff.mpr
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l

Tactic:
exact (countable_bInter_mem hSc).2 hS

Premises used: countable_bInter_mem, Iff.mpr
-- 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₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
⟨fun S hSc hS => ?_⟩

Premises used: CountableInterFilter.mk
-- 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₂
refine : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂), ⋂₀ S ∈ l₁ ⊓ l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
refine ⟨fun S hSc hS => ?_⟩
-- 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₂
choose :
  ∀ (s : (s : Set α) → s ∈ S → Set α) (hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁)
    (t : (s : Set α) → s ∈ S → Set α) (ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂)
    (hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a), ⋂₀ S ∈ l₁ ⊓ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂

Tactic:
choose s hs t ht hst using hS
-- 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
s : (s : Set α) → s ∈ S → Set α
hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
⊢ ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁

Tactic:
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
-- 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
s t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
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₁
⊢ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂

Tactic:
replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
-- 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
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₂

Tactic:
mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)

Premises used: Filter.inter_mem_inf, Set.subset_sInter, Filter.mem_of_superset
-- 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
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₂
refine : ∀ (i : Set α) (hi : i ∈ S), (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i
⊢ ⋂₀ S ∈ l₁ ⊓ l₂

Tactic:
refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)

Premises used: Filter.inter_mem_inf, Set.subset_sInter, Filter.mem_of_superset
-- 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
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
rw : (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i

Tactic:
rw [hst i hi]
-- 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
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
h₂ : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ t i hi
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi

Tactic:
apply inter_subset_inter

Premises used: Set.inter_subset_inter
-- 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
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 ⊆ s i hi

Tactic:
iInter_subset_of_subset i (iInter_subset _ _)

Premises used: Set.iInter_subset_of_subset, Set.iInter_subset
-- 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
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 ⊆ s i hi

Tactic:
exact iInter_subset_of_subset i (iInter_subset _ _)

Premises used: Set.iInter_subset_of_subset
-- 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
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), t i h ⊆ t i hi

Tactic:
iInter_subset_of_subset i (iInter_subset _ _)

Premises used: Set.iInter_subset_of_subset, Set.iInter_subset
-- 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
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), t i h ⊆ t i hi

Tactic:
exact iInter_subset_of_subset i (iInter_subset _ _)

Premises used: Set.iInter_subset_of_subset
-- 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₂
⊢ CountableInterFilter (l₁ ⊔ l₂)

Tactic:
⟨fun S hSc hS => ⟨?_, ?_⟩⟩

Premises used: And.intro, CountableInterFilter.mk
-- 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₂
refine_1 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₁
refine_2 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₂
⊢ CountableInterFilter (l₁ ⊔ l₂)

Tactic:
refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- 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 ∈ l₁

Tactic:
(countable_sInter_mem hSc).2 fun s hs => ?_

Premises used: Iff.mpr, countable_sInter_mem
-- 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₂
refine_1 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₁
⊢ ⋂₀ S ∈ l₁

Tactic:
refine (countable_sInter_mem hSc).2 fun s hs => ?_

Premises used: Iff.mpr, countable_sInter_mem
-- 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 ∈ l₂

Tactic:
(countable_sInter_mem hSc).2 fun s hs => ?_

Premises used: Iff.mpr, countable_sInter_mem
-- 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₂
refine_2 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₂
⊢ ⋂₀ S ∈ l₂

Tactic:
refine (countable_sInter_mem hSc).2 fun s hs => ?_

Premises used: Iff.mpr, countable_sInter_mem