[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_have 1 → 4
[GOAL]
case tfae_1_to_4
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
exact fun h y => h { y }
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_have 4 → 3
[GOAL]
case tfae_4_to_3
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
⊢ (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
exact fun h x => h (f x)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
⊢ (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
exact fun h x => IsOpen.mem_nhds (h x) rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_have 2 → 5
[GOAL]
case tfae_2_to_5
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
[PROOFSTEP]
intro h x
[GOAL]
case tfae_2_to_5
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
[PROOFSTEP]
rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
[GOAL]
case tfae_2_to_5.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
U : Set X
eq : U ⊆ {x_1 | (fun x' => f x' = f x) x_1}
hU : IsOpen U
hx : x ∈ U
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
[PROOFSTEP]
exact ⟨U, hU, hx, eq⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_have 5 → 1
[GOAL]
case tfae_5_to_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
⊢ (∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x) → IsLocallyConstant f
[PROOFSTEP]
intro h s
[GOAL]
case tfae_5_to_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
s : Set Y
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
refine' isOpen_iff_forall_mem_open.2 fun x hx => _
[GOAL]
case tfae_5_to_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
⊢ ∃ t, t ⊆ f ⁻¹' s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rcases h x with ⟨U, hU, hxU, eq⟩
[GOAL]
case tfae_5_to_1.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen U
hxU : x ∈ U
eq : ∀ (x' : X), x' ∈ U → f x' = f x
⊢ ∃ t, t ⊆ f ⁻¹' s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x
tfae_5_to_1 : (∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x) → IsLocallyConstant f
⊢ TFAE
    [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]
[PROOFSTEP]
tfae_finish
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen (g ∘ f ⁻¹' s)
[PROOFSTEP]
rw [Set.preimage_comp]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))
[PROOFSTEP]
exact hf _
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (g ∘ f ⁻¹' s)
[PROOFSTEP]
rw [Set.preimage_comp]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))
[PROOFSTEP]
exact hf.isOpen_preimage _ (hg _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y
[PROOFSTEP]
let U := f ⁻¹' {f y}
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y
[PROOFSTEP]
suffices : x ∉ Uᶜ
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
this : ¬x ∈ Uᶜ
⊢ f x = f y
case this
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
[PROOFSTEP]
exact Classical.not_not.1 this
[GOAL]
case this
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
[PROOFSTEP]
intro hxV
[GOAL]
case this
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False
[PROOFSTEP]
specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
[GOAL]
case this
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ
[PROOFSTEP]
simp only [union_compl_self, subset_univ]
[GOAL]
case this
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : Set.Nonempty (s ∩ (U ∩ Uᶜ))
⊢ False
[PROOFSTEP]
simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs 
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
⊢ ∃ y, f = Function.const X y
[PROOFSTEP]
cases' isEmpty_or_nonempty X with h h
[GOAL]
case inl
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y
[PROOFSTEP]
exact ⟨Classical.arbitrary Y, funext <| h.elim⟩
[GOAL]
case inr
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y
[PROOFSTEP]
exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
⊢ Set.Finite (range f)
[PROOFSTEP]
letI : TopologicalSpace Y := ⊥
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ Set.Finite (range f)
[PROOFSTEP]
haveI := discreteTopology_bot Y
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ Set.Finite (range f)
[PROOFSTEP]
exact (isCompact_range hf.continuous).finite_of_discrete
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [← preimage_image_eq s inj, preimage_preimage]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))
[PROOFSTEP]
exact h (g '' s)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
⊢ Function.Injective LocallyConstant.toFun
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩ _
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
toFun✝¹ : X → Y
isLocallyConstant✝¹ : IsLocallyConstant toFun✝¹
toFun✝ : X → Y
isLocallyConstant✝ : IsLocallyConstant toFun✝
a✝ :
  { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ }.toFun =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }.toFun
