awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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) ∩ ⋂ (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.CardinalInter (goal)
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
⊢ (⋂ (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.CardinalInter (hypothesis)
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₁ ⊓ l₂) (min c₁ c₂)
have this : CardinalInterFilter l₁ (min c₁ c₂)
Tactic: have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
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₁ ⊓ l₂) (min c₁ c₂)
have this₁ : CardinalInterFilter l₂ (min c₁ c₂)
Tactic: have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
have refine_1 : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₁
Tactic: refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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₁
⊢ CardinalInterFilter (l₁ ⊔ l₂) c
have refine_2 : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂), ⋂₀ S ∈ l₂
Tactic: refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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₁
have refine_1 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₁
Tactic: refine (cardinal_sInter_mem hSc).2 fun s hs => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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₂
have refine_2 : ∀ (s : Set α) (hs : s ∈ S), s ∈ l₂
Tactic: refine (cardinal_sInter_mem hSc).2 fun s hs => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
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₁ ⊔ l₂) (min c₁ c₂)
have this : CardinalInterFilter l₁ (min c₁ c₂)
Tactic: have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
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₁ ⊔ l₂) (min c₁ c₂)
have this₁ : CardinalInterFilter l₂ (min c₁ c₂)
Tactic: have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mp : s ∈ cardinalGenerate g sorry → ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mpr : (∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s) → s ∈ cardinalGenerate g sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
have mp : #(↑{s} : Type u) < c ∧ ⋂₀ {s} ⊆ s
Tactic: refine ⟨{s}, singleton_subset_iff.mpr hs, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∀ (a : Set (Set α)), a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ s_1 → a ⊆ g ∧ #(↑a : Type u) < c ∧ ⋂₀ a ⊆ t
have 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
Tactic: tauto
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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
⊢ ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ 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) : Type u) < c) (hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s),
  ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S
Tactic: choose T Tg Tct hT using ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ 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,
        (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
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 ⊆ ⋂₀ 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.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, #(↑S : Type u) < 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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mp₁ : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ Set.univ
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
mp₁ : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ Set.univ
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mp₂ : ∀ {s t : Set α},
  CardinalGenerateSets (c := c) g s →
    s ⊆ t → ∀ (ih : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ t
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
mp : ∀ {s : Set α} (hs : s ∈ g), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
mp₁ : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ Set.univ
mp₂ :
  ∀ {s t : Set α},
    CardinalGenerateSets (c := c) g s →
      s ⊆ t → ∀ (ih : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s), ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ t
⊢ ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
have mp₃ : ∀ {S : Set (Set α)} (Sct : #(↑S : Type u) < c),
  (∀ s ∈ S, CardinalGenerateSets (c := c) g s) →
    ∀ (ih : ∀ s ∈ S, ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s), ∃ S_1 ⊆ g, #(↑S_1 : Type u) < c ∧ ⋂₀ S_1 ⊆ ⋂₀ 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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : ∃ S ⊆ g, #(↑S : Type u) < c ∧ ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯
have mpr : ∀ (S : Set (Set α)) (Sg : S ⊆ g) (Sct : #(↑S : Type u) < c) (hS : ⋂₀ S ⊆ s), s ∈ cardinalGenerate g sorry
Tactic: rcases h with ⟨S, Sg, Sct, hS⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #(↑S : Type u) < c
hS : ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯
have this : CardinalInterFilter (cardinalGenerate g sorry) c
Tactic: have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c :=
    cardinalInter_ofCardinalGenerate _ _
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets
have mp : f ≤ cardinalGenerate g hc → g ⊆ f.sets
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
mp : f ≤ cardinalGenerate g hc → g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets
have mpr : g ⊆ f.sets → f ≤ cardinalGenerate g hc
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
⊢ 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 (cardinal_sInter_mem Sct).mpr ih
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
mpr : ∀ {s : Set α} (hs : s ∈ g), s ∈ f
⊢ s ∈ f
have mpr₁ : Set.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 (cardinal_sInter_mem Sct).mpr ih
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
mpr : ∀ {s : Set α} (hs : s ∈ g), s ∈ f
mpr₁ : Set.univ ∈ f
⊢ s ∈ f
have mpr₂ : ∀ {s t : Set α}, CardinalGenerateSets (c := c) 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 (cardinal_sInter_mem Sct).mpr ih
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
mpr : ∀ {s : Set α} (hs : s ∈ g), s ∈ f
mpr₁ : Set.univ ∈ f
mpr₂ : ∀ {s t : Set α}, CardinalGenerateSets (c := c) g s → ∀ (st : s ⊆ t) (ih : s ∈ f), t ∈ f
⊢ s ∈ f
have mpr₃ : ∀ {S : Set (Set α)} (Sct : #(↑S : Type u) < c),
  (∀ s ∈ S, CardinalGenerateSets (c := c) 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 (cardinal_sInter_mem Sct).mpr ih
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ IsGreatest {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)
have refine : Membership.mem (γ := Set (Filter α)) (upperBounds {f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets})
  (cardinalGenerate g hc)
Tactic: refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
⊢ Filter α
have hUnion : ∀ (S : Set (Set α)),
  #(↑S : Type u) < c →
    (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
      Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)
Tactic: apply ofCardinalUnion {s | Cardinal.mk s < c} (natCast_lt_aleph0.trans_le hreg.aleph0_le)