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

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) = ⊥
ι : 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) = ⊥
constructor
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
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) = ⊥
simp only [inf_principal_eq_bot, mem_pi]
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ᶜ
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
contrapose!
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
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ᶜ
rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
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
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
have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
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
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
choose x hxs hxt using this
no goals
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
exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
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
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) = ⊥
simp only [inf_principal_eq_bot]
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
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
rintro ⟨i, hi⟩
no goals
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
filter_upwards [mem_pi_of_mem i hi]with x using mt fun h => h i trivial