[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
j : Discrete α
⊢ j ∈ {j}
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ m =
    (fun s =>
        colimit.desc (liftToFinset F) { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
      s
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ ∀ (j : Finset (Discrete α)),
    colimit.ι (liftToFinset F) j ≫ m =
      colimit.ι (liftToFinset F) j ≫
        (fun s =>
            colimit.desc (liftToFinset F)
              { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
          s
[PROOFSTEP]
rintro t
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ colimit.ι (liftToFinset F) t ≫ m =
    colimit.ι (liftToFinset F) t ≫
      (fun s =>
          colimit.desc (liftToFinset F)
            { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x })
        s
[PROOFSTEP]
dsimp [liftToFinset]
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ colimit.ι
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        t ≫
      m =
    colimit.ι
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        t ≫
      colimit.desc
        (Functor.mk
          { obj := fun s => ∐ fun x => F.obj ↑x,
            map := fun {x Y} h =>
              Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
        { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w.w
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
⊢ ∀ (j : Discrete { x // x ∈ t }),
    colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫
        colimit.ι
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            t ≫
          m =
      colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫
        colimit.ι
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            t ≫
          colimit.desc
            (Functor.mk
              { obj := fun s => ∐ fun x => F.obj ↑x,
                map := fun {x Y} h =>
                  Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
            { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
rintro ⟨⟨j, hj⟩⟩
[GOAL]
case w.w.mk.mk
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        colimit.desc
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x }
[PROOFSTEP]
convert h j using 1
[GOAL]
case h.e'_2.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    NatTrans.app
        { pt := colimit (liftToFinset F),
            ι :=
              Discrete.natTrans fun j =>
                Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.ι
        j ≫
      m
[PROOFSTEP]
simp [← colimit.w (liftToFinset F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
[GOAL]
case h.e'_2.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        m =
    Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : ↑{ val := j, property := (_ : j ∈ {j}) } ∈ t) } ≫
      colimit.ι (liftToFinset F) t ≫ m
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinset F),
        ι :=
          Discrete.natTrans fun j =>
            Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          { pt := colimit (liftToFinset F),
              ι :=
                Discrete.natTrans fun j =>
                  Sigma.ι (fun x => F.obj ↑x) { val := j, property := (_ : j ∈ {j}) } ≫
                    colimit.ι (liftToFinset F) {j} }.ι
          j ≫
        m =
      NatTrans.app s.ι j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x => F.obj ↑x).obj { as := { val := j, property := hj } } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x => F.obj ↑x) { as := { val := j, property := hj } } ≫
      colimit.ι
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          t ≫
        colimit.desc
          (Functor.mk
            { obj := fun s => ∐ fun x => F.obj ↑x,
              map := fun {x Y} h =>
                Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) { val := ↑y, property := (_ : ↑y ∈ Y) } })
          { pt := s.pt, ι := NatTrans.mk fun t => Sigma.desc fun x => NatTrans.app s.ι ↑x } =
    NatTrans.app s.ι j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α✝ : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C
[PROOFSTEP]
classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
α✝ : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C
[PROOFSTEP]
exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩
