awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ι') ⊆ x' i

Tactic:
have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
    rintro (_ | i)
    exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]
-- 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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)

Tactic:
⟨fun i => (x i).1, fun i => (x i).2, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- 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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
refine : f.HasAntitoneBasis fun (i : ℕ) ↦ s ((fun (i : ℕ) ↦ (↑(x i) : ι')) i)
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)

Tactic:
refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩
-- 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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
⊢ HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')

Tactic:
have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')

Tactic:
this
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
h₁ : f = ⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))
⊢ f.HasAntitoneBasis fun (i : ℕ) ↦ s ((fun (i : ℕ) ↦ (↑(x i) : ι')) i)

Tactic:
convert! this
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
i : ℕ
zero : s (↑(x 0) : ι') ∈ f
succ : ∀ (n : ℕ), s (↑(x (n + 1)) : ι') ∈ f
⊢ s (↑(x i) : ι') ∈ f

Tactic:
cases i
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ s (↑(x 0) : ι') ∈ f

Tactic:
apply hs.set_index_mem

Premises used: Filter.HasBasis.set_index_mem
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
n : ℕ
⊢ s (↑(x (n + 1)) : ι') ∈ f

Tactic:
apply hs.set_index_mem

Premises used: Filter.HasBasis.set_index_mem
-- 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_1 : ∀ (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) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ f = ⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))

Tactic:
exact
    le_antisymm (le_iInf fun i => le_principal_iff.2 <| by cases i <;> apply hs.set_index_mem)
      (hx'.symm ▸
        le_iInf fun i => le_principal_iff.2 <| this.1.mem_iff.2 ⟨i, trivial, x_subset i⟩)

Premises used: Iff.mpr, Filter.le_principal_iff, le_iInf, le_antisymm
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
⊢ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x

Tactic:
let ⟨x, _, hx⟩ := f.basis_sets.exists_antitone_subbasis
  ⟨x, hx⟩

Premises used: Filter.HasBasis.exists_antitone_subbasis, Exists, Filter.basis_sets, Exists.intro, Filter.HasAntitoneBasis, _private.0.Filter.exists_antitone_basis.match_1
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
x : ℕ → Set α
hx : f.HasAntitoneBasis x
⊢ ∀ {s : Set α}, s ∈ f ↔ ∃ (i : ℕ), x i ⊆ s

Tactic:
simp [hx.1.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.HasAntitoneBasis.toHasBasis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
rcases : ∀ (s : ℕ → Set α) (hs : f.HasAntitoneBasis s), (f ⊓ g).IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
rcases : ∀ (t : ℕ → Set α) (ht : g.HasAntitoneBasis t), (f ⊓ g).IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
rcases g.exists_antitone_basis with ⟨t, ht⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
HasCountableBasis.isCountablyGenerated ⟨hs.1.inf ht.1, Set.to_countable _⟩

Premises used: Filter.HasBasis.inf, Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, Filter.HasCountableBasis.isCountablyGenerated, Set.to_countable
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
exact HasCountableBasis.isCountablyGenerated ⟨hs.1.inf ht.1, Set.to_countable _⟩

Premises used: Filter.HasBasis.inf, Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, Filter.HasCountableBasis.isCountablyGenerated, Set.to_countable
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
l : Filter α
inst : l.IsCountablyGenerated
f : α → β
⊢ (map f l).IsCountablyGenerated

Tactic:
let ⟨_x, hxl⟩ := l.exists_antitone_basis
  (hxl.map _).isCountablyGenerated

Premises used: _private.0.Filter.exists_antitone_seq.match_1, Filter.HasAntitoneBasis.toHasBasis, Filter.map, Filter.IsCountablyGenerated, Filter.exists_antitone_basis, Filter.HasAntitoneBasis.map, Filter.HasBasis.isCountablyGenerated
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
l : Filter β
inst : l.IsCountablyGenerated
f : α → β
⊢ (comap f l).IsCountablyGenerated

Tactic:
let ⟨_x, hxl⟩ := l.exists_antitone_basis
  (hxl.comap _).isCountablyGenerated

Premises used: _private.0.Filter.exists_antitone_seq.match_1, Filter.HasAntitoneBasis.toHasBasis, Filter.HasAntitoneBasis.comap, Filter.IsCountablyGenerated, Filter.exists_antitone_basis, Filter.HasBasis.isCountablyGenerated, Filter.comap
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
rcases : ∀ (s : ℕ → Set α) (hs : f.HasAntitoneBasis s), (f ⊔ g).IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
rcases : ∀ (t : ℕ → Set α) (ht : g.HasAntitoneBasis t), (f ⊔ g).IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
rcases g.exists_antitone_basis with ⟨t, ht⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, Filter.HasCountableBasis.isCountablyGenerated, Set.to_countable, Filter.HasBasis.sup
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, Filter.HasCountableBasis.isCountablyGenerated, Set.to_countable, Filter.HasBasis.sup
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
la : Filter α
lb : Filter β
inst : la.IsCountablyGenerated
inst_1 : lb.IsCountablyGenerated
⊢ (la ×ˢ lb).IsCountablyGenerated

Tactic:
Filter.Inf.isCountablyGenerated _ _

Premises used: Filter.Inf.isCountablyGenerated
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
la : Filter α
lb : Filter β
inst : la.IsCountablyGenerated
inst_1 : lb.IsCountablyGenerated
⊢ (la.coprod lb).IsCountablyGenerated

Tactic:
Filter.Sup.isCountablyGenerated _ _

Premises used: Filter.Sup.isCountablyGenerated, Filter.coprod
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
inst : Countable ι'
x : ι' → Set α
right : ⨅ (i : ι'), 𝓟 (x i) = generate (range x)
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ι'), 𝓟 (x i))

Tactic:
use range x, countable_range x

Premises used: Set.countable_range, Set.range
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
ι' : Sort u_5
inst : Countable ι'
x : ι' → Set α
right : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ι'), 𝓟 (x i)) (⨅ s ∈ range x, 𝓟 s)
right₁ right₂ : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ι'), 𝓟 (x i)) (⨅ (i : ι'), 𝓟 (x i))
⊢ ⨅ (i : ι'), 𝓟 (x i) = generate (range x)

Tactic:
rw [generate_eq_biInf, iInf_range]

Premises used: iInf_range, Filter.generate_eq_biInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
h : ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), 𝓟 (x i)
rcases : ∀ (x : ℕ → Set α), IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))
⊢ f.IsCountablyGenerated

Tactic:
rcases h with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
x : ℕ → Set α
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
apply isCountablyGenerated_seq

Premises used: Filter.isCountablyGenerated_seq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
B : Set (Set α)
h : B.Countable
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ s ∈ B, 𝓟 s)

Tactic:
isCountablyGenerated_of_seq (countable_biInf_principal_eq_seq_iInf h)

Premises used: Filter.isCountablyGenerated_of_seq, Filter.countable_biInf_principal_eq_seq_iInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
mp : f.IsCountablyGenerated → ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
mpr : (∃ (x : ℕ → Set α), f.HasAntitoneBasis x) → f.IsCountablyGenerated
⊢ f.IsCountablyGenerated ↔ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x

Tactic:
constructor
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
h : f.IsCountablyGenerated
⊢ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x

Tactic:
f.exists_antitone_basis

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
h : f.IsCountablyGenerated
⊢ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x

Tactic:
exact f.exists_antitone_basis

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
mpr : IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))
⊢ f.IsCountablyGenerated

Tactic:
rw [h.1.eq_iInf]

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.eq_iInf
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
isCountablyGenerated_seq x

Premises used: Filter.isCountablyGenerated_seq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))

