awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (hypothesis)
Goal:
α : Type u_1
B : FilterBasis α
⊢ B.filter = ⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)
have this : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)
Tactic: have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) := by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
this : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)
⊢ B.filter = ⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)
have h : ∀ (U : Set α), U ∈ B.filter ↔ Membership.mem (γ := Filter α) (⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)) U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
⊢ generate B.sets = B.filter
have a : generate B.sets ≤ B.filter
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
a : generate B.sets ≤ B.filter
⊢ generate B.sets = B.filter
have a₁ : B.filter ≤ generate B.sets
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets
have a : ∀ (V : Set α) (V_in : V ∈ B) (h : V ⊆ U), U ∈ generate B.sets
Tactic: rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
⊢ B.filter ≤ generate B.sets
have a : B.sets ⊆ B.filter.sets
Tactic: rw [le_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filter (p := p) (s := s) = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
have rw : h.filterBasis (p := p) (s := s).filter = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
Tactic: rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
rw : h.filterBasis (p := p) (s := s).filter = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
⊢ h.filter (p := p) (s := s) = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
have rw₁ : generate h.filterBasis (p := p) (s := s).sets = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
Tactic: rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
rw : h.filterBasis (p := p) (s := s).filter = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
rw₁ : generate h.filterBasis (p := p) (s := s).sets = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
⊢ h.filter (p := p) (s := s) = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
have rw₂ : generate { sets := {t : Set α | ∃ (i : ι), p i ∧ s i = t}, nonempty := sorry, inter_sets := sorry : FilterBasis α }.sets =
  generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
Tactic: rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
⊢ l = l'
have h : ∀ (t : Set α), t ∈ l ↔ t ∈ l'
Tactic: ext t
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'
have h : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ t ∈ l'
Tactic: rw [hl.mem_iff, hl'.mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
h : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ t ∈ l'
⊢ t ∈ l ↔ t ∈ l'
have h₁ : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ ∃ (i : ι), p i ∧ s i ⊆ t
Tactic: rw [hl.mem_iff, hl'.mem_iff]
-- 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
⊢ ⋯.filter (p := p) (s := s) = l
have h₁ : ∀ (U : Set α), U ∈ sorry.filter (p := p) (s := s) ↔ U ∈ l
Tactic: ext U
-- 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
⊢ l = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
have rw : l = sorry.filter (p := p) (s := s)
Tactic: rw [← h.isBasis.filter_eq_generate, h.filter_eq]
-- 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
rw : l = ⋯.filter (p := p) (s := s)
⊢ l = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
have rw₁ : l = l
Tactic: rw [← h.isBasis.filter_eq_generate, h.filter_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
⊢ l.HasBasis p' s'
have refine : ∀ (t : Set α) (ht : t ∈ l), ∃ (i : ι'), p' i ∧ s' i ⊆ t
Tactic: refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t
have rcases : ∀ (i : ι) (hi : p i) (ht : s i ⊆ t), ∃ (i : ι'), p' i ∧ s' i ⊆ t
Tactic: rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht_1 : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t
have rcases : ∀ (i' : ι') (hi' : p' i') (hs's : s' i' ⊆ s i), ∃ (i : ι'), p' i ∧ s' i ⊆ t
Tactic: rcases h i hi with ⟨i', hi', hs's⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ t ∈ l ↔ ∃ (i : ι), p' i ∧ s' i ⊆ t
have simp : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ ∃ (i : ι), p i ∧ s' i ⊆ t
Tactic: simp only [hl.mem_iff, ← hp]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
have simp : (¬∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
Tactic: simp only [Filter.Frequently, hl.eventually_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (¬∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
have push : (∀ (i : ι) (_ : p i), ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ l.HasBasis (fun (s : Set α) ↦ s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
have simp : (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
Tactic: simp only [hasBasis_iff, id, and_assoc]
-- 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
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun (i : ι) ↦ p i ∧ q i) s
have refine : ∀ (t : Set α) (ht : t ∈ l), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
Tactic: refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
-- 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
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
have rcases : ∀ (i : ι) (hpi : p i) (hti : s i ⊆ t), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
Tactic: rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
-- 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
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
have rcases : ∀ (j : ι) (hpj : p j) (hqj : q j) (hji : s j ⊆ s i), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
Tactic: rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
⊢ l = l'
have a : l ≤ l'
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
a : l ≤ l'
⊢ l = l'
have a₁ : l' ≤ l
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' ↔ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
have mp : t ∈ l ⊓ l' → ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
mp : t ∈ l ⊓ l' → ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
⊢ t ∈ l ⊓ l' ↔ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
have mpr : (∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
have mp : (∃ (t₁ : Set α), (∃ (i : ι), p i ∧ s i ⊆ t₁) ∧ ∃ (t₂ : Set α), (∃ (i : ι'), p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
  ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
Tactic: simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (ii' : (i : ι) × ι' i) ↦ p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))
have refine : ∀ (t : Set α),
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
Tactic: refine ⟨fun t => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
have rw : (∃ (i : ι), t ∈ l i) ↔
  ∃ (a : ι) (b : ι' a),
    p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
        ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ∧
      s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
        t
Tactic: rw [mem_iInf_of_directed h, Sigma.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
⊢ HasBasis (α := α) (⨅ (i : ι), l i) (fun (ii' : ι × ι') ↦ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦ s ii'.1 ii'.2
have refine : ∀ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔ ∃ (i : ι × ι'), p i.1 i.2 ∧ s i.1 i.2 ⊆ t
Tactic: refine ⟨fun t => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔ ∃ (i : ι × ι'), p i.1 i.2 ∧ s i.1 i.2 ⊆ t
have rw : (∃ (i : ι), t ∈ l i) ↔ ∃ (a : ι) (b : ι'), p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t
Tactic: rw [mem_iInf_of_directed h, Prod.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i)
    (fun (ii' : (i : ι) × ι' i) ↦
      ii'.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
        p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))
have refine : ∀ (t : Set α),
  Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      (i.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧ p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i))) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
Tactic: refine ⟨fun t => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      (i.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧ p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i))) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
have rw : (∃ i ∈ dom, t ∈ l i) ↔
  ∃ (a : ι) (b : ι' a),
    ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
        p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i))) ∧
      s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
        t
Tactic: rw [mem_biInf_of_directed h hdom, Sigma.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i) (fun (ii' : ι × ι') ↦ ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦
    s ii'.1 ii'.2
have refine : ∀ (t : Set α),
  Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔ ∃ (i : ι × ι'), (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t
Tactic: refine ⟨fun t => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔ ∃ (i : ι × ι'), (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t
have rw : (∃ i ∈ dom, t ∈ l i) ↔ ∃ (a : ι) (b : ι'), ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t
Tactic: rw [mem_biInf_of_directed h hdom, Prod.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊔ l' ↔ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t
have simp_rw : (∃ (x : ι) (x_1 : ι'), (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ (a : ι) (b : ι'), (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
Tactic: simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥
have refine : (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f
Tactic: refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f
have rw : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 sᶜᶜ = ⊥
Tactic: rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
rw : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 sᶜᶜ = ⊥
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f
have rw₁ : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 s = ⊥
Tactic: rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
rw : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 sᶜᶜ = ⊥
rw₁ : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 s = ⊥
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f
have rw₂ : f ⊓ 𝓟 s = ⊥ ↔ f ⊓ 𝓟 s = ⊥
Tactic: rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f
have rw : Disjoint f (𝓟 s) ↔ sᶜ ∈ f
Tactic: rw [disjoint_comm, disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f : Filter α
s : Set α
rw : Disjoint f (𝓟 s) ↔ sᶜ ∈ f
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f
have rw₁ : sᶜ ∈ f ↔ sᶜ ∈ f
Tactic: rw [disjoint_comm, disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
have rw : Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ
Tactic: rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
s t : Set α
rw : Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
have rw₁ : sᶜ ∈ 𝓟 t ↔ t ⊆ sᶜ
Tactic: rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
s t : Set α
rw : Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ
rw₁ : sᶜ ∈ 𝓟 t ↔ t ⊆ sᶜ
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
have rw₂ : t ⊆ sᶜ ↔ t ⊆ sᶜ
Tactic: rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
have simp : (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
  ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ (x : α), p x ∧ x ∈ U
Tactic: simp only [inf_neBot_iff, frequently_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
have rw : (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
Tactic: rw [inf_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) ↦ x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ S, 𝓟 (s i)) t ↔ ∃ i ∈ S, s i ⊆ t
have refine : DirectedOn ((fun (i : β) ↦ 𝓟 (s i)) ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) S
Tactic: refine mem_biInf_of_directed ?_ ne
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) ↦ x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ DirectedOn ((fun (i : β) ↦ 𝓟 (s i)) ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) S
have rw : ∀ (h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S)))
  (ne : S.Nonempty) (t : Set α),
  Directed.{u_1, u_2 + 1} (ι := { x : β // x ∈ S }) (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (i : β) ↦ 𝓟 (s i)) ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
Tactic: rw [directedOn_iff_directed, ← directed_comp] at h ⊢
Cleared hypotheses: h, ne, t
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
ne : S.Nonempty
t : Set α
⊢ Directed.{u_1, u_2 + 1} (ι := { x : β // x ∈ S }) (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (i : β) ↦ 𝓟 (s i)) ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
have refine : ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y
Tactic: refine h.mono_comp _ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.comap f l ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t
have simp : (∃ (i : ι), p i ∧ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t
Tactic: simp only [mem_comap', hl.mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ (∃ (i : ι), p i ∧ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t
have refine : ∀ (i : ι), s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t
Tactic: refine exists_congr (fun i => Iff.rfl.and ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ x ∈ f ⁻¹' s i
have rwa : f x ∈ s i
Tactic: rwa [mem_preimage, hx]