⊢ { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ } =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }
[PROOFSTEP]
congr
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsLocallyConstant fun x => if x ∈ U then 0 else 1
[PROOFSTEP]
refine IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩
[GOAL]
case refine_1
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen ((fun x => if x ∈ U then 0 else 1) ⁻¹' {0})
[PROOFSTEP]
convert hU.1 using 1
[GOAL]
case h.e'_3
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ (fun x => if x ∈ U then 0 else 1) ⁻¹' {0} = U
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ (fun x => if x ∈ U then 0 else 1) ⁻¹' {0} ↔ x✝ ∈ U
[PROOFSTEP]
simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff, Nat.succ_succ_ne_one]
[GOAL]
case h.e'_3.h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ ¬x✝ ∈ U → False ↔ x✝ ∈ U
[PROOFSTEP]
tauto
[GOAL]
case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen ((fun x => if x ∈ U then 0 else 1) ⁻¹' {1})
[PROOFSTEP]
rw [← isClosed_compl_iff]
[GOAL]
case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsClosed ((fun x => if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ
[PROOFSTEP]
convert hU.2
[GOAL]
case h.e'_3
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ((fun x => if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ = U
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ((fun x => if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ ↔ x✝ ∈ U
[PROOFSTEP]
simp
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ↑(ofClopen hU) ⁻¹' {0} = U
[PROOFSTEP]
ext
[GOAL]
case h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ↑(ofClopen hU) ⁻¹' {0} ↔ x✝ ∈ U
[PROOFSTEP]
simp only [ofClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage, ite_eq_left_iff,
  Nat.succ_succ_ne_one]
[GOAL]
case h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ ¬x✝ ∈ U → False ↔ x✝ ∈ U
[PROOFSTEP]
tauto
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ↑(ofClopen hU) ⁻¹' {1} = Uᶜ
[PROOFSTEP]
ext
[GOAL]
case h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ↑(ofClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ
[PROOFSTEP]
simp only [ofClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage, ite_eq_right_iff, mem_compl_iff,
  Nat.succ_succ_ne_one]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X✝
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ↑f ⁻¹' {0} = ↑g ⁻¹' {0}
⊢ f = g
[PROOFSTEP]
simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h 
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X✝
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
⊢ f = g
[PROOFSTEP]
ext1 x
[GOAL]
case h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X✝
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
x : X
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact Fin.fin_two_eq_of_eq_zero_iff (h x)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
⊢ ∃ y, f = const X y
[PROOFSTEP]
rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)
[GOAL]
case inl.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
x : X
⊢ ∃ y, f = const X y
[PROOFSTEP]
exact ⟨f x, f.eq_const x⟩
[GOAL]
case inr
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ y, f = const X y
[PROOFSTEP]
exact ⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ IsOpen ((fun x a => ↑(f a) x) ⁻¹' {g})
[PROOFSTEP]
have : (fun (x : X) (a : α) => f a x) ⁻¹' { g } = ⋂ a : α, f a ⁻¹' {g a} := by ext; simp [Function.funext_iff]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ (fun x a => ↑(f a) x) ⁻¹' {g} = ⋂ (a : α), ↑(f a) ⁻¹' {g a}
[PROOFSTEP]
ext
[GOAL]
case h
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x✝ : X
⊢ x✝ ∈ (fun x a => ↑(f a) x) ⁻¹' {g} ↔ x✝ ∈ ⋂ (a : α), ↑(f a) ⁻¹' {g a}
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this : (fun x a => ↑(f a) x) ⁻¹' {g} = ⋂ (a : α), ↑(f a) ⁻¹' {g a}
⊢ IsOpen ((fun x a => ↑(f a) x) ⁻¹' {g})
[PROOFSTEP]
rw [this]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this : (fun x a => ↑(f a) x) ⁻¹' {g} = ⋂ (a : α), ↑(f a) ⁻¹' {g a}
⊢ IsOpen (⋂ (a : α), ↑(f a) ⁻¹' {g a})
[PROOFSTEP]
exact isOpen_iInter fun a => (f a).isLocallyConstant _
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
⊢ LocallyConstant Y Z → LocallyConstant X Z
[PROOFSTEP]
by_cases H : Nonempty X
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : Nonempty X
⊢ LocallyConstant Y Z → LocallyConstant X Z
[PROOFSTEP]
intro g
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : Nonempty X
g : LocallyConstant Y Z
⊢ LocallyConstant X Z
[PROOFSTEP]
exact const X (g <| f <| Classical.arbitrary X)
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : ¬Nonempty X
⊢ LocallyConstant Y Z → LocallyConstant X Z
[PROOFSTEP]
refine fun _ => ⟨fun x => (H ⟨x⟩).elim, fun s => ?_⟩
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : ¬Nonempty X
x✝ : LocallyConstant Y Z
s : Set Z
⊢ IsOpen ((fun x => False.elim (_ : False)) ⁻¹' s)
[PROOFSTEP]
rw [isOpen_iff_nhds]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : ¬Nonempty X
x✝ : LocallyConstant Y Z
s : Set Z
⊢ ∀ (a : X), a ∈ (fun x => False.elim (_ : False)) ⁻¹' s → 𝓝 a ≤ 𝓟 ((fun x => False.elim (_ : False)) ⁻¹' s)
[PROOFSTEP]
intro x
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ¬Continuous f
H : ¬Nonempty X
x✝ : LocallyConstant Y Z
s : Set Z
x : X
⊢ x ∈ (fun x => False.elim (_ : False)) ⁻¹' s → 𝓝 x ≤ 𝓟 ((fun x => False.elim (_ : False)) ⁻¹' s)
[PROOFSTEP]
exact (H ⟨x⟩).elim
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
⊢ ↑(comap f g) = ↑g ∘ f
[PROOFSTEP]
rw [comap, dif_pos hf]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
⊢ ↑{ toFun := ↑g ∘ f, isLocallyConstant := (_ : IsLocallyConstant (g.toFun ∘ f)) } = ↑g ∘ f
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
x : X
⊢ ↑(comap f g) x = ↑g (f x)
[PROOFSTEP]
simp only [hf, coe_comap, Function.comp_apply]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ comap id = id
[PROOFSTEP]
ext
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝¹ : LocallyConstant X Z
x✝ : X
⊢ ↑(comap id x✝¹) x✝ = ↑(id x✝¹) x✝
[PROOFSTEP]
simp only [continuous_id, id.def, Function.comp.right_id, coe_comap]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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)
[PROOFSTEP]
ext
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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✝
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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✝
[PROOFSTEP]
simp only [hf, hg, hg.comp hf, coe_comap]
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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 α
⊢ comap f (comap g x) = comap (g ∘ f) x
[PROOFSTEP]
rw [← comap_comp f g hf hg]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : 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 α
⊢ comap f (comap g x) = (comap f ∘ comap g) x
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g => const X (↑g y)
[PROOFSTEP]
ext
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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✝ = ↑(const X (↑x✝¹ y)) x✝
[PROOFSTEP]
rw [coe_comap]
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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✝ = ↑(const X (↑x✝¹ y)) x✝
[PROOFSTEP]
simp only [Function.comp_apply, h, coe_const, Function.const_apply]
[GOAL]
case h.h.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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
[PROOFSTEP]
rw [show f = fun _ => y by ext; apply h]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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
[PROOFSTEP]
apply h
[GOAL]
case h.h.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
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
[PROOFSTEP]
exact continuous_const
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
⊢ Function.Injective (comap f)
[PROOFSTEP]
intro a b h
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
a b : LocallyConstant Y Z
h : comap f a = comap f b
⊢ a = b
[PROOFSTEP]
rw [LocallyConstant.ext_iff] at h 
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
a b : LocallyConstant Y Z
h : ∀ (x : X), ↑(comap f a) x = ↑(comap f b) x
⊢ a = b
[PROOFSTEP]
ext y
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
a b : LocallyConstant Y Z
h : ∀ (x : X), ↑(comap f a) x = ↑(comap f b) x
y : Y
⊢ ↑a y = ↑b y
[PROOFSTEP]
obtain ⟨x, hx⟩ := hfs y
[GOAL]
case h.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
a b : LocallyConstant Y Z
h : ∀ (x : X), ↑(comap f a) x = ↑(comap f b) x
y : Y
x : X
hx : f x = y
⊢ ↑a y = ↑b y
[PROOFSTEP]
specialize h x
[GOAL]
case h.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
hfs : Function.Surjective f
a b : LocallyConstant Y Z
y : Y
x : X
hx : f x = y
h : ↑(comap f a) x = ↑(comap f b) x
⊢ ↑a y = ↑b y
[PROOFSTEP]
rwa [coe_comap_apply _ _ hf, coe_comap_apply _ _ hf, hx] at h 
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen (Set.mulIndicator U ↑f ⁻¹' s)
[PROOFSTEP]
rw [mulIndicator_preimage, Set.ite, Set.diff_eq]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen (↑f ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)
[PROOFSTEP]
exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
⊢ Function.LeftInverse (comap ↑e) (comap ↑(Homeomorph.symm e))
[PROOFSTEP]
intro
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
x✝ : LocallyConstant X Z
⊢ comap (↑e) (comap (↑(Homeomorph.symm e)) x✝) = x✝
[PROOFSTEP]
rw [comap_comap _ _ e.continuous e.symm.continuous]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
x✝ : LocallyConstant X Z
⊢ comap (↑(Homeomorph.symm e) ∘ ↑e) x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
⊢ Function.RightInverse (comap ↑e) (comap ↑(Homeomorph.symm e))
[PROOFSTEP]
intro
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
x✝ : LocallyConstant Y Z
⊢ comap (↑(Homeomorph.symm e)) (comap (↑e) x✝) = x✝
[PROOFSTEP]
rw [comap_comap _ _ e.symm.continuous e.continuous]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
x✝ : LocallyConstant Y Z
⊢ comap (↑e ∘ ↑(Homeomorph.symm e)) x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun f { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun g { val := x, property := (_ : x ∈ C₂) }
inst✝ : (j : X) → Decidable (j ∈ C₁)
⊢ IsLocallyConstant fun i =>
    if hi : i ∈ C₁ then ↑f { val := i, property := hi } else ↑g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
let dZ : TopologicalSpace Z := ⊥
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun f { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun g { val := x, property := (_ : x ∈ C₂) }
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
⊢ IsLocallyConstant fun i =>
    if hi : i ∈ C₁ then ↑f { val := i, property := hi } else ↑g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
haveI : DiscreteTopology Z := discreteTopology_bot Z
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun f { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun g { val := x, property := (_ : x ∈ C₂) }
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
⊢ IsLocallyConstant fun i =>
    if hi : i ∈ C₁ then ↑f { val := i, property := hi } else ↑g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
obtain ⟨f, hf⟩ := f
[GOAL]
case mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
g : LocallyConstant (↑C₂) Z
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf : IsLocallyConstant f
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun g { val := x, property := (_ : x ∈ C₂) }
⊢ IsLocallyConstant fun i =>
    if hi : i ∈ C₁ then ↑{ toFun := f, isLocallyConstant := hf } { val := i, property := hi }
    else ↑g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
obtain ⟨g, hg⟩ := g
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf : IsLocallyConstant f
g : ↑C₂ → Z
hg : IsLocallyConstant g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg } { val := x, property := (_ : x ∈ C₂) }
⊢ IsLocallyConstant fun i =>
    if hi : i ∈ C₁ then ↑{ toFun := f, isLocallyConstant := hf } { val := i, property := hi }
    else ↑{ toFun := g, isLocallyConstant := hg } { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
rw [IsLocallyConstant.iff_continuous] at hf hg ⊢
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous fun i =>
    if hi : i ∈ C₁ then ↑{ toFun := f, isLocallyConstant := hf✝ } { val := i, property := hi }
    else ↑{ toFun := g, isLocallyConstant := hg✝ } { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
dsimp only [coe_mk]
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
rw [Set.union_eq_iUnion] at h 
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) }
[PROOFSTEP]
refine' (locallyFinite_of_finite _).continuous h (fun i ↦ _) (fun i ↦ _)
[GOAL]
case mk.mk.refine'_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
i : Bool
⊢ IsClosed (bif i then C₁ else C₂)
[PROOFSTEP]
cases i <;> [exact h₂; exact h₁]
[GOAL]
case mk.mk.refine'_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
i : Bool
⊢ IsClosed (bif i then C₁ else C₂)
[PROOFSTEP]
cases i
[GOAL]
case mk.mk.refine'_1.false
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ IsClosed (bif false then C₁ else C₂)
[PROOFSTEP]
exact h₂
[GOAL]
case mk.mk.refine'_1.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ IsClosed (bif true then C₁ else C₂)
[PROOFSTEP]
exact h₁
[GOAL]
case mk.mk.refine'_2
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
i : Bool
⊢ ContinuousOn
    (fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) })
    (bif i then C₁ else C₂)
[PROOFSTEP]
cases i
[GOAL]
case mk.mk.refine'_2.false
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ ContinuousOn
    (fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) })
    (bif false then C₁ else C₂)
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
case mk.mk.refine'_2.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ ContinuousOn
    (fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) })
    (bif true then C₁ else C₂)
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
case mk.mk.refine'_2.false
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous
    (restrict (bif false then C₁ else C₂) fun i =>
      if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) })
[PROOFSTEP]
convert hg
[GOAL]
case h.e'_5.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
e_1✝ : ↑(bif false then C₁ else C₂) = ↑C₂
⊢ (restrict (bif false then C₁ else C₂) fun i =>
      if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) }) =
    g
[PROOFSTEP]
ext x
[GOAL]
case h.e'_5.h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
e_1✝ : ↑(bif false then C₁ else C₂) = ↑C₂
x : ↑(bif false then C₁ else C₂)
⊢ restrict (bif false then C₁ else C₂)
      (fun i => if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) }) x =
    g x
