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

case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s) → s ∈ pi f
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f ↔ ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s
constructor
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      Set.Finite I ∧
        ∃ V,
          (∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i) ∧
            (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (s = ⋂ (i : ι) (_ : i ∈ I), V i) ∧ s = ⋂ (i : ι), V i) →
    ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I), eval a ⁻¹' t a) ⊆ s
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s
simp only [pi, mem_iInf', mem_comap, pi_def]
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a) ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      Set.Finite I ∧
        ∃ V,
          (∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i) ∧
            (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (s = ⋂ (i : ι) (_ : i ∈ I), V i) ∧ s = ⋂ (i : ι), V i) →
    ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I), eval a ⁻¹' t a) ⊆ s
rintro ⟨I, If, V, hVf, -, rfl, -⟩
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a) ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a) ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
choose t htf htV using hVf
no goals
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ t, (∀ (i : ι), t i ∈ f i) ∧ (⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a) ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
case mpr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ s
⊢ s ∈ pi f
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s) → s ∈ pi f
rintro ⟨I, If, t, htf, hts⟩
no goals
case mpr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ s
⊢ s ∈ pi f
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts