awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
mp : ∀ {V : Set α} (V_in : V ∈ s), ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V
mp₁ : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ
mp₂ :
  ∀ {s_1 t : Set α},
    GenerateSets s s_1 → ∀ (hVW : s_1 ⊆ t) (hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1), ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mp₃ : ∀ {s_1 t : Set α},
  GenerateSets s s_1 →
    GenerateSets s t →
      ∀ (hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1) (hW : ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t),
        ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ s_1 ∩ t
Tactic: induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s
have mpr : ∀ (t : Set (Set α)) (hts : t ⊆ s) (tfin : t.Finite) (h : ⋂₀ t ⊆ U), U ∈ generate s
Tactic: rcases h with ⟨t, hts, tfin, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
have haveI : ∀ (this : Fintype (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
Tactic: haveI := I_fin.fintype
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
this : Fintype (↑I : Type u_2)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
have refine : ∀ (i : (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (V i)
Tactic: refine mem_of_superset (iInter_mem.2 fun i => ?_) hU
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have mp : Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U →
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have mpr : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
  Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have mp : (∃ t ⊆ ⋃ (i : ι), (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) →
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
Tactic: rw [iInf_eq_generate, mem_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ (i : ι), (s i).sets
tfin : t.Finite
tinter : ⋂₀ t ⊆ U
⊢ ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have mp : ∀ (I : Set ι) (Ifin : I.Finite) (σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α))
  (σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite)
  (σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets)
  (tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets))
  (tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i))
  (tinter : ⋂₀ ⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ U),
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
Tactic: rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩
Cleared hypotheses: t, tsub, tfin, tinter
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂₀ ⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ U
⊢ ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have tinter₁ : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
Tactic: rw [sInter_iUnion] at tinter
Cleared hypotheses: tinter
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
⊢ ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have hV : let V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i;
V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
Tactic: set V := fun i => U ∪ ⋂₀ σ i with hV
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
⊢ ⋂₀ σ i ∈ s (↑i : ι)
have rw : ∀ U ∈ σ i, U ∈ s (↑i : ι)
Tactic: rw [sInter_mem (σfin _)]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
⊢ V i ∈ s (↑i : ι)
have this : ⋂₀ σ i ∈ s (↑i : ι)
Tactic: have : ⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
⊢ ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
Tactic: have V_in : ∀ (i : I), V i ∈ s i := by
      rintro i
      have : ⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
      exact mem_of_superset this subset_union_right
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
⊢ ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
have mp : U = ⋂ (i : (↑I : Type u_2)), V i
Tactic: refine ⟨I, Ifin, V, V_in, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
mp : U = ⋂ (i : (↑I : Type u_2)), (fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i) i
⊢ U = ⋂ (i : (↑I : Type u_2)), V i
have mp₁ : U = U ∪ ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i
Tactic: rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
mp : U = ⋂ (i : (↑I : Type u_2)), (fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i) i
mp₁ : U = U ∪ ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i
⊢ U = ⋂ (i : (↑I : Type u_2)), V i
have mp₂ : U = U
Tactic: rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
mp : U = ⋂ (i : (↑I : Type u_2)), (fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i) i
mp₁ : U = U ∪ ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i
mp₂ : U = U
⊢ U = ⋂ (i : (↑I : Type u_2)), V i
have mp₃ : ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i ⊆ U
Tactic: rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have simp : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set α),
        (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
Tactic: simp only [mem_iInf, biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
have refine : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set α),
        (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
Tactic: refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (V_1 : ι → Set α),
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ i ∉ I_1, V_1 i = univ) ∧
            Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
have refine_1 : ∀ (i : ι), (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
Tactic: refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
refine_1 :
  ∀ (i : ι),
    (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (V_1 : ι → Set α),
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ i ∉ I_1, V_1 i = univ) ∧
            Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
have refine_2 : ∀ (i : ι) (hi : i ∉ I),
  Eq.{u + 1} (α := Set α)
    ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
Tactic: refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
refine_1 :
  ∀ (i : ι),
    (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
refine_2 :
  ∀ (i : ι) (hi : i ∉ I),
    Eq.{u + 1} (α := Set α)
      ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (V_1 : ι → Set α),
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ i ∉ I_1, V_1 i = univ) ∧
            Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
have refine_3 : Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
    (⋂ (x : (↑I : Type u_2)),
      (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) (↑x : ι)) ∧
  Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
    (⋂ (i : ι), (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i)
Tactic: refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
⊢ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ) ∈ s i
have pos : ∀ (h : i ∈ I), V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) ∈ s i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
pos : ∀ (h : i ∈ I), V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) ∈ s i
⊢ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ) ∈ s i
have neg : i ∉ I → univ ∈ s i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have simp : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set α),
        (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have simp₁ : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
  ∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set α),
        (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]