[PROOFSTEP]
simp only [cond_false, restrict_apply, Subtype.coe_eta, dite_eq_right_iff]
[GOAL]
case h.e'_5.h.h
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
e_1✝ : ↑(bif false then C₁ else C₂) = ↑C₂
x : ↑(bif false then C₁ else C₂)
⊢ ∀ (h : ↑x ∈ C₁), f { val := ↑x, property := (_ : ↑x ∈ C₁) } = g x
[PROOFSTEP]
exact fun hx ↦ hfg x ⟨hx, x.prop⟩
[GOAL]
case mk.mk.refine'_2.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous
    (restrict (bif true then C₁ else C₂) fun i =>
      if hi : i ∈ C₁ then f { val := i, property := hi } else g { val := i, property := (_ : i ∈ C₂) })
[PROOFSTEP]
simp only [cond_true, restrict_dite, Subtype.coe_eta]
[GOAL]
case mk.mk.refine'_2.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ (b : Bool), bif b then C₁ else C₂) = univ
inst✝ : (j : X) → Decidable (j ∈ C₁)
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    LocallyConstant.toFun { toFun := f, isLocallyConstant := hf✝ } { val := x, property := (_ : x ∈ C₁) } =
      LocallyConstant.toFun { toFun := g, isLocallyConstant := hg✝ } { val := x, property := (_ : x ∈ C₂) }
⊢ Continuous fun a => f a
[PROOFSTEP]
exact hf
