awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
s : Set α
inst_2 : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ (a : α), {a} ∈ l

Tactic:
(exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦
      And.right

Premises used: Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating, Exists.imp, And.right
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
s : Set α
inst_2 : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ (a : α), {a} ∈ l

Tactic:
exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦
      And.right

Premises used: Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating, Exists.imp, And.right
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
inst_1 : HasCountableSeparatingOn α p univ
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ (s : Set α), s.Subsingleton ∧ s ∈ l

Tactic:
let ⟨t, _, hts, htl⟩ := exists_subset_subsingleton_mem_of_forall_separating p univ_mem hl
  ⟨t, hts, htl⟩

Premises used: Membership.mem, Exists, And, _private.0.Filter.exists_subsingleton_mem_of_forall_separating.match_1, And.intro, Set.Subsingleton, Exists.intro, Filter.univ_mem, Filter.exists_subset_subsingleton_mem_of_forall_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
inst_2 : HasCountableSeparatingOn α p univ
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ (x : α), {x} ∈ l

Tactic:
exists_singleton_mem_of_mem_of_forall_separating p univ_mem hl

Premises used: Filter.exists_singleton_mem_of_mem_of_forall_separating, Filter.univ_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f : α → β
p : Set β → Prop
s : Set β
inst_1 : HasCountableSeparatingOn β p s
hs : ∀ᶠ (x : α) in l, f x ∈ s
hne : s.Nonempty
h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U
⊢ ∃ a ∈ s, f =ᶠ[l] const α a

Tactic:
exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p (l := map f l) hs hne h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating, Filter.EventuallyEq, Set.preimage, Set.singleton
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f : α → β
inst_1 : Nonempty β
p : Set β → Prop
s : Set β
inst_2 : HasCountableSeparatingOn β p s
hs : ∀ᶠ (x : α) in l, f x ∈ s
h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U
⊢ ∃ (a : β), f =ᶠ[l] const α a

Tactic:
exists_singleton_mem_of_mem_of_forall_separating (l := map f l) p hs h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.preimage, Set.singleton, Filter.exists_singleton_mem_of_mem_of_forall_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f : α → β
inst_1 : Nonempty β
p : Set β → Prop
inst_2 : HasCountableSeparatingOn β p univ
h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U
⊢ ∃ (a : β), f =ᶠ[l] const α a

Tactic:
exists_singleton_mem_of_forall_separating (l := map f l) p h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.preimage, Filter.exists_singleton_mem_of_forall_separating, Set.singleton
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
rcases :
  ∀ (S : Set (Set β)) (hSc : S.Countable) (hSp : ∀ s ∈ S, p s)
    (hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y), f =ᶠ[l] g
⊢ f =ᶠ[l] g

Tactic:
rcases h'.1 with ⟨S, hSc, hSp, hS⟩

Premises used: HasCountableSeparatingOn.exists_countable_separating
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s

Tactic:
have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s :=
    (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
x : α
hx : ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
hxf : f x ∈ s
hxg : g x ∈ s
⊢ f x = g x

Tactic:
hS _ hxf _ hxg hx
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ s ∈ S, f x ∈ s ↔ g x ∈ s) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ∈ s) x} x →
                      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = g x) x} x}
                  x}
            x}
      a
h₂ h₃ : ∀ (x : α) (hx : ∀ s ∈ S, f x ∈ s ↔ g x ∈ s) (hxf : f x ∈ s) (hxg : g x ∈ s), f x = g x
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
inst_1 : HasCountableSeparatingOn β p univ
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
⊢ f =ᶠ[l] g

Tactic:
of_eventually_mem_of_forall_separating_mem_iff p (s := univ) univ_mem univ_mem h

Premises used: Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff, Filter.univ_mem
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
inst_1 : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U
⊢ f =ᶠ[l] g

Tactic:
of_eventually_mem_of_forall_separating_mem_iff p hf hg fun U hU ↦ (h U hU).mem_iff

Premises used: Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff, Filter.EventuallyEq.mem_iff
-- Module: Mathlib.Order.Filter.CountableSeparatingOn
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
inst_1 : HasCountableSeparatingOn β p univ
h : ∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U
⊢ f =ᶠ[l] g

