no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
x✝ : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ ((preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) s ↔ (a₁, a₂) ∈ id s
simp [preimage, gen, pureCauchy, prod_principal_principal]
no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : (preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen = id
⊢ Filter.lift' (𝓤 α) ((preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) = 𝓤 α
simp [this]