-- Mathlib/Topology/UniformSpace/Completion.lean
theorem symm_gen : map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map (fun p => (p.2, p.1)) (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s => 𝓟 {p | (fun p => (p.2, p.1)) ⁻¹' (Prod.swap ⁻¹' s) ∈ ↑p.1 ×ˢ ↑p.2}) ≤ (𝓤 α).lift' gen

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
let f := fun s : Set (α × α) =>
      { p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α)) }

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f

Tactic:
delta gen

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' fun s => {p | s ∈ ↑p.1 ×ˢ ↑p.2}) = (𝓤 α).lift' f

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
  delta gen
  simp [f, map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp_def,
    image_swap_eq_preimage_swap]

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
exact h₁.trans_le h₂

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ ((𝓤 α).lift fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Tactic:
have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map (fun p => (p.2, p.1)) (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map (fun p => (p.2, p.1)) (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Tactic:
simp only [Function.comp, h, mem_map, f]

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map (fun p => (p.2, p.1)) (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s => 𝓟 {p | (fun p => (p.2, p.1)) ⁻¹' (Prod.swap ⁻¹' s) ∈ ↑p.1 ×ˢ ↑p.2}) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
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 only [Function.comp, h, mem_map, f]
      exact le_rfl)

Result:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Proof state:
α : Type u
inst✝ : UniformSpace α
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' fun s => {p | s ∈ ↑p.1 ×ˢ ↑p.2}) = (𝓤 α).lift' f

Tactic:
simp [f, map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp_def,
  image_swap_eq_preimage_swap]

Result:
no goals