Tactic:
exact isCountablyGenerated_seq x

Premises used: Filter.isCountablyGenerated_seq
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
s : Set α
⊢ (𝓟 s).IsCountablyGenerated

Tactic:
isCountablyGenerated_of_seq ⟨fun _ => s, iInf_const.symm⟩

Premises used: Filter.isCountablyGenerated_of_seq, Exists.intro, Eq.symm, iInf_const
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
a : α
rw : IsCountablyGenerated (α := α) (𝓟 {a})
⊢ IsCountablyGenerated (pure a)

Tactic:
rw [← principal_singleton]

Premises used: Filter.principal_singleton
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
a : α
⊢ IsCountablyGenerated (α := α) (𝓟 {a})

Tactic:
isCountablyGenerated_principal _

Premises used: Filter.isCountablyGenerated_principal
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
a : α
⊢ IsCountablyGenerated (α := α) (𝓟 {a})

Tactic:
exact isCountablyGenerated_principal _

Premises used: Filter.isCountablyGenerated_principal
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
⊢ IsCountablyGenerated.{u_1} (α := α) ⊥

Tactic:
@principal_empty α ▸ isCountablyGenerated_principal _

Premises used: Eq.rec, Filter.principal_empty, Filter.isCountablyGenerated_principal
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α : Type u_1
⊢ IsCountablyGenerated.{u_1} (α := α) ⊤

Tactic:
@principal_univ α ▸ isCountablyGenerated_principal _

Premises used: Filter.principal_univ, Eq.rec, Filter.isCountablyGenerated_principal
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
choose :
  ∀ (s : (i : ι) → ℕ → Set α) (hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)),
    IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)

Tactic:
choose s hs using fun i => exists_antitone_basis (f i)

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
rw : IsCountablyGenerated.{u_7} (α := α) (⨅ (x : PLift ι), f x.down)
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)

Tactic:
rw [← PLift.down_surjective.iInf_comp]

Premises used: PLift.down_surjective, Function.Surjective.iInf_comp
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (x : PLift ι), f x.down)

Tactic:
HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasBasis.iInf, Filter.HasAntitoneBasis.toHasBasis, PLift.down, Filter.HasCountableBasis.isCountablyGenerated
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
refine :
  Set.Countable.{u_6} (α := (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ))
    {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
      If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (x : PLift ι), f x.down)

Tactic:
refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasBasis.iInf, Filter.HasAntitoneBasis.toHasBasis, Filter.HasCountableBasis.isCountablyGenerated
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ Set.Countable.{u_6} (α := (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ))
    {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
      If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}

Tactic:
(countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_

Premises used: id, Set.countable_range, SetLike.coe, Sigma.map, Set.Countable.mono