[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ fst f g ≫ f = snd f g ≫ g
[PROOFSTEP]
ext ⟨_, h⟩
[GOAL]
case w.mk
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
val✝ : ↑X.toTop × ↑Y.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
[PROOFSTEP]
exact h
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : ↑Z.toTop
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
apply_fun (fun q => q z) at w 
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
z : ↑Z.toTop
w : ↑(a ≫ f) z = ↑(b ≫ g) z
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
exact w
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun z => { val := (↑a z, ↑b z), property := (_ : ↑(a ≫ f) z = ↑(b ≫ g) z) }
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun x => (↑a x, ↑b x)
[PROOFSTEP]
rw [continuous_prod_mk]
[GOAL]
case h
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ (Continuous fun x => ↑a x) ∧ Continuous fun x => ↑b x
[PROOFSTEP]
exact ⟨a.continuous, b.continuous⟩
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b
[PROOFSTEP]
ext z
[GOAL]
case w
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget CompHaus).obj Z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply_fun (fun q => q z) at hfst hsnd 
[GOAL]
case w
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case w.a
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
[PROOFSTEP]
apply Prod.ext
[GOAL]
case w.a.h₁
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst
[PROOFSTEP]
exact hfst
[GOAL]
case w.a.h₂
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
[PROOFSTEP]
exact hsnd
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.fst
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.fst
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.snd
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.snd
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
intro a
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
exact (e a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
[PROOFSTEP]
ext ⟨a, x⟩
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
specialize h a
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
apply_fun (fun q => q x) at h 
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), NatTrans.app (cocone X).ι j ≫ m = NatTrans.app s.ι j
a : α
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
specialize hm ⟨a⟩
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
ext t
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
t : (forget CompHaus).obj (X a)
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
apply_fun (fun q => q t) at hm 
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
t : (forget CompHaus).obj (X a)
hm : ↑(NatTrans.app (cocone X).ι { as := a } ≫ m) t = ↑(NatTrans.app s.ι { as := a }) t
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
exact hm
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Limits.Sigma.ι X a ≫ (coproductIsoCoproduct X).inv = finiteCoproduct.ι X a
[PROOFSTEP]
dsimp [coproductIsoCoproduct]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Limits.Sigma.ι X a ≫
      (Limits.IsColimit.coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
          (Limits.colimit.isColimit (Discrete.functor X))).inv =
    finiteCoproduct.ι X a
[PROOFSTEP]
simp only [Limits.colimit.comp_coconePointUniqueUpToIso_inv, finiteCoproduct.cocone_pt, finiteCoproduct.cocone_ι,
  Discrete.natTrans_app]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Function.Injective ↑(ι X a)
[PROOFSTEP]
intro x y hxy
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
x y : (forget CompHaus).obj (X a)
hxy : ↑(ι X a) x = ↑(ι X a) y
⊢ x = y
[PROOFSTEP]
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (forget CompHaus).obj (X a)), ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
intro x
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
x : (forget CompHaus).obj (X a)
⊢ ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
change (ι X a ≫ desc X π) _ = _
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
x : (forget CompHaus).obj (X a)
⊢ ↑(ι X a ≫ desc X π) x = ↑(π a) x
[PROOFSTEP]
simp only [ι_desc]
  -- `elementwise` should work here, but doesn't
