α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
let f := fun s : Set (α × α) =>
      { p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α)) }
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
  delta gen
  simp [map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp,
    image_swap_eq_preimage_swap]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h₂ : Filter.lift' (𝓤 α) f ≤ Filter.lift' (𝓤 α) gen
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
  uniformity_lift_le_swap
    (monotone_principal.comp
      (monotone_setOf fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
    (by
      have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
      simp [Function.comp, h, mem_map']
      exact le_rfl)
no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h₂ : Filter.lift' (𝓤 α) f ≤ Filter.lift' (𝓤 α) gen
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
exact h₁.trans_le h₂
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) fun s => {p | s ∈ ↑p.fst ×ˢ ↑p.snd}) = Filter.lift' (𝓤 α) f
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
delta gen
no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) fun s => {p | s ∈ ↑p.fst ×ˢ ↑p.snd}) = Filter.lift' (𝓤 α) f
simp [map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp,
  image_swap_eq_preimage_swap]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ Filter.lift' (𝓤 α) gen
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
⊢ (Filter.lift (𝓤 α) fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ Filter.lift' (𝓤 α) gen
have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => 𝓟 {p | (fun p => (p.snd, p.fst)) ⁻¹' (Prod.swap ⁻¹' s) ∈ ↑p.fst ×ˢ ↑p.snd}) ≤
    Filter.lift' (𝓤 α) gen
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ Filter.lift' (𝓤 α) gen
simp [Function.comp, h, mem_map']
no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => 𝓟 {p | (fun p => (p.snd, p.fst)) ⁻¹' (Prod.swap ⁻¹' s) ∈ ↑p.fst ×ˢ ↑p.snd}) ≤
    Filter.lift' (𝓤 α) gen
exact le_rfl