Tactic:
of_eventually_mem_of_forall_separating_preimage p (s := univ) univ_mem univ_mem h

Premises used: Filter.EventuallyEq.of_eventually_mem_of_forall_separating_preimage, Filter.univ_mem
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
f : Filter α
p : ι → Prop
s : ι → Set α
h : f.HasCountableBasis p s
⊢ f.IsCountablyGenerated

Tactic:
⟨⟨{ t | ∃ i, p i ∧ s i = t }, h.countable.image s, h.toHasBasis.eq_generate⟩⟩

Premises used: Filter.HasBasis.eq_generate, Filter.HasCountableBasis.countable, setOf, Filter.IsCountablyGenerated.mk, Exists, Set.Countable.image, And, And.intro, Exists.intro, Eq, Filter.HasCountableBasis.toHasBasis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : Countable ι
f : Filter α
p : ι → Prop
s : ι → Set α
h : f.HasBasis p s
⊢ f.IsCountablyGenerated

Tactic:
HasCountableBasis.isCountablyGenerated ⟨h, to_countable _⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasCountableBasis.isCountablyGenerated, Set.to_countable
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
h :
  (Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m) ∧
    Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i))
      (⨅ (i : ℕ), 𝓟 ((fun (n : ℕ) ↦ (⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m : Set α)) i))
⊢ ∃ (t : ℕ → Set α), Antitone t ∧ Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (t i))

Tactic:
use fun n => ⋂ m ≤ n, s m

Premises used: Set.iInter
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
h : Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m
h₁ : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
⊢ (Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m) ∧
    Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i))
      (⨅ (i : ℕ), 𝓟 ((fun (n : ℕ) ↦ (⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m : Set α)) i))

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
⊢ Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m

Tactic:
fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl

Premises used: Iff.mpr, Set.biInter_mono, Set.Mem, Set.Iic_subset_Iic, Antitone, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
⊢ Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m

Tactic:
exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl

Premises used: Iff.mpr, Set.biInter_mono, Set.Iic_subset_Iic, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
h : LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
h₁ : LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)) (⨅ (i : ℕ), 𝓟 (s i))
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
h : ∀ (i : ℕ), LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))

Tactic:
rw [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
h : ∀ (i : ℕ), ⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)) (⨅ (i : ℕ), 𝓟 (s i))

Tactic:
rw [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
h : Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))

Tactic:
rw [le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)

Tactic:
(biInter_mem (finite_le_nat _)).2 fun j _ => ?_

Premises used: Iff.mpr, Set.Mem, setOf, Filter.biInter_mem, Set.finite_le_nat
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
h :
  ∀ (j : ℕ),
    Membership.mem (γ := Set ℕ) {i_1 : ℕ | i_1 ≤ i} j → Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (s j)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)

Tactic:
refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_

Premises used: Iff.mpr, Filter.biInter_mem, Set.finite_le_nat
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i j : ℕ
h : Membership.mem (γ := Set ℕ) {i_1 : ℕ | i_1 ≤ i} j
⊢ Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (s j)

Tactic:
mem_iInf_of_mem j (mem_principal_self _)

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i j : ℕ
h : Membership.mem (γ := Set ℕ) {i_1 : ℕ | i_1 ≤ i} j
⊢ Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (s j)

Tactic:
exact mem_iInf_of_mem j (mem_principal_self _)

Premises used: Filter.mem_iInf_of_mem
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, Set.iInter₂_subset, iInf_le_of_le
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
h : i ≤ i
⊢ ⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)

Premises used: iInf_le_of_le
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
Bne : B.Nonempty
f : ι → α
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))

Tactic:
let ⟨g, hg⟩ := Bcbl.exists_eq_range Bne
  ⟨g, hg.symm ▸ iInf_range⟩

Premises used: iInf, _private.0.Filter.countable_biInf_eq_iInf_seq.match_1, iInf_range, Exists, Eq.rec, Exists.intro, Set.Countable.exists_eq_range, Eq.symm, Eq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
inl : ∀ (hB : B = ∅), ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
inr : ∀ (Bnonempty : B.Nonempty), ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))

Tactic:
rcases B.eq_empty_or_nonempty with hB | Bnonempty

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
inl : ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f (x i))
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))

Tactic:
rw [hB, iInf_emptyset]

