awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ⋂₀ S ∈ comap f l

Tactic:
⟨_, (cardinal_bInter_mem hSc).2 htl, ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, And.intro, Exists.intro, Filter.cardinal_bInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
refine : f ⁻¹' ⋂ i ∈ S, t i ⊆ ⋂₀ S
⊢ ⋂₀ S ∈ comap f l

Tactic:
refine ⟨_, (cardinal_bInter_mem hSc).2 htl, ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ f ⁻¹' ⋂ i ∈ S, t i ⊆ ⋂₀ S

Tactic:
simpa [preimage_iInter] using iInter₂_mono ht

Premises used: Set.iInter₂_mono, Set.preimage_iInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (map f l) c

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

Premises used: CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
refine : ∀ (S : Set (Set β)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ map f l), ⋂₀ S ∈ map f l
⊢ CardinalInterFilter (map f l) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set β)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set β)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l

Tactic:
(cardinal_bInter_mem hSc).2 hS

Premises used: Iff.mpr, Filter.cardinal_bInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set β)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l

Tactic:
exact (cardinal_bInter_mem hSc).2 hS

Premises used: Iff.mpr, Filter.cardinal_bInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
⊢ CardinalInterFilter (l₁ ⊓ l₂) c

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

Premises used: CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
refine : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂), ⋂₀ S ∈ l₁ ⊓ l₂
⊢ CardinalInterFilter (l₁ ⊓ l₂) c

Tactic:
refine ⟨fun S hSc hS => ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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₁ := (cardinal_bInter_mem hSc).2 hs
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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₂ := (cardinal_bInter_mem hSc).2 ht
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
⊢ CardinalInterFilter l₁ (min c₁ c₂)

Tactic:
have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
this : CardinalInterFilter l₁ (min c₁ c₂)
⊢ CardinalInterFilter l₂ (min c₁ c₂)

Tactic:
have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
this_1 : CardinalInterFilter l₁ (min c₁ c₂)
this : CardinalInterFilter l₂ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)

Tactic:
cardinalInterFilter_inf_eq _ _

Premises used: Filter.cardinalInterFilter_inf_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
this_1 : CardinalInterFilter l₁ (min c₁ c₂)
this : CardinalInterFilter l₂ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)

Tactic:
exact cardinalInterFilter_inf_eq _ _

Premises used: Filter.cardinalInterFilter_inf_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
⊢ CardinalInterFilter (l₁ ⊔ l₂) c

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

Premises used: And.intro, CardinalInterFilter.mk
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
refine_1 : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₁
refine_2 : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₂
⊢ CardinalInterFilter (l₁ ⊔ l₂) c

Tactic:
refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₁

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

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
refine_1 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₁
⊢ ⋂₀ S ∈ l₁

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

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₂

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

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
refine_2 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₂
⊢ ⋂₀ S ∈ l₂

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

Premises used: Iff.mpr, cardinal_sInter_mem
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
this_1 : CardinalInterFilter l₁ (min c₁ c₂)
this : CardinalInterFilter l₂ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)

Tactic:
cardinalInterFilter_sup_eq _ _

Premises used: Filter.cardinalInterFilter_sup_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst_1 : CardinalInterFilter l₁ c₁
inst_2 : CardinalInterFilter l₂ c₂
this_1 : CardinalInterFilter l₁ (min c₁ c₂)
this : CardinalInterFilter l₂ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)

Tactic:
exact cardinalInterFilter_sup_eq _ _

Premises used: Filter.cardinalInterFilter_sup_eq
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (ofCardinalInter (CardinalGenerateSets (c := c) g) hc ⋯ ⋯) c

Tactic:
apply cardinalInter_ofCardinalInter _ _ _

Premises used: Filter.cardinalInter_ofCardinalInter
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
mp : s ∈ cardinalGenerate g ⋯ → ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
mpr : (∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s) → s ∈ cardinalGenerate g ⋯
⊢ s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s_1 : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s

Tactic:
⟨{s}, singleton_subset_iff.mpr hs, ?_⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s_1 : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
mp : #(↑{s} : Type u) < c ∧ ⋂₀ {s} ⊆ s
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s

Tactic:
refine ⟨{s}, singleton_subset_iff.mpr hs, ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s_1 : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ #(↑{s} : Type u) < c ∧ ⋂₀ {s} ⊆ s

Tactic:
simpa [subset_refl] using IsRegular.nat_lt hreg 1

Premises used: subset_refl, Cardinal.IsRegular.nat_lt, OfNat.ofNat
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ Subset.{u} (α := Set α) (⋂₀ ∅) Set.univ

Tactic:
simp
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ Set.univ

Tactic:
exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s_1 t : Set α
h : CardinalGenerateSets (c := c) g s_1
h_1 : s_1 ⊆ t
ih : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s_1
tauto tauto₁ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
left : ∀ (a w : Set (Set α)), w ⊆ g → #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g
right :
  ∀ (a w : Set (Set α)),
    w ⊆ g → #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → #(↑a : Type u) < c
right₁ :
  ∀ (a w : Set (Set α)), w ⊆ g → #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → ⋂₀ a ⊆ t
left₁ left₂ left₃ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : Set α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ a → a_1 ∈ g
right₂ right₃ right₄ :
  ∀ (a w : Set (Set α)),
    w ⊆ g → #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → #(↑a : Type u) < c
right₅ right₆ right₇ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ ⋂₀ a → a_1 ∈ t
left₄ left₅ left₆ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : Set α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ a → a_1 ∈ g
right₈ right₉ right₁₀ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ ⋂₀ a → a_1 ∈ t
left₇ left₈ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : Set α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ a → a_1 ∈ g
right₁₁ right₁₂ :
  ∀ (a w : Set (Set α)),
    w ⊆ g →
      #(↑w : Type u) < c → ⋂₀ w ⊆ s_1 → ∀ ⦃a_1 : α⦄, a ⊆ g → #(↑a : Type u) < c → ⋂₀ a ⊆ s_1 → a_1 ∈ ⋂₀ a → a_1 ∈ t
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t

Tactic:
tauto
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s_1 t : Set α
h : CardinalGenerateSets (c := c) g s_1
h_1 : s_1 ⊆ t
ih : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s_1
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ t

Tactic:
exact Exists.imp (by tauto) ih

Premises used: Exists.imp
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #(↑S : Type u) < c
h : ∀ s ∈ S, CardinalGenerateSets (c := c) g s
ih : ∀ s ∈ S, ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ 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) : Type u) < c) (hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s),
    ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S
⊢ ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #(↑S : Type u) < c
h : ∀ s ∈ S, CardinalGenerateSets (c := c) 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) : Type u) < c
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.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #(↑S : Type u) < c
h : ∀ s ∈ S, CardinalGenerateSets (c := c) 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) : Type u) < c
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 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa,
        (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #(↑S : Type u) < c
h : ∀ s ∈ S, CardinalGenerateSets (c := c) 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) : Type u) < c
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