-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem HasBasis.exists_antitone_subbasis {f : Filter α} [h : f.IsCountablyGenerated]
    {p : ι' → Prop} {s : ι' → Set α} (hs : f.HasBasis p s) :
    ∃ x : ℕ → ι', (∀ i, p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)

Proof state:
case mk.intro.intro
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s✝ : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s✝
⊢ ∃ x, ⨅ s_1 ∈ s, 𝓟 s_1 = ⨅ i, 𝓟 (x i)

Tactic:
exact countable_biInf_principal_eq_seq_iInf hsc

Result:
no goals

Proof state:
case intro
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i => s ↑(x i)
⊢ f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) i)

Tactic:
convert this

Result:
case h.e'_4
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i => s ↑(x i)
⊢ f = ⨅ i, 𝓟 (s ↑(x i))

Proof state:
case zero
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i => s ↑(x i)
⊢ s ↑(x 0) ⊆ x' 0

case succ
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i => s ↑(x i)
i : ℕ
⊢ s ↑(x (i + 1)) ⊆ x' (i + 1)

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

Result:
no goals

Proof state:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ 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

Result:
case intro
α : 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)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)

Proof state:
case intro
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone 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:
refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩

Result:
case intro
α : 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 n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i => s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) i)