-- Mathlib/Order/Filter/CardinalInter.lean
theorem mem_cardinaleGenerate_iff {s : Set α} {hreg : c.IsRegular} :
    s ∈ cardinalGenerate g (IsRegular.nat_lt hreg 2) ↔
    ∃ S : Set (Set α), S ⊆ g ∧ (#S < c) ∧ ⋂₀ S ⊆ s

Proof state:
case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1 ⊆ g, #↑S_1 < 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, ?_⟩

Result:
case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ ⋂₀ S

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Proof state:
case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1 ⊆ g, #↑S_1 < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih

Result:
case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1 ⊆ g, #↑S_1 < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Proof state:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
rcases h with ⟨S, Sg, Sct, hS⟩

Result:
case mpr.intro.intro.intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Proof state:
case mp.superset
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s✝ t✝ : Set α
a✝¹ : CardinalGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s✝
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ t✝

Tactic:
exact Exists.imp (by tauto) ih

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
this : CardinalInterFilter (cardinalGenerate g ⋯) c
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
exact mem_of_superset ((cardinal_sInter_mem Sct).mpr
  (fun s H => CardinalGenerateSets.basic (Sg H))) hS

Result:
no goals

Proof state:
case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

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

Result:
case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ #↑{s} < c ∧ ⋂₀ {s} ⊆ s

Proof state:
case mp.univ
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ Set.univ

Tactic:
exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s✝ t✝ : Set α
a✝¹ : CardinalGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s✝
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #↑a < c ∧ ⋂₀ a ⊆ s✝ → a ⊆ g ∧ #↑a < c ∧ ⋂₀ a ⊆ t✝

Tactic:
tauto

Result:
no goals

Proof state:
case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ ⋂₀ S

Tactic:
apply subset_sInter

Result:
case mp.sInter.h
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ t' ∈ S, ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ t'

Proof state:
case mpr.intro.intro.intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c :=
  cardinalInter_ofCardinalGenerate _ _

Result:
case mpr.intro.intro.intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
this : CardinalInterFilter (cardinalGenerate g ⋯) c
⊢ s ∈ cardinalGenerate g ⋯

Proof state:
case mp.sInter.h
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ t' ∈ S, ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ t'

Tactic:
apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Result:
no goals

Proof state:
case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ #↑{s} < c ∧ ⋂₀ {s} ⊆ s

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

Result:
no goals

Proof state:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
induction h with
| @basic s hs =>
  refine ⟨{s}, singleton_subset_iff.mpr hs, ?_⟩
  simpa [subset_refl] using IsRegular.nat_lt hreg 1
| univ =>
  exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩
| superset _ _ ih => exact Exists.imp (by tauto) ih
| @sInter S Sct _ ih =>
  choose T Tg Tct hT using ih
  refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa,
    (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
  apply subset_sInter
  apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ ⋂₀ ∅ ⊆ Set.univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets 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) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
simpa

Result:
no goals