[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
[PROOFSTEP]
simp only [pi, tendsto_iInf, tendsto_comap_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ Set.pi I s ∈ pi f
[PROOFSTEP]
rw [pi_def, biInter_eq_iInter]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ ⋂ (x : ↑I), eval ↑x ⁻¹' s ↑x ∈ pi f
[PROOFSTEP]
refine' mem_iInf_of_iInter hI (fun i => _) Subset.rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)
[PROOFSTEP]
exact preimage_mem_comap (h i i.2)
[GOAL]
ι : 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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
simp only [pi, mem_iInf', mem_comap, pi_def]
[GOAL]
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
[PROOFSTEP]
rintro ⟨I, If, V, hVf, -, rfl, -⟩
[GOAL]
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
[PROOFSTEP]
choose t htf htV using hVf
[GOAL]
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
[PROOFSTEP]
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨I, If, t, htf, hts⟩
[GOAL]
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
[PROOFSTEP]
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
⊢ s i ∈ f i
[PROOFSTEP]
rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
⊢ s i ∈ f i
[PROOFSTEP]
refine' mem_of_superset (htf i) fun x hx => _
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
⊢ x ∈ s i
[PROOFSTEP]
have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
this : ∀ (i : ι), Set.Nonempty (t i)
⊢ x ∈ s i
[PROOFSTEP]
choose g hg using this
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
⊢ x ∈ s i
[PROOFSTEP]
have : update g i x ∈ I'.pi t := fun j _ => by rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
⊢ update g i x j ∈ t j
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hi : j ∈ I
x : α j
hx : x ∈ t j
⊢ update g j x j ∈ t j
[PROOFSTEP]
simp [*]
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hne : j ≠ i
⊢ update g i x j ∈ t j
[PROOFSTEP]
simp [*]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
this : update g i x ∈ Set.pi I' t
⊢ x ∈ s i
[PROOFSTEP]
simpa using hts this i hi
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
ι' : ι → Type
s : (i : ι) → ι' i → Set (α i)
p : (i : ι) → ι' i → Prop
h : ∀ (i : ι), HasBasis (f i) (p i) (s i)
⊢ HasBasis (pi f) (fun If => Set.Finite If.fst ∧ ∀ (i : ι), i ∈ If.fst → p i (Prod.snd If i)) fun If =>
    Set.pi If.fst fun i => s i (Prod.snd If i)
[PROOFSTEP]
simpa [Set.pi_def] using hasBasis_iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ → ∃ i, f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp only [inf_principal_eq_bot, mem_pi]
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ (Set.pi univ s)ᶜ) → ∃ i, (s i)ᶜ ∈ f i
[PROOFSTEP]
contrapose!
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∀ (i : ι), ¬(s i)ᶜ ∈ f i) →
    ∀ (I : Set ι), Set.Finite I → ∀ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) → ¬Set.pi I t ⊆ (Set.pi univ s)ᶜ
[PROOFSTEP]
rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
⊢ False
[PROOFSTEP]
have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
this : ∀ (i : ι), Set.Nonempty (s i ∩ t i)
⊢ False
[PROOFSTEP]
choose x hxs hxt using this
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
x : (i : ι) → α i
hxs : ∀ (i : ι), x i ∈ s i
hxt : ∀ (i : ι), x i ∈ t i
⊢ False
[PROOFSTEP]
exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (Set.pi univ s) = ⊥
[PROOFSTEP]
simp only [inf_principal_eq_bot]
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, (s i)ᶜ ∈ f i) → (Set.pi univ s)ᶜ ∈ pi f
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
⊢ (Set.pi univ s)ᶜ ∈ pi f
[PROOFSTEP]
filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i, i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥) ↔ ∃ i, i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
refine' exists_congr fun i => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
by_cases hi : i ∈ I
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp [hi, NeBot.ne']
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
hi : ¬i ∈ I
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp [hi, NeBot.ne']
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ (i : ι), NeBot (f i ⊓ 𝓟 (s i))
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ NeBot (pi f ⊓ 𝓟 (Set.pi I s)) ↔ ∀ (i : ι), i ∈ I → NeBot (f i ⊓ 𝓟 (s i))
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥
[PROOFSTEP]
simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (pi f) ↔ ∀ (i : ι), NeBot (f i)
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
⊢ map (eval i) (pi f) = f i
[PROOFSTEP]
refine' le_antisymm (tendsto_eval_pi f i) fun s hs => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i
[PROOFSTEP]
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : Set.pi I t ⊆ eval i ⁻¹' s
⊢ s ∈ f i
[PROOFSTEP]
rw [← image_subset_iff] at hI 
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ s ∈ f i
[PROOFSTEP]
refine' mem_of_superset (htf i) ((subset_eval_image_pi _ _).trans hI)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ Set.Nonempty (Set.pi I t)
[PROOFSTEP]
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂
[PROOFSTEP]
refine' ⟨fun h => _, congr_arg pi⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
⊢ f₁ = f₂
[PROOFSTEP]
have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂
[PROOFSTEP]
haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), NeBot (f₂ i)
⊢ f₁ = f₂
[PROOFSTEP]
exact hle.antisymm (pi_le_pi.1 h.ge)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
[PROOFSTEP]
simp [Filter.coprodᵢ]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (eval i '' s)ᶜ ∈ f i
[PROOFSTEP]
simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (Filter.coprodᵢ f) ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, NeBot (f d)
[PROOFSTEP]
simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ NeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d)
[PROOFSTEP]
simp [coprodᵢ_neBot_iff', *]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
[PROOFSTEP]
simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff] using coprodᵢ_neBot_iff'.not
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ f = ⊥
[PROOFSTEP]
simpa [funext_iff] using coprodᵢ_neBot_iff.not
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)
[PROOFSTEP]
simp only [le_def, mem_map, mem_coprodᵢ_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x
[PROOFSTEP]
intro s h i
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
[PROOFSTEP]
obtain ⟨t, H, hH⟩ := h i
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
[PROOFSTEP]
exact ⟨{x : α i | m i x ∈ t}, H, fun x hx => hH hx⟩
