case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap
      (fun x =>
        ((↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.fst,
          (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ UniformInducing (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
constructor
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap
      (fun x =>
        ((↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.fst,
          (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap
      (fun x =>
        ((↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.fst,
          (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap
      (Prod.map (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
        (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
rw [← uniformity_comap] at hf⊢
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
congr
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) =
    UniformSpace.comap ((fun x x_1 => x ∘ x_1) f) (uniformSpace α β 𝔖)
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖
rw [← uniformSpace_eq hf, UniformOnFun.comap_eq]
no goals
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.78533
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) =
    UniformSpace.comap ((fun x x_1 => x ∘ x_1) f) (uniformSpace α β 𝔖)
rfl