-- 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 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))

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⟩)

Result:
no goals

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, generate s = ⨅ i, 𝓟 (x i)

Tactic:
rw [generate_eq_biInf]

Result:
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)

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, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis 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

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

Proof state:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ x, f = ⨅ i, 𝓟 (x i)

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

Result:
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, generate s = ⨅ i, 𝓟 (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, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (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]

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
⊢ ∃ 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 (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)

Tactic:
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)

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

Proof state:
α : 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)
i : ℕ
⊢ s ↑(x i) ∈ f

Tactic:
cases i <;> apply hs.set_index_mem

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' : ℕ → 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) ⊆ x' i

Tactic:
rintro (_ | i)

Result:
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)

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
⊢ f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) i)

Tactic:
have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti

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
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i => s ↑(x i)
⊢ f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) 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)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)

Tactic:
have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)

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 (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)