[GOAL]
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
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 α
B✝ : Stonean
X : α → Stonean
B : Stonean
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 α
B✝ : Stonean
X : α → Stonean
B : Stonean
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 α
B✝ : Stonean
X : α → Stonean
B : Stonean
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 α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
specialize h a
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
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 α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
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 α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : Discrete α), NatTrans.app (cocone F).ι j ≫ m = NatTrans.app s.ι j
a : Discrete α
⊢ ι (fun a => F.obj a) a ≫ m = ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s
[PROOFSTEP]
specialize hm a
[GOAL]
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
hm : NatTrans.app (cocone F).ι a ≫ m = NatTrans.app s.ι a
⊢ ι (fun a => F.obj a) a ≫ m = ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s
[PROOFSTEP]
ext t
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
hm : NatTrans.app (cocone F).ι a ≫ m = NatTrans.app s.ι a
t : (forget Stonean).obj (F.obj a)
⊢ ↑(ι (fun a => F.obj a) a ≫ m) t =
    ↑(ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s) t
[PROOFSTEP]
apply_fun (fun q => q t) at hm 
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
t : (forget Stonean).obj (F.obj a)
hm : ↑(NatTrans.app (cocone F).ι a ≫ m) t = ↑(NatTrans.app s.ι a) t
⊢ ↑(ι (fun a => F.obj a) a ≫ m) t =
    ↑(ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s) t
[PROOFSTEP]
exact hm
