internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.epi_iff_surjective
Proof 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'⟩
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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'
Proof state after:
no goals
Theorem: ExtrDisc.epi_iff_surjective
Proof 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 _⟩
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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⟩
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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⟩
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof state after:
no goals
Theorem: ExtrDisc.epi_iff_surjective
Proof 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]
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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 =  _
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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]
Proof 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
Theorem: ExtrDisc.epi_iff_surjective
Proof 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]
Proof 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