awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))
rw₁ :
  Eq (α := F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
          (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
        CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (leftToMax i₀ j))
          (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
rw₂ :
  Eq (α := F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫
          CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (leftToMax i₀ j))
            (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))) :
      F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
rw₃ rw₄ :
  Eq (α := F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    s.ι.app j

Tactic:
rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.rightToMax, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc, CategoryTheory.Limits.Cocone.w, CategoryTheory.IsFiltered.leftToMax
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
m : h.cocone.pt ⟶ s.pt
hm : ∀ (j : J), h.cocone.ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app i₀

Tactic:
simp only [← hm i₀, cocone_ι_app, coconeιApp_eq_id, id_comp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ι_app, CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
⊢ HasColimit F

Tactic:
⟨_, h.isColimitCocone⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitCocone, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
hc : IsColimit c
simp : IsIso (X := F.obj i₀) (Iso.inv (hc.coconePointUniqueUpToIso h.isColimitCocone) : h.cocone.pt ⟶ c.pt)
⊢ IsIso (c.ι.app i₀)

Tactic:
simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀,
    cocone_ι_app, coconeιApp_eq_id, id_comp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ι_app, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitCocone, CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
hc : IsColimit c
⊢ IsIso (X := F.obj i₀) (Iso.inv (hc.coconePointUniqueUpToIso h.isColimitCocone) : h.cocone.pt ⟶ c.pt)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
hc : IsColimit c
j : J
ι : i₀ ⟶ j
⊢ IsIso (c.ι.app j)

Tactic:
(h.postcomp ι).isIso_ι_of_isColimit hc

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.postcomp, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
inst_3 : IsIso (c.ι.app i₀)
refine : ∀ (j : J), h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
⊢ h.cocone ≅ c

Tactic:
refine Cocone.ext (asIso (c.ι.app i₀)) (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
inst_3 : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max.{v_1, u_1} i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
dsimp : h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
c : Cocone F
inst_3 : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max.{v_1, u_1} i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
rw : h.coconeιApp j ≫ F.map α ≫ c.ι.app i = c.ι.app j
rw₁ : h.coconeιApp j ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
rw₂ : (F.map β ≫ (h.isoMap α ⋯).inv) ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
rw₃ : F.map β ≫ (h.isoMap α ⋯).inv ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
rw₄ rw₅ : F.map β ≫ c.ι.app i = F.map β ≫ c.ι.app i
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j

Tactic:
rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq, CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsCofiltered.{v_1, u_1} J
obtain : ∀ (j : J) (h : F.IsEventuallyConstantTo j), HasLimit F
⊢ HasLimit F

Tactic:
obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantTo

Premises used: CategoryTheory.IsCofiltered.IsEventuallyConstant.exists_isEventuallyConstantTo
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsCofiltered.{v_1, u_1} J
j : J
h : F.IsEventuallyConstantTo j
⊢ HasLimit F

Tactic:
h.hasLimit

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsCofiltered.{v_1, u_1} J
j : J
h : F.IsEventuallyConstantTo j
⊢ HasLimit F

Tactic:
exact h.hasLimit

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsFiltered.{v_1, u_1} J
obtain : ∀ (j : J) (h : F.IsEventuallyConstantFrom j), HasColimit F
⊢ HasColimit F

Tactic:
obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantFrom

Premises used: CategoryTheory.IsFiltered.IsEventuallyConstant.exists_isEventuallyConstantFrom
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsFiltered.{v_1, u_1} J
j : J
h : F.IsEventuallyConstantFrom j
⊢ HasColimit F

Tactic:
h.hasColimit

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
hF : IsEventuallyConstant F
inst_2 : IsFiltered.{v_1, u_1} J
j : J
h : F.IsEventuallyConstantFrom j
⊢ HasColimit F

Tactic:
exact h.hasColimit

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
F : Functor.{w, v, w, u} (Discrete α) C
j : Discrete α
⊢ Membership.mem (γ := Finset (Discrete α)) {j} j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cocone F
m :
  Cocone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := colimit (liftToFinsetObj F),
        ι :=
          Discrete.natTrans fun (j : Discrete α) ↦
            CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
              (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
              (colimit.ι (liftToFinsetObj F) {j}) :
        Cocone F } ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          (Cocone.ι
            { pt := colimit (liftToFinsetObj F),
              ι :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
                    (colimit.ι (liftToFinsetObj F) {j}) })
          j ≫
        m =
      s.ι.app j
w :
  ∀ (j : Finset (Discrete α)),
    colimit.ι (liftToFinsetObj F) j ≫ m =
      CategoryStruct.comp (Y := colimit (liftToFinsetObj F)) (colimit.ι (liftToFinsetObj F) j)
        (colimit.desc (liftToFinsetObj F)
          { pt := s.pt,
            ι :=
              { app := fun (x : Finset (Discrete α)) ↦ Sigma.desc fun (x_1 : ↥x) ↦ s.ι.app (↑x_1 : Discrete α),
                naturality := ⋯ :
                NatTrans (liftToFinsetObj F) (Functor.obj (Functor.const (Finset (Discrete α))) s.pt) } })
⊢ m =
    colimit.desc (liftToFinsetObj F)
      { pt := s.pt,
        ι :=
          { app := fun (x : Finset (Discrete α)) ↦ Sigma.desc fun (x_1 : ↥x) ↦ s.ι.app (↑x_1 : Discrete α),
            naturality := ⋯ : NatTrans (liftToFinsetObj F) (Functor.obj (Functor.const (Finset (Discrete α))) s.pt) } }

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cocone F
m :
  Cocone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := colimit (liftToFinsetObj F),
        ι :=
          Discrete.natTrans fun (j : Discrete α) ↦
            CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
              (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
              (colimit.ι (liftToFinsetObj F) {j}) :
        Cocone F } ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          (Cocone.ι
            { pt := colimit (liftToFinsetObj F),
              ι :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
                    (colimit.ι (liftToFinsetObj F) {j}) })
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
⊢ NatTrans.app
        (Cocone.ι
          { pt := colimit (liftToFinsetObj F),
            ι :=
              Discrete.natTrans fun (j : Discrete α) ↦
                CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                  (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
                  (colimit.ι (liftToFinsetObj F) {j}) })
        j ≫
      m =
    s.ι.app j

Tactic:
h j
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cocone F
m :
  Cocone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := colimit (liftToFinsetObj F),
        ι :=
          Discrete.natTrans fun (j : Discrete α) ↦
            CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
              (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
              (colimit.ι (liftToFinsetObj F) {j}) :
        Cocone F } ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          (Cocone.ι
            { pt := colimit (liftToFinsetObj F),
              ι :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
                    (colimit.ι (liftToFinsetObj F) {j}) })
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1 :
  (Functor.obj.{w, v, w, u} (Discrete.functor fun (x : ↥t) ↦ F.obj (↑x : Discrete α))
        { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ t) j hj : Discrete ↥t } ⟶
      s.pt) =
    (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun (x : ↥t) ↦ F.obj (↑x : Discrete α))
        { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ t) j hj : Discrete ↥t } ≫
      colimit.ι
          { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
            map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
              Sigma.desc fun (y : ↥x) ↦
                Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                  (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
            map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α)) C }
          t ≫
        m =
    Sigma.ι.{w, v, u} (C := C) (fun (x : ↥t) ↦ F.obj (↑x : Discrete α))
        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ t) j ⋯) ≫
      colimit.ι (liftToFinsetObj F) t ≫ m

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
f : α → C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
inst_3 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
simp :
  Eq.{v + 1} (α := (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
          Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
            colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (Iso.hom
            (IsColimit.coconePointUniqueUpToIso
              (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
              (colimit.isColimit (Discrete.functor f))) :
          colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ sigmaObj.{w, v, u} f) :
      (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as :
      (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
      Cocone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubcoproductsCocone f))
    (CategoryStruct.comp (Y :=
        Cocone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f))
          (colimit.cocone (liftToFinsetObj (Discrete.functor f))))
        (NatTrans.app (Cocone.ι (colimit.cocone (liftToFinsetObj (Discrete.functor f)))) S)
        (Iso.hom
          (IsColimit.coconePointUniqueUpToIso (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
            (colimit.isColimit (Discrete.functor f)))) :
      Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
        Cocone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubcoproductsCocone f))
    (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone f)) S :
      Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Finset (Discrete α)))
            (Cocone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubcoproductsCocone f)))
          S)

Tactic:
simp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
      colimit.cocone_x, colimit.cocone_ι, finiteSubcoproductsCocone_ι_app]

Premises used: CategoryTheory.Limits.colimit.cocone_ι, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app, CategoryTheory.Limits.colimit.cocone_x
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
f : α → C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
inst_3 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
h :
  ∀ (j : ↥S),
    Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j :
            f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (CategoryStruct.comp (Y := colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
              (colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
                Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
                  colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
              (Iso.hom
                  (IsColimit.coconePointUniqueUpToIso
                    (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
                    (colimit.isColimit (Discrete.functor f))) :
                colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ sigmaObj.{w, v, u} f) :
            (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f) :
        f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j)
          (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
        f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
⊢ Eq.{v + 1} (α := (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
          Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
            colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (Iso.hom
            (IsColimit.coconePointUniqueUpToIso
              (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
              (colimit.isColimit (Discrete.functor f))) :
          colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ sigmaObj.{w, v, u} f) :
      (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as :
      (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)

Tactic:
ext j