Premises used: iInf_emptyset
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
h₁ : Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f ((fun (x : ℕ) ↦ i₀) i))
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f (x i))

Tactic:
use fun _ => i₀
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f ((fun (x : ℕ) ↦ i₀) i))

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))

Tactic:
countable_biInf_eq_iInf_seq Bcbl Bnonempty f

Premises used: Filter.countable_biInf_eq_iInf_seq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))

Tactic:
exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

Premises used: Filter.countable_biInf_eq_iInf_seq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
B : Set (Set α)
Bcbl : B.Countable
⊢ ∃ (x : ℕ → Set α), Eq.{u_1 + 1} (α := Filter α) (⨅ t ∈ B, 𝓟 t) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
countable_biInf_eq_iInf_seq' Bcbl 𝓟 principal_univ

Premises used: Filter.principal_univ, Filter.countable_biInf_eq_iInf_seq', Filter.principal
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder ι
l : Filter α
s : ι → Set α
hs : l.HasAntitoneBasis s
t : Set α
⊢ (∃ (i : ι), True ∧ s i ⊆ t) ↔ ∃ (i : ι), s i ⊆ t

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder ι
l : Filter α
s : ι → Set α
hs : l.HasAntitoneBasis s
i : ι
⊢ s i ∈ l

Tactic:
hs.toHasBasis.mem_of_mem trivial

Premises used: trivial, Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
l : Filter α
s : ι → Set α
hs : l.HasAntitoneBasis s
i : ι
⊢ l.HasBasis (fun (j : ι) ↦ i ≤ j) s

Tactic:
hs.1.to_hasBasis (fun j _ => (exists_ge_ge i j).imp fun _k hk => ⟨hk.1, hs.2 hk.2⟩) fun j _ =>
    ⟨j, trivial, Subset.rfl⟩

Premises used: trivial, Filter.HasAntitoneBasis.toHasBasis, Exists.imp, exists_ge_ge, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasAntitoneBasis.antitone, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
rcases :
  ∀ (s_1 : Set (Set α)) (hsc : s_1.Countable) (hs : (generate s_1).HasBasis p s),
    ∃ (x : ℕ → Set α), generate s_1 = ⨅ (i : ℕ), 𝓟 (x i)
⊢ ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), 𝓟 (x i)

Tactic:
rcases h with ⟨s, hsc, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s_1 : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s_1
rw : ∃ (x : ℕ → Set α), Eq.{u_1 + 1} (α := Filter α) (⨅ s_2 ∈ s, 𝓟 s_2) (⨅ (i : ℕ), 𝓟 (x i))
⊢ ∃ (x : ℕ → Set α), generate s = ⨅ (i : ℕ), 𝓟 (x i)

Tactic:
rw [generate_eq_biInf]

Premises used: Filter.generate_eq_biInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s_1 : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s_1
⊢ ∃ (x : ℕ → Set α), Eq.{u_1 + 1} (α := Filter α) (⨅ s_2 ∈ s, 𝓟 s_2) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
countable_biInf_principal_eq_seq_iInf hsc

Premises used: Filter.countable_biInf_principal_eq_seq_iInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s_1 : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s_1
⊢ ∃ (x : ℕ → Set α), Eq.{u_1 + 1} (α := Filter α) (⨅ s_2 ∈ s, 𝓟 s_2) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
exact countable_biInf_principal_eq_seq_iInf hsc

Premises used: Filter.countable_biInf_principal_eq_seq_iInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
obtain :
  ∀ (x' : ℕ → Set α) (hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)),
    ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)

Tactic:
obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) := by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
⊢ ∀ (i : ℕ), x' i ∈ f

Tactic:
have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
⊢ Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')

Tactic:
have x_anti : Antitone fun i => s (x i).1 :=
    antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans inter_subset_right
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ s (↑(x 0) : ι') ⊆ x' 0

Tactic:
hs.set_index_subset _

Premises used: Filter.HasBasis.set_index_subset
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
i : ℕ
⊢ s (↑(x (i + 1)) : ι') ⊆ x' (i + 1)

Tactic:
(hs.set_index_subset _).trans inter_subset_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Filter.HasBasis.set_index_subset
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ s (↑(x 0) : ι') ⊆ x' 0

Tactic:
exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Filter.HasBasis.set_index_subset