-- Mathlib/Order/Filter/Pi.lean
theorem mem_pi {s : Set (∀ i, α i)} :
    s ∈ pi f ↔ ∃ I : Set ι, I.Finite ∧ ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s

Proof state:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

Tactic:
simp only [pi, mem_iInf', mem_comap, pi_def]

Result:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      I.Finite ∧
        ∃ V, (∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i) ∧ (∀ i ∉ I, V i = univ) ∧ s = ⋂ i ∈ I, V i ∧ s = ⋂ i, V i) →
    ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I, eval a ⁻¹' t a ⊆ s

Proof state:
case mpr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi t ⊆ s
⊢ s ∈ pi f

Tactic:
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f ↔ ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Proof state:
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i

Tactic:
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩

Result:
no goals

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Tactic:
rintro ⟨I, If, t, htf, hts⟩

Result:
case mpr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi t ⊆ s
⊢ s ∈ pi f

Proof state:
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i

Tactic:
choose t htf htV using hVf

Result:
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i

Proof state:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      I.Finite ∧
        ∃ V, (∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i) ∧ (∀ i ∉ I, V i = univ) ∧ s = ⋂ i ∈ I, V i ∧ s = ⋂ i, V i) →
    ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I, eval a ⁻¹' t a ⊆ s

Tactic:
rintro ⟨I, If, V, hVf, -, rfl, -⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i