case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
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
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
let x : ℕ → { i : ι' // p i } := fun n =>
  Nat.recOn n (hs.index _ <| this 0) fun n xn =>
    hs.index _ <| inter_mem (this <| n + 1) (hs.mem_of_mem xn.2)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
have x_mono : Antitone fun i => s (x i).1 :=
  antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans (inter_subset_right _ _)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
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 _ _)]
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ HasAntitoneBasis f fun i => s ((fun i => ↑(x i)) i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ HasAntitoneBasis f fun i => s (x i)
refine' ⟨fun i => (x i).1, fun i => (x i).2, _⟩
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : HasAntitoneBasis (⨅ (i : ℕ), 𝓟 (s ↑(x i))) fun i => s ↑(x i)
⊢ HasAntitoneBasis f fun i => s ((fun i => ↑(x i)) i)
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ HasAntitoneBasis f fun i => s ((fun i => ↑(x i)) i)
have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 :=
  ⟨hasBasis_iInf_principal (directed_of_sup x_mono), x_mono⟩
case h.e'_4
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : HasAntitoneBasis (⨅ (i : ℕ), 𝓟 (s ↑(x i))) fun i => s ↑(x i)
⊢ f = ⨅ (i : ℕ), 𝓟 (s ↑(x i))
case intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : HasAntitoneBasis (⨅ (i : ℕ), 𝓟 (s ↑(x i))) fun i => s ↑(x i)
⊢ HasAntitoneBasis f fun i => s ((fun i => ↑(x i)) i)
convert this
no goals
case h.e'_4
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : HasAntitoneBasis (⨅ (i : ℕ), 𝓟 (s ↑(x i))) fun i => s ↑(x i)
⊢ f = ⨅ (i : ℕ), 𝓟 (s ↑(x i))
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⟩)
case mk.intro.intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : Set.Countable s
hs : HasBasis (generate s) p s✝
⊢ ∃ x, generate s = ⨅ (i : ℕ), 𝓟 (x i)
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
⊢ ∃ x, f = ⨅ (i : ℕ), 𝓟 (x i)
rcases h with ⟨s, hsc, rfl⟩
case mk.intro.intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : Set.Countable s
hs : HasBasis (generate s) p s✝
⊢ ∃ x, (⨅ (s_1 : Set α) (_ : s_1 ∈ s), 𝓟 s_1) = ⨅ (i : ℕ), 𝓟 (x i)
case mk.intro.intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : Set.Countable s
hs : HasBasis (generate s) p s✝
⊢ ∃ x, generate s = ⨅ (i : ℕ), 𝓟 (x i)
rw [generate_eq_biInf]
no goals
case mk.intro.intro
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : Set.Countable s
hs : HasBasis (generate s) p s✝
⊢ ∃ x, (⨅ (s_1 : Set α) (_ : s_1 ∈ s), 𝓟 s_1) = ⨅ (i : ℕ), 𝓟 (x i)
exact countable_biInf_principal_eq_seq_iInf hsc
case zero
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
⊢ s ↑(x Nat.zero) ⊆ x' Nat.zero

case succ
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
i : ℕ
⊢ s ↑(x (Nat.succ i)) ⊆ x' (Nat.succ i)
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
⊢ ∀ (i : ℕ), s ↑(x i) ⊆ x' i
rintro (_ | i)
no goals
case zero
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
⊢ s ↑(x Nat.zero) ⊆ x' Nat.zero

case succ
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
i : ℕ
⊢ s ↑(x (Nat.succ i)) ⊆ x' (Nat.succ i)
exacts [hs.set_index_subset _, (hs.set_index_subset _).trans (inter_subset_left _ _)]
no goals
α : Type u_1
β : Type ?u.96678
γ : Type ?u.96681
ι : Type ?u.96684
ι' : Sort u_2
f : Filter α
h : IsCountablyGenerated f
p : ι' → Prop
s : ι' → Set α
hs : HasBasis f p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } :=
  fun n =>
    Nat.recOn n (index hs (x' 0) (_ : x' 0 ∈ f)) fun n xn => index hs (x' (n + 1) ∩ s ↑xn) (_ : x' (n + 1) ∩ s ↑xn ∈ f)
x_mono : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : HasAntitoneBasis (⨅ (i : ℕ), 𝓟 (s ↑(x i))) fun i => s ↑(x i)
i : ℕ
⊢ s ↑(x i) ∈ f
cases i <;> apply hs.set_index_mem