case a
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.137464
α : Type u_1
β : Type u_2
γ : Type u_3
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.137464
α : Type u_1
β : Type u_2
γ : Type u_3
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)
ext1
no goals
case a
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.137464
α : Type u_1
β : Type u_2
γ : Type u_3
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α
simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]