awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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)
⊢ 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
have 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)
Tactic: rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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 (c.ι.app i₀)
have simp : IsIso (X := F.obj i₀) (Iso.inv (hc.coconePointUniqueUpToIso h.isColimitCocone) : h.cocone.pt ⟶ c.pt)
Tactic: simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀,
    cocone_ι_app, coconeιApp_eq_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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₀)
⊢ h.cocone ≅ c
have refine : ∀ (j : J), h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
Tactic: refine Cocone.ext (asIso (c.ι.app i₀)) (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
have dsimp : h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
have rw : h.coconeιApp j ≫ F.map α ≫ c.ι.app i = c.ι.app j
Tactic: rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
have rw₁ : h.coconeιApp j ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Tactic: rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
have rw₂ : (F.map β ≫ (h.isoMap α sorry).inv) ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Tactic: rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
have rw₃ : F.map β ≫ (h.isoMap α sorry).inv ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Tactic: rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j
have rw₄ : F.map β ≫ c.ι.app i = F.map β ≫ c.ι.app i
Tactic: rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ HasLimit F
have obtain : ∀ (j : J) (h : F.IsEventuallyConstantTo j), HasLimit F
Tactic: obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantTo
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ HasColimit F
have obtain : ∀ (j : J) (h : F.IsEventuallyConstantFrom j), HasColimit F
Tactic: obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantFrom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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
⊢ 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) } }
have 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 := sorry :
              NatTrans (liftToFinsetObj F) (Functor.obj (Functor.const (Finset (Discrete α))) s.pt) } })
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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 α)
⊢ 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)
have 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)
Tactic: simp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
      colimit.cocone_x, colimit.cocone_ι, finiteSubcoproductsCocone_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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 α)
⊢ 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)
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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} (α := 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)
have 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)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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} (α := 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)
have h : (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))) →
  f (↑j : Discrete α).as = Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) →
    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: convert!
      IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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
⊢ 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 β)
have 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 β))
Tactic: simp only [Functor.comp_obj, colim_obj, Functor.comp_map, colim_map, Iso.symm_hom]