case h.h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ ↑(comap f x✝¹) x✝ =
    ↑{ toFun := fun x => ↑x✝¹ y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X (↑x✝¹ y))) } x✝
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g => { toFun := fun x => ↑g y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X (↑g y))) }
ext
case h.h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (↑x✝¹ ∘ f) x✝ =
    ↑{ toFun := fun x => ↑x✝¹ y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X (↑x✝¹ y))) } x✝

case h.h.hf
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ Continuous f
case h.h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ ↑(comap f x✝¹) x✝ =
    ↑{ toFun := fun x => ↑x✝¹ y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X (↑x✝¹ y))) } x✝
rw [coe_comap]
no goals
case h.h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (↑x✝¹ ∘ f) x✝ =
    ↑{ toFun := fun x => ↑x✝¹ y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X (↑x✝¹ y))) } x✝
simp only [h, coe_mk, Function.comp_apply]
case h.h.hf
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ Continuous fun x => y
case h.h.hf
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ Continuous f
rw [show f = fun _ => y by ext; apply h]
no goals
case h.h.hf
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ Continuous fun x => y
exact continuous_const
case h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝² : LocallyConstant Y Z
x✝¹ x✝ : X
⊢ f x✝ = y
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ f = fun x => y
ext
no goals
case h
X : Type u_2
Y : Type u_1
Z : Type u_3
α : Type ?u.34199
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
x✝² : LocallyConstant Y Z
x✝¹ x✝ : X
⊢ f x✝ = y
apply h