α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort ?u.23551
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort ?u.23551
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
simp_rw [map_swap4_eq_comap, SProd.sprod, Filter.prod, comap_inf, comap_comap]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort ?u.23551
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
ac_rfl