awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α)
j : ↥S
h :
  Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j ≫
            colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
          f (↑j : Discrete α).as ⟶ 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) :
      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} (α := 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)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 α)
j : ↥S
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
      Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Discrete α))
          (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
            (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
        (↑j : Discrete α))
      (NatTrans.app (Cocone.ι (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f))))
        (↑j : Discrete α))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
          (colimit.isColimit (Discrete.functor f)))))
    (NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor f))) (↑j : Discrete α))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.ColimitCocone.isColimit, Subtype.val
-- 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 α)
j : ↥S
e_1 :
  (f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f) =
    (Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
      Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f)))
e_3 : f (↑j : Discrete α).as = Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α)
e_4 :
  colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) =
    Functor.obj.{w, v, w, u}
      (Functor.obj (Functor.const (Discrete α))
        (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
          (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
      (↑j : Discrete α)
⊢ {(↑j : Discrete α)} ≤ S

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
f : α → C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
inst_3 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
j : ↥S
e_1 :
  (f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f) =
    (Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
      Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f)))
e_3 : f (↑j : Discrete α).as = Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α)
e_4 :
  colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) =
    Functor.obj.{w, v, w, u}
      (Functor.obj (Functor.const (Discrete α))
        (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
          (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
      (↑j : Discrete α)
⊢ Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j ≫
        colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
      f (↑j : Discrete α).as ⟶ colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
    (NatTrans.app (Cocone.ι (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))) (↑j : Discrete α) :
      Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Discrete α))
            (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
              (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
          (↑j : Discrete α))

Tactic:
simp [← colimit.w (liftToFinsetObj _) (homOfLE (x := {j.1}) (y := S) (by simp))]

Premises used: CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj, CategoryTheory.homOfLE, CategoryTheory.Limits.colimit.w
-- 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 α)
j : ↥S
e_1 :
  (f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f) =
    (Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
      Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f)))
⊢ 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)
        (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
      f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor f))) (↑j : Discrete α) :
      Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Discrete α))
            (Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f))))
          (↑j : Discrete α))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete α) C

Tactic:
⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone, CategoryTheory.Limits.HasColimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete α) C

Tactic:
exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete α) C

Tactic:
classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w, w, v, u} C
⊢ HasColimitsOfSize.{w, w, v, u} C

Tactic:
have : HasCoproducts.{w} C := hasCoproducts_of_finite_and_filtered
  has_colimits_of_hasCoequalizers_and_coproducts

Premises used: CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts, CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasCofilteredLimitsOfSize.{w, w, v, u} C
⊢ HasProducts.{w, v, u} C

Tactic:
have : HasCoproducts.{w} Cᵒᵖ := hasCoproducts_of_finite_and_filtered
  hasProducts_of_opposite

Premises used: CategoryTheory.Limits.hasProducts_of_opposite, CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : HasCofilteredLimitsOfSize.{w, w, v, u} C
⊢ HasLimitsOfSize.{w, w, v, u} C

Tactic:
have : HasProducts.{w} C := hasProducts_of_finite_and_cofiltered
  has_limits_of_hasEqualizers_and_products

Premises used: CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products, CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered
-- 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
F : Functor.{w, v, w, u} (Discrete α) C
J : Finset (Discrete α)
j : ↥J
⊢ Eq (α := F.obj (↑j : Discrete α) ⟶ colimit F)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥J) ↦ F.obj (↑x : Discrete α)) j ≫
      colimit.ι (liftToFinsetObj F) J ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone F)))
    (colimit.ι F (↑j : Discrete α))

Tactic:
simp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
simp :
  Eq (α := colimit (Functor.obj (liftToFinset C α) X) ⟶ colimit Y)
    (colimMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y)))
    (CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
      (colimMap β))
⊢ Eq (α := Functor.obj (liftToFinset C α ⋙ colim) X ⟶ Functor.obj colim Y)
    (Functor.map (liftToFinset C α ⋙ colim) β ≫
      Iso.hom
        ((fun (F : Functor.{w, v, w, u} (Discrete α) C) ↦
            (Iso.symm (colimit.isoColimitCocone (liftToFinsetColimitCocone F)) :
              Functor.obj (liftToFinset C α ⋙ colim) F ≅ Functor.obj colim F))
          Y))
    (Iso.hom
        ((fun (F : Functor.{w, v, w, u} (Discrete α) C) ↦
            (Iso.symm (colimit.isoColimitCocone (liftToFinsetColimitCocone F)) :
              Functor.obj (liftToFinset C α ⋙ colim) F ≅ Functor.obj colim F))
          X) ≫
      Functor.map colim β)

Tactic:
simp only [Functor.comp_obj, colim_obj, Functor.comp_map, colim_map, Iso.symm_hom]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.colim_map, CategoryTheory.Limits.colim_obj, CategoryTheory.Functor.comp_map
-- 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
w :
  ∀ (J : Finset (Discrete α)),
    Eq (α := (Functor.obj (liftToFinset C α) X).obj J ⟶ colimit Y)
      (CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
        (colimit.ι (Functor.obj (liftToFinset C α) X) J)
        (colimMap (Functor.map (liftToFinset C α) β) ≫
          Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
      (colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
        CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
          (colimMap β))
⊢ Eq (α := colimit (Functor.obj (liftToFinset C α) X) ⟶ colimit Y)
    (colimMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y)))
    (CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
      (colimMap β))

Tactic:
ext 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
J : Finset (Discrete α)
w :
  Eq (α := (sigmaObj.{w, v, u} fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
      (colimit.ι (Functor.obj (liftToFinset C α) X) J)
      (colimMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
    (colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
      CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
        (colimMap β))
⊢ Eq (α := (Functor.obj (liftToFinset C α) X).obj J ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
      (colimit.ι (Functor.obj (liftToFinset C α) X) J)
      (colimMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
    (colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
      CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
        (colimMap β))

Tactic:
simp only [liftToFinset_obj_obj]

Premises used: CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj
-- 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
J : Finset (Discrete α)
w :
  ∀ (j : ↥J),
    Eq (α := X.obj (↑j : Discrete α) ⟶ colimit Y)
      (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) j ≫
        CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
          (colimit.ι (Functor.obj (liftToFinset C α) X) J)
          (colimMap (Functor.map (liftToFinset C α) β) ≫
            Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
      (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) j ≫
        colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
          CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
            (colimMap β))
⊢ Eq (α := (sigmaObj.{w, v, u} fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
      (colimit.ι (Functor.obj (liftToFinset C α) X) J)
      (colimMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
    (colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
      CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
        (colimMap β))

Tactic:
ext 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
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
J : Finset (Discrete α)
j : ↥J
⊢ Eq (α := X.obj (↑j : Discrete α) ⟶ colimit Y)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) j ≫
      CategoryStruct.comp (Y := colimit (Functor.obj (liftToFinset C α) X))
        (colimit.ι (Functor.obj (liftToFinset C α) X) J)
        (colimMap (Functor.map (liftToFinset C α) β) ≫
          Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone Y))))
    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥J) ↦ X.obj (↑x : Discrete α)) j ≫
      colimit.ι (Functor.obj (liftToFinset C α) X) J ≫
        CategoryStruct.comp (Y := colimit X) (Iso.inv (colimit.isoColimitCocone (liftToFinsetColimitCocone X)))
          (colimMap β))

Tactic:
simp [liftToFinset, liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc]

Premises used: CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
dsimp :
  Eq (α :=
    (sigmaObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) ⟶
      colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥I) ↦ Y.obj (↑x : Discrete α))
      (Sigma.map fun (x_1 : ↥I) ↦ x.app (↑x_1 : Discrete α))
      (Iso.hom
        (HasColimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (Y.obj (↑x.as : Discrete α))))))
    (CategoryStruct.comp (Y := colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ X))
      (Iso.hom (HasColimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (X.obj (↑x.as : Discrete α)))))
      (colimMap (Functor.whiskerLeft (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) x)))
⊢ Eq (α :=
    Functor.obj (liftToFinset C α ⋙ Functor.obj (evaluation (Finset (Discrete α)) C) I) X ⟶
      Functor.obj
        (Functor.comp (D := Functor.{w, v, w, u} (Discrete ↥I) C)
          (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
            (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
          colim)
        Y)
    (Functor.map (liftToFinset C α ⋙ Functor.obj (evaluation (Finset (Discrete α)) C) I) x ≫
      Iso.hom
        ((fun (x : Functor.{w, v, w, u} (Discrete α) C) ↦
            (HasColimit.isoOfNatIso
                (Discrete.natIso fun (x_1 : Discrete ↥I) ↦
                  Iso.refl
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (x_2 : ↥I) ↦ x.obj (↑x_2 : Discrete α)) x_1)) :
              colimit.{w, w, v, u} (J := Discrete ↥I) (Discrete.functor fun (x_1 : ↥I) ↦ x.obj (↑x_1 : Discrete α)) ≅
                colimit (J := Discrete ↥I)
                  (Functor.obj
                    (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
                      (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
                    x)))
          Y))
    (Iso.hom
        ((fun (x : Functor.{w, v, w, u} (Discrete α) C) ↦
            (HasColimit.isoOfNatIso
                (Discrete.natIso fun (x_1 : Discrete ↥I) ↦
                  Iso.refl
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (x_2 : ↥I) ↦ x.obj (↑x_2 : Discrete α)) x_1)) :
              colimit.{w, w, v, u} (J := Discrete ↥I) (Discrete.functor fun (x_1 : ↥I) ↦ x.obj (↑x_1 : Discrete α)) ≅
                colimit (J := Discrete ↥I)
                  (Functor.obj
                    (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
                      (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
                    x)))
          X) ≫
      Functor.map
        (Functor.comp (D := Functor.{w, v, w, u} (Discrete ↥I) C)
          (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
            (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
          colim)
        x)

Tactic:
dsimp