awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
have simp : (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
Tactic: simp only [h.mem_iff, exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t
have simp : (∀ t ∈ lb, ∃ (i : ι), pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t
Tactic: simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ (la ×ˢ lb).HasBasis p fun (i : ι) ↦ sa i ×ˢ sb i
have simp : ∀ (t : Set (α × β)),
  (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
Tactic: simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
have refine_1 : ∀ (t : Set (α × β)),
  (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
Tactic: refine fun t => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
refine_1 :
  ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
⊢ ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
have refine_2 : ∀ (t : Set (α × β)),
  (∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
Tactic: refine fun t => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
⊢ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
have refine_1 : ∀ (k : ι) (hk : p k) (ki : sa k ⊆ sa ⟨i, j⟩.fst) (kj : sb k ⊆ sb ⟨i, j⟩.snd), ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
Tactic: rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk (β := π) a) (comap (g a) l) =
    comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)
have refine : (comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)).HasBasis
  (fun (s : Set (π' (f a))) ↦ s ∈ l) fun (i : Set (π' (f a))) ↦ Sigma.mk (β := π) a '' g a ⁻¹' id i
Tactic: refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ (comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)).HasBasis
    (fun (s : Set (π' (f a))) ↦ s ∈ l) fun (i : Set (π' (f a))) ↦ Sigma.mk (β := π) a '' g a ⁻¹' id i
have h : ∀ (x : Set (π' (f a))),
  Sigma.mk (β := π) a '' g a ⁻¹' id x = Sigma.map (β₁ := π) (β₂ := π') f g ⁻¹' Sigma.mk (β := π') (f a) '' id x
Tactic: convert! ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
s : Set (Set α)
⊢ generate s = generate (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s})
have rw : sorry.filter (p := fun (t : Set (Set α)) ↦ t.Finite ∧ t ⊆ s) (s := fun (t : Set (Set α)) ↦ ⋂₀ t) =
  (FilterBasis.ofSets s).filter
Tactic: rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
s : Set (Set α)
⊢ (FilterBasis.ofSets s).filter = generate s
have rw : generate (FilterBasis.ofSets s).sets = generate s
Tactic: rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
s : Set (Set α)
rw : generate (FilterBasis.ofSets s).sets = generate s
⊢ (FilterBasis.ofSets s).filter = generate s
have rw₁ : generate (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}) = generate s
Tactic: rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
s : Set (Set α)
rw : generate (FilterBasis.ofSets s).sets = generate s
rw₁ : generate (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}) = generate s
⊢ (FilterBasis.ofSets s).filter = generate s
have rw₂ : generate s = generate s
Tactic: rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
have mp : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t →
  ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t →
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
have mpr : (∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) →
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t →
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
have mp : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set α),
        (∀ (i : ι), ∃ (i_1 : ι' i), p i i_1 ∧ s i i_1 ⊆ V i) ∧
          (∀ i ∉ I, V i = univ) ∧ t = ⋂ i ∈ I, V i ∧ t = ⋂ (i : ι), V i) →
  ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
Tactic: simp only [mem_iInf', (hl _).mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
I : Set ι
hI : I.Finite
V : ι → Set α
hV : ∀ (i : ι), ∃ (i_1 : ι' i), p i i_1 ∧ s i i_1 ⊆ V i
⊢ ∃ (i : Set ι × ((i : ι) → ι' i)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
      Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)
have mp : ∀ (u : (i : ι) → ι' i) (hu : ∀ (i : ι), p i (u i) ∧ s i (u i) ⊆ V i),
  ∃ (i : Set ι × ((i : ι) → ι' i)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
      Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)
Tactic: choose u hu using hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
have mpr : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) (⋂ i ∈ (I, f).1, s i ((I, f).2 i))
Tactic: grw [← hsub]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
      If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i))
    fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
      s (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i)
have refine_1 : ∀ (t : Set α) (ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t),
  ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t
Tactic: refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
refine_1 :
  ∀ (t : Set α) (ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t),
    ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
      (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
          ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
        ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
          t
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
      If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i))
    fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
      s (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i)
have refine_2 : ∀ (t : Set α),
  (∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
      (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
          ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
        ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
          t) →
    Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
Tactic: refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
⊢ ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t
have refine_1 : ∀ (I : Set ι) (f : (i : ι) → ι' i) (hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t) (hI : (I, f).1.Finite)
  (hf : ∀ i ∈ (I, f).1, p i ((I, f).2 i)),
  ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t
Tactic: rcases (HasBasis.iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
have refine_2 : Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
  (⋂ (i :
    (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
      Type u_6)),
    s (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))
Tactic: grw [← hsub]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))
have refine_2 : ∀
  (val :
    Fintype
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))
Tactic: cases hI.nonempty_fintype
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
have rcases : ∀ (t : I → Set α) (htl : ∀ (i : I), t i ∈ l i) (hd : Pairwise (Disjoint on t)),
  ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
Tactic: rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd_1 : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
have choose : ∀ (ind : (i : I) → ι i) (hp : ∀ (i : I), p i (ind i)) (ht : ∀ (i : I), s i (ind i) ⊆ t i),
  ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
Tactic: choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
have rcases : ∀ (t : I → Set α) (htl : ∀ (i : I), t i ∈ l i) (hd : S.PairwiseDisjoint t),
  ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
Tactic: rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd_1 : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
have choose : ∀ (ind : (i : I) → ι i) (hp : ∀ (i : I), p i (ind i)) (ht : ∀ (i : I), s i (ind i) ⊆ t i),
  ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
Tactic: choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Finite (goal)
Goal:
α : Type u_1
ι : Type u_6
s : ι → Set α
⊢ HasBasis.{u_1, u_6 + 1} (α := α) (⨅ (i : ι), 𝓟 (s i)) (fun (t : Set ι) ↦ t.Finite) fun (t : Set ι) ↦ ⋂ i ∈ t, s i
have refine : ∀ (U : Set α),
  (∃ (t : Finset ι), Membership.mem (γ := Filter α) (⨅ i ∈ t, 𝓟 (s i)) U) ↔
    ∃ (i : Set ι), i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U
Tactic: refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
have he : ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
Tactic: apply Subsingleton.induction_on hf
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
he : ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
have h₁ : ∀ (x : β),
  ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) {x} i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) {x} i → s i ∈ f
Tactic: apply Subsingleton.induction_on hf
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Subsingleton β
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f
have rw : ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
Tactic: rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Subsingleton β
rw : ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f
have rw₁ : ⋂ i ∈ range s, i ∈ f ↔ ∀ (i : β), s i ∈ f
Tactic: rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]