Theorem: ExtrDisc.epi_iff_surjective (ExtrDisc/Epi.lean)

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f

case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f

State before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f
Tactic:
dsimp [Function.Surjective]
State after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → ∀ (b : CoeSort.coe Y), ∃ a, ↑f a = b

State before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → ∀ (b : CoeSort.coe Y), ∃ a, ↑f a = b
Tactic:
contrapose!
State after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ (∃ b, ∀ (a : CoeSort.coe X), ↑f a ≠ b) → ¬Epi f

State before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ (∃ b, ∀ (a : CoeSort.coe X), ↑f a ≠ b) → ¬Epi f
Tactic:
rintro ⟨y,hy⟩ h
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
⊢ False
Tactic:
let C := Set.range f
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
⊢ False
Tactic:
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
⊢ False
Tactic:
let U := Cᶜ
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ False
Tactic:
have hyU : y ∈ U := by
  refine' Set.mem_compl _
  rintro ⟨y', hy'⟩
  exact hy y' hy'
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
⊢ False
Tactic:
have hUy : U ∈ nhds y := hC.compl_mem_nhds hyU
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
⊢ False
Tactic:
haveI : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y)) :=
  show TotallyDisconnectedSpace Y from inferInstance
State after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
⊢ False

State before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
⊢ False
Tactic:
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Tactic:
classical
let g : Y ⟶ ExtrDisc.two :=
  ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ ExtrDisc.two := ⟨fun _ => ⟨1⟩, continuous_const⟩
have H : h = g := by
  rw [← cancel_epi f]
  apply ContinuousMap.ext ; intro x
  apply ULift.ext
  change 1 =  _
  dsimp [LocallyConstant.ofClopen]
  rw [comp_apply, @ContinuousMap.coe_mk _ _ (ExtrDisc.instTopologicalSpace Y),
  Function.comp_apply, if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
  exact ⟨x, rfl⟩
apply_fun fun e => (e y).down at H
dsimp [LocallyConstant.ofClopen] at H
change 1 = ite _ _ _ at H
rw [if_pos hyV] at H
exact top_ne_bot H
State after:
no goals

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ y ∈ U
Tactic:
refine' Set.mem_compl _
State after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ ¬y ∈ C

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ ¬y ∈ C
Tactic:
rintro ⟨y', hy'⟩
State after:
case intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
y' : CoeSort.coe X
hy' : ↑f y' = y
⊢ False

State before:
case intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
y' : CoeSort.coe X
hy' : ↑f y' = y
⊢ False
Tactic:
exact hy y' hy'
State after:
no goals

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Tactic:
let g : Y ⟶ ExtrDisc.two :=
  ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
⊢ False
Tactic:
let h : Y ⟶ ExtrDisc.two := ⟨fun _ => ⟨1⟩, continuous_const⟩
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ False
Tactic:
have H : h = g := by
  rw [← cancel_epi f]
  apply ContinuousMap.ext ; intro x
  apply ULift.ext
  change 1 =  _
  dsimp [LocallyConstant.ofClopen]
  rw [comp_apply, @ContinuousMap.coe_mk _ _ (ExtrDisc.instTopologicalSpace Y),
  Function.comp_apply, if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
  exact ⟨x, rfl⟩
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : h = g
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : h = g
⊢ False
Tactic:
apply_fun fun e => (e y).down at H
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : (↑h y).down = (↑g y).down
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : (↑h y).down = (↑g y).down
⊢ False
Tactic:
dsimp [LocallyConstant.ofClopen] at H
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H :
  (↑(ContinuousMap.mk fun x => { down := 1 }) y).down =
    (↑(ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) y).down
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H :
  (↑(ContinuousMap.mk fun x => { down := 1 }) y).down =
    (↑(ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) y).down
⊢ False
Tactic:
change 1 = ite _ _ _ at H
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : 1 = if y ∈ V then 0 else 1
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : 1 = if y ∈ V then 0 else 1
⊢ False
Tactic:
rw [if_pos hyV] at H
State after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : 1 = 0
⊢ False

State before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
H : 1 = 0
⊢ False
Tactic:
exact top_ne_bot H
State after:
no goals

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ h = g
Tactic:
rw [← cancel_epi f]
State after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ f ≫ h = f ≫ g

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ f ≫ h = f ≫ g
Tactic:
apply ContinuousMap.ext
State after:
case h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ ∀ (a : ↑((fun x => x.compHaus) X).toTop), ↑(f ≫ h) a = ↑(f ≫ g) a

State before:
case h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
⊢ ∀ (a : ↑((fun x => x.compHaus) X).toTop), ↑(f ≫ h) a = ↑(f ≫ g) a
Tactic:
intro x
State after:
case h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ↑(f ≫ h) x = ↑(f ≫ g) x

State before:
case h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ↑(f ≫ h) x = ↑(f ≫ g) x
Tactic:
apply ULift.ext
State after:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ (↑(f ≫ h) x).down = (↑(f ≫ g) x).down

State before:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ (↑(f ≫ h) x).down = (↑(f ≫ g) x).down
Tactic:
change 1 =  _
State after:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ 1 = (↑(f ≫ g) x).down

State before:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ 1 = (↑(f ≫ g) x).down
Tactic:
dsimp [LocallyConstant.ofClopen]
State after:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ 1 = (↑(f ≫ ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) x).down

State before:
case h.h
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ 1 = (↑(f ≫ ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) x).down
Tactic:
rw [comp_apply, @ContinuousMap.coe_mk _ _ (ExtrDisc.instTopologicalSpace Y),
Function.comp_apply, if_neg]
State after:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ V

State before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ V
Tactic:
refine' mt (fun α => hVU α) _
State after:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ U

State before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ U
Tactic:
simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
State after:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ∃ y, ↑f y = ↑f x

State before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ∃ y, ↑f y = ↑f x
Tactic:
exact ⟨x, rfl⟩
State after:
no goals

State before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f
Tactic:
intro (h : Function.Surjective (toCompHaus.map f))
State after:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Function.Surjective ↑(toCompHaus.map f)
⊢ Epi f

State before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Function.Surjective ↑(toCompHaus.map f)
⊢ Epi f
Tactic:
rw [← CompHaus.epi_iff_surjective] at h
State after:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ Epi f

State before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ Epi f
Tactic:
constructor
State after:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ ∀ {Z : ExtrDisc} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

State before:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ ∀ {Z : ExtrDisc} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Tactic:
intro W a b h
State after:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ a = b

State before:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ a = b
Tactic:
apply Functor.map_injective toCompHaus
State after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ toCompHaus.map a = toCompHaus.map b

State before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
apply_fun toCompHaus.map at h
State after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map (f ≫ a) = toCompHaus.map (f ≫ b)
⊢ toCompHaus.map a = toCompHaus.map b

State before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map (f ≫ a) = toCompHaus.map (f ≫ b)
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
simp only [Functor.map_comp] at h
State after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map f ≫ toCompHaus.map a = toCompHaus.map f ≫ toCompHaus.map b
⊢ toCompHaus.map a = toCompHaus.map b

State before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map f ≫ toCompHaus.map a = toCompHaus.map f ≫ toCompHaus.map b
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
rwa [← cancel_epi (toCompHaus.map f)]
State after:
no goals