case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ↑((comap f ∘ comap g) x✝¹) x✝ = ↑(comap (g ∘ f) x✝¹) x✝
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
⊢ comap f ∘ comap g = comap (g ∘ f)
ext
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ↑(comap f (comap g x✝¹)) x✝ = ↑(comap (g ∘ f) x✝¹) x✝
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ↑((comap f ∘ comap g) x✝¹) x✝ = ↑(comap (g ∘ f) x✝¹) x✝
rw [Function.comp_apply]
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ((↑x✝¹ ∘ g) ∘ f) x✝ = (↑x✝¹ ∘ g ∘ f) x✝
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ↑(comap f (comap g x✝¹)) x✝ = ↑(comap (g ∘ f) x✝¹) x✝
simp only [hf, hg, hg.comp hf, coe_comap]
no goals
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_1
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
x✝¹ : LocallyConstant Z α
x✝ : X
⊢ ((↑x✝¹ ∘ g) ∘ f) x✝ = (↑x✝¹ ∘ g ∘ f) x✝
rfl