[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


[GOAL]
m n : ℤ
⊢ dist m n = ↑|m - n|
[PROOFSTEP]
rw [dist_eq]
[GOAL]
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|
[PROOFSTEP]
norm_cast
[GOAL]
⊢ Pairwise fun m n => 1 ≤ dist m n
[PROOFSTEP]
intro m n hne
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
[PROOFSTEP]
rw [dist_eq]
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|
[PROOFSTEP]
norm_cast
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
[PROOFSTEP]
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
[GOAL]
x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
[PROOFSTEP]
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]
[GOAL]
x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋
[PROOFSTEP]
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
[GOAL]
x : ℤ
r : ℝ
⊢ IsCompact (closedBall x r)
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
x : ℤ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉ ⌊↑x + r⌋)
[PROOFSTEP]
exact (Set.finite_Icc _ _).isCompact
[GOAL]
⊢ cocompact ℤ = atBot ⊔ atTop
[PROOFSTEP]
simp_rw [← comap_dist_right_atTop_eq_cocompact (0 : ℤ), dist_eq', sub_zero, ← comap_abs_atTop, ←
  @Int.comap_cast_atTop ℝ, comap_comap]
[GOAL]
⊢ comap (fun y => ↑|y|) atTop = comap (Int.cast ∘ abs) atTop
[PROOFSTEP]
rfl
[GOAL]
⊢ cofinite = atBot ⊔ atTop
[PROOFSTEP]
rw [← cocompact_eq_cofinite, cocompact_eq]


[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
⊢ ∀ (t : ↑unitInterval) (x : A),
    x ∈ S →
      ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                              ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.pi f) x ∧
        ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                              ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.pi g) x
[PROOFSTEP]
intro t x hx
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A),
                        ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                          ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
              (t, x))
        x =
      ↑(ContinuousMap.pi f) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A),
                        ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                          ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
              (t, x))
        x =
      ↑(ContinuousMap.pi g) x
[PROOFSTEP]
dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap]
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ (↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i => ↑(f i) x) ∧
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i => ↑(g i) x
[PROOFSTEP]
simp only [Function.funext_iff, ← forall_and]
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ∀ (x_1 : I),
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) x_1 = ↑(f x_1) x ∧
      ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) x_1 = ↑(g x_1) x
[PROOFSTEP]
intro i
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
i : I
⊢ ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) i = ↑(f i) x ∧
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) i = ↑(g i) x
[PROOFSTEP]
exact (homotopies i).prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
x : A
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => (↑F t, ↑G t)) (0, x) = ↑(ContinuousMap.prodMk f₀ g₀) x
[PROOFSTEP]
simp only [prod_eval, Homotopy.apply_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
x : A
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => (↑F t, ↑G t)) (1, x) = ↑(ContinuousMap.prodMk f₁ g₁) x
[PROOFSTEP]
simp only [prod_eval, Homotopy.apply_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
⊢ ∀ (t : ↑unitInterval) (x : A),
    x ∈ S →
      ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(prodMk f₀ g₀) x ∧
        ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(prodMk f₁ g₁) x
[PROOFSTEP]
intro t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
have hF := F.prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF :
  ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₁ x
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
have hG := G.prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF :
  ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₁ x
hG :
  ↑(mk fun x => ContinuousMap.toFun G.toContinuousMap (t, x)) x = ↑g₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun G.toContinuousMap (t, x)) x = ↑g₁ x
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
simp only [coe_mk, prod_eval, Prod.mk.inj_iff, Homotopy.prod] at hF hG ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF : ContinuousMap.toFun F.toContinuousMap (t, x) = ↑f₀ x ∧ ContinuousMap.toFun F.toContinuousMap (t, x) = ↑f₁ x
hG : ContinuousMap.toFun G.toContinuousMap (t, x) = ↑g₀ x ∧ ContinuousMap.toFun G.toContinuousMap (t, x) = ↑g₁ x
⊢ (↑F.toHomotopy (t, x) = ↑f₀ x ∧ ↑G.toHomotopy (t, x) = ↑g₀ x) ∧
    ↑F.toHomotopy (t, x) = ↑f₁ x ∧ ↑G.toHomotopy (t, x) = ↑g₁ x
[PROOFSTEP]
exact ⟨⟨hF.1, hG.1⟩, ⟨hF.2, hG.2⟩⟩
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (γ i)) =
    Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi γ)
[PROOFSTEP]
unfold pi
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.map Path.pi (_ : ∀ (x y : (i : ι) → Path (as i) (bs i)), x ≈ y → Nonempty (Homotopy (Path.pi x) (Path.pi y)))
      (Quotient.choice fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (γ i)) =
    Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi γ)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi γ₀ ⬝ pi γ₁ = pi fun i => γ₀ i ⬝ γ₁ i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) γ₁
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ ∀ (a : (i : ι) → Path (bs i) (cs i)),
    (pi γ₀ ⬝ pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
      pi fun i => γ₀ i ⬝ (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ (pi γ₀ ⬝ pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
    pi fun i => γ₀ i ⬝ (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) γ₀
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ ∀ (a_1 : (i : ι) → Path (as i) (bs i)),
    ((pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a_1 i)) ⬝
        pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
      pi fun i =>
        (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a_1 i)) i ⬝
          (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ((pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) ⬝
      pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
    pi fun i =>
      (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i ⬝
        (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
simp only [pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi fun i => a✝ i) ⬝
      Quotient.mk (Homotopic.setoid (fun i => bs i) fun i => cs i) (Path.pi fun i => a i) =
    pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i) ⬝ Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)
[PROOFSTEP]
rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => Quotient.mk (Homotopic.setoid (as i) (cs i)) (Path.trans (a✝ i) (a i))) =
    pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i) ⬝ Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ proj i (pi paths) = paths i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) paths
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ ∀ (a : (i : ι) → Path (as i) (bs i)),
    proj i (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a i)) =
      (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a i)) i
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
unfold proj
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mapFn (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) (ContinuousMap.mk fun p => p i) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
rw [pi_lift, ← Path.Homotopic.map_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk
      (Homotopic.setoid (↑(ContinuousMap.mk fun p => p i) fun i => as i)
        (↑(ContinuousMap.mk fun p => p i) fun i => bs i))
      (Path.map (Path.pi fun i => a✝ i) (_ : Continuous ↑(ContinuousMap.mk fun p => p i))) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i => proj i p) = p
[PROOFSTEP]
apply Quotient.inductionOn (motive := _) p
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ ∀ (a : Path as bs),
    (pi fun i => proj i (Quotient.mk (Homotopic.setoid as bs) a)) = Quotient.mk (Homotopic.setoid as bs) a
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i => proj i (Quotient.mk (Homotopic.setoid as bs) a✝)) = Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
unfold proj
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i => Quotient.mapFn (Quotient.mk (Homotopic.setoid as bs) a✝) (ContinuousMap.mk fun p => p i)) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
simp_rw [← Path.Homotopic.map_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i =>
      Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk fun p => p i) as) (↑(ContinuousMap.mk fun p => p i) bs))
        (Path.map a✝ (_ : Continuous ↑(ContinuousMap.mk fun p => p i)))) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
erw [pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i)
      (Path.pi fun i => Path.map a✝ (_ : Continuous ↑(ContinuousMap.mk fun p => p i))) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝ prod r₁ r₂ =
      prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ r₁) (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ r₂)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
⊢ prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝ prod r₁ r₂ =
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ r₁) (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ r₂)
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) r₁ r₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
⊢ ∀ (a_1 : Path a₂ a₃) (b_1 : Path b₂ b₃),
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝
        prod (Quotient.mk (Homotopic.setoid a₂ a₃) a_1) (Quotient.mk (Homotopic.setoid b₂ b₃) b_1) =
      prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ Quotient.mk (Homotopic.setoid a₂ a₃) a_1)
        (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ Quotient.mk (Homotopic.setoid b₂ b₃) b_1)
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝
      prod (Quotient.mk (Homotopic.setoid a₂ a₃) a✝) (Quotient.mk (Homotopic.setoid b₂ b₃) b✝) =
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ Quotient.mk (Homotopic.setoid a₂ a₃) a✝)
      (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ Quotient.mk (Homotopic.setoid b₂ b₃) b✝)
[PROOFSTEP]
simp only [prod_lift, ← Path.Homotopic.comp_lift, Path.trans_prod_eq_prod_trans]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ projLeft (prod q₁ q₂) = q₁
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    projLeft (prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b)) =
      Quotient.mk (Homotopic.setoid a₁ a₂) a
[PROOFSTEP]
intro p₁ p₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ projLeft (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂)) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
unfold projLeft
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mapFn (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂))
      (ContinuousMap.mk Prod.fst) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
rw [prod_lift, ← Path.Homotopic.map_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.fst) (a₁, b₁)) (↑(ContinuousMap.mk Prod.fst) (a₂, b₂)))
      (Path.map (Path.prod p₁ p₂) (_ : Continuous ↑(ContinuousMap.mk Prod.fst))) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ projRight (prod q₁ q₂) = q₂
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    projRight (prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b)) =
      Quotient.mk (Homotopic.setoid b₁ b₂) b
[PROOFSTEP]
intro p₁ p₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ projRight (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂)) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
unfold projRight
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mapFn (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂))
      (ContinuousMap.mk Prod.snd) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
rw [prod_lift, ← Path.Homotopic.map_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.snd) (a₁, b₁)) (↑(ContinuousMap.mk Prod.snd) (a₂, b₂)))
      (Path.map (Path.prod p₁ p₂) (_ : Continuous ↑(ContinuousMap.mk Prod.snd))) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p
[PROOFSTEP]
apply Quotient.inductionOn (motive := _) p
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ ∀ (a : Path (a₁, b₁) (a₂, b₂)),
    prod (projLeft (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a))
        (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a)) =
      Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a
[PROOFSTEP]
intro p'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'))
      (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p')) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
unfold projLeft
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.fst))
      (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p')) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
unfold projRight
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.fst))
      (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.snd)) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
simp only [← Path.Homotopic.map_lift, prod_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod
      (Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.fst) (a₁, b₁)) (↑(ContinuousMap.mk Prod.fst) (a₂, b₂)))
        (Path.map p' (_ : Continuous ↑(ContinuousMap.mk Prod.fst))))
      (Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.snd) (a₁, b₁)) (↑(ContinuousMap.mk Prod.snd) (a₂, b₂)))
        (Path.map p' (_ : Continuous ↑(ContinuousMap.mk Prod.snd)))) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
congr


[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
refine' (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr _
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ (fun x => 1) =ᶠ[nhds a] ↑SignType.sign
[PROOFSTEP]
rw [Filter.EventuallyEq, eventually_nhds_iff]
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ (x : α), x ∈ t → 1 = ↑SignType.sign x) ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨{x | 0 < x}, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
refine' (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr _
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ (fun x => -1) =ᶠ[nhds a] ↑SignType.sign
[PROOFSTEP]
rw [Filter.EventuallyEq, eventually_nhds_iff]
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ (x : α), x ∈ t → -1 = ↑SignType.sign x) ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨{x | x < 0}, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩
[GOAL]
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
rcases h.lt_or_lt with (h_neg | h_pos)
[GOAL]
case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
exact continuousAt_sign_of_neg h_neg
[GOAL]
case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
exact continuousAt_sign_of_pos h_pos