α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ map (Prod.map (fun x => b) id) (Filter.coprod (𝓟 {a}) (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)
rw [principal_coprod_principal, map_principal]
case e_s
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
congr
case e_s.h.mk
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ
case e_s
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ
ext ⟨b', i'⟩
case e_s.h.mk.mp
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

case e_s.h.mk.mpr
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
case e_s.h.mk
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ
constructor
case e_s.h.mk.mp.intro.mk.intro.refl
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ
case e_s.h.mk.mp
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ
rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
no goals
case e_s.h.mk.mp.intro.mk.intro.refl
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ
simp
case e_s.h.mk.mpr.intro
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
case e_s.h.mk.mpr
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
rintro ⟨h₁, _⟩
case e_s.h.mk.mpr.intro
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')
case e_s.h.mk.mpr.intro
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
use (a, i')
no goals
case e_s.h.mk.mpr.intro
α✝ : Type ?u.66772
β✝ : Type ?u.66775
γ : Type ?u.66778
δ : Type ?u.66781
ι✝ : Sort ?u.66784
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')
simpa using h₁.symm