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
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
h :
  ∀ (b : ↥I),
    Eq (α :=
      X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α))
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) b)
          (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 α)))))) :
        X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α))
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) b)
          (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))) :
        X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
⊢ 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)))

Tactic:
ext
-- 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
b : ↥I
⊢ Eq (α :=
    X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α))
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) b)
        (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 α)))))) :
      X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α))
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) b)
        (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))) :
      X.obj (↑b : Discrete α) ⟶ colimit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{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 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cone F
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := limit (liftToFinsetObj F),
        π :=
          Discrete.natTrans fun (j : Discrete α) ↦
            limit.π (liftToFinsetObj F) (op {j}) ≫
              Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) }
h :
  ∀ (j : Discrete α),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := limit (liftToFinsetObj F),
              π :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  limit.π (liftToFinsetObj F) (op {j}) ≫
                    Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) })
          j =
      s.π.app j
w :
  ∀ (j : (Finset (Discrete α))ᵒᵖ),
    m ≫ limit.π (liftToFinsetObj F) j =
      CategoryStruct.comp (Y := limit (liftToFinsetObj F))
        (limit.lift (liftToFinsetObj F)
          { pt := s.pt,
            π :=
              { app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦ Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
                naturality := ⋯ } })
        (limit.π (liftToFinsetObj F) j)
⊢ m =
    limit.lift (liftToFinsetObj F)
      { pt := s.pt,
        π :=
          { app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦ Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
            naturality := ⋯ } }

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cone F
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := limit (liftToFinsetObj F),
        π :=
          Discrete.natTrans fun (j : Discrete α) ↦
            limit.π (liftToFinsetObj F) (op {j}) ≫
              Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) }
h :
  ∀ (j : Discrete α),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := limit (liftToFinsetObj F),
              π :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  limit.π (liftToFinsetObj F) (op {j}) ≫
                    Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) })
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
⊢ m ≫
      NatTrans.app
        (Cone.π
          { pt := limit (liftToFinsetObj F),
            π :=
              Discrete.natTrans fun (j : Discrete α) ↦
                limit.π (liftToFinsetObj F) (op {j}) ≫
                  Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) })
        j =
    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 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cone F
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := limit (liftToFinsetObj F),
        π :=
          Discrete.natTrans fun (j : Discrete α) ↦
            limit.π (liftToFinsetObj F) (op {j}) ≫
              Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) }
h :
  ∀ (j : Discrete α),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := limit (liftToFinsetObj F),
              π :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  limit.π (liftToFinsetObj F) (op {j}) ≫
                    Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) })
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1 :
  (s.pt ⟶
      Functor.obj.{w, v, w, u} (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
        { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j hj : Discrete ↥(unop t) }) =
    (s.pt ⟶ F.obj j)
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫
        limit.π
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C }
            t ≫
          limit.π (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
            { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j hj } :
      s.pt ⟶ F.obj j)
    (m ≫
        limit.π (liftToFinsetObj F) t ≫
          Pi.π (fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
            (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j ⋯) :
      s.pt ⟶ F.obj j)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
f : α → C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
simp :
  Eq.{v + 1} (α :=
    limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶
      piObj.{w, v, u} fun (x : ↥(unop S)) ↦ f (↑x : Discrete α).as)
    (limit.π (liftToFinsetObj (Discrete.functor f)) S)
    (CategoryStruct.comp (Y := piObj.{w, v, u} f)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (LimitCone.isLimit (liftToFinsetLimitCone (Discrete.functor f)))
          (limit.isLimit (Discrete.functor f))))
      (Pi.lift fun (s : ↥(unop S)) ↦ Pi.π f (↑s : Discrete α).as))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ)
          (Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f))
            (limit.cone (liftToFinsetObj (Discrete.functor f)))))
        S ⟶
      Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S)
    (NatTrans.app (Cone.π (limit.cone (liftToFinsetObj (Discrete.functor f)))) S)
    (CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubproductsCone f))
      (Iso.hom
          (IsLimit.conePointUniqueUpToIso (LimitCone.isLimit (liftToFinsetLimitCone (Discrete.functor f)))
            (limit.isLimit (Discrete.functor f))) :
        Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f))
            (limit.cone (liftToFinsetObj (Discrete.functor f))) ⟶
          Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubproductsCone f))
      (NatTrans.app (Cone.π (finiteSubproductsCone f)) S :
        Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ)
              (Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubproductsCone f)))
            S ⟶
          Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S))

Tactic:
simp only [limit.cone_x, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
      limit.cone_π, finiteSubproductsCone_pt, finiteSubproductsCone_π_app]

Premises used: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, CategoryTheory.Limits.limit.cone_x, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt, CategoryTheory.Limits.limit.cone_π, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
f : α → C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
h :
  ∀ (j : ↥(unop S)),
    Eq.{v + 1} (α :=
      limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶
        Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α))
      (limit.π (liftToFinsetObj (Discrete.functor f)) S ≫
        Pi.π (fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α)) j)
      (CategoryStruct.comp (Y :=
        piObj.{w, v, u} fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α))
        (CategoryStruct.comp (Y := piObj.{w, v, u} f)
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (LimitCone.isLimit (liftToFinsetLimitCone (Discrete.functor f)))
              (limit.isLimit (Discrete.functor f))))
          (Pi.lift fun (s : ↥(unop S)) ↦ Pi.π f (↑s : Discrete α).as))
        (Pi.π (fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α)) j))
⊢ Eq.{v + 1} (α :=
    limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶
      piObj.{w, v, u} fun (x : ↥(unop S)) ↦ f (↑x : Discrete α).as)
    (limit.π (liftToFinsetObj (Discrete.functor f)) S)
    (CategoryStruct.comp (Y := piObj.{w, v, u} f)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (LimitCone.isLimit (liftToFinsetLimitCone (Discrete.functor f)))
          (limit.isLimit (Discrete.functor f))))
      (Pi.lift fun (s : ↥(unop S)) ↦ Pi.π f (↑s : Discrete α).as))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
f : α → C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
j : ↥(unop S)
h :
  Eq.{v + 1} (α := limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ f (↑j : Discrete α).as)
    (limit.π (liftToFinsetObj (Discrete.functor f)) S ≫ Pi.π (fun (x : ↥(unop S)) ↦ f (↑x : Discrete α).as) j)
    (limit.π (liftToFinsetObj (Discrete.functor f)) (op {(↑j : Discrete α)}) ≫
      Pi.π (fun (x : ↥{(↑j : Discrete α)}) ↦ f (↑x : Discrete α).as)
        (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {(↑j : Discrete α)} x)
          (↑j : Discrete α) ⋯))
⊢ Eq.{v + 1} (α :=
    limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶
      Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α))
    (limit.π (liftToFinsetObj (Discrete.functor f)) S ≫
      Pi.π (fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α)) j)
    (CategoryStruct.comp (Y :=
      piObj.{w, v, u} fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α))
      (CategoryStruct.comp (Y := piObj.{w, v, u} f)
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (LimitCone.isLimit (liftToFinsetLimitCone (Discrete.functor f)))
            (limit.isLimit (Discrete.functor f))))
        (Pi.lift fun (s : ↥(unop S)) ↦ Pi.π f (↑s : Discrete α).as))
      (Pi.π (fun (x : ↥(unop S)) ↦ Functor.obj.{w, v, w, u} (Discrete.functor f) (↑x : Discrete α)) j))

Tactic:
simp only [Discrete.functor_obj_eq_as, Category.assoc, limit.lift_π, Fan.mk_pt, Fan.mk_π_app,
      limit.conePointUniqueUpToIso_hom_comp, liftToFinsetLimitCone_cone_pt, Discrete.mk_as,
      liftToFinsetLimitCone_cone_π_app]

Premises used: CategoryTheory.Discrete.mk_as, CategoryTheory.Category.assoc, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
f : α → C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
j : ↥(unop S)
⊢ {(↑j : Discrete α)} ≤ unop S

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
f : α → C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
j : ↥(unop S)
⊢ Eq.{v + 1} (α := limit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ f (↑j : Discrete α).as)
    (limit.π (liftToFinsetObj (Discrete.functor f)) S ≫ Pi.π (fun (x : ↥(unop S)) ↦ f (↑x : Discrete α).as) j)
    (limit.π (liftToFinsetObj (Discrete.functor f)) (op {(↑j : Discrete α)}) ≫
      Pi.π (fun (x : ↥{(↑j : Discrete α)}) ↦ f (↑x : Discrete α).as)
        (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {(↑j : Discrete α)} x)
          (↑j : Discrete α) ⋯))

Tactic:
simp [← limit.w (liftToFinsetObj _)
      (Quiver.Hom.op (homOfLE (x := {j.1}) (y := S.unop) (by simp)))]

Premises used: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj, Quiver.Hom.op, CategoryTheory.homOfLE, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
simp :
  Eq (α := limit (Functor.obj (liftToFinset C α) X) ⟶ limit Y)
    (limMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone Y)))
    (CategoryStruct.comp (Y := limit X) (Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone X))) (limMap β))
⊢ Eq (α := Functor.obj (liftToFinset C α ⋙ lim) X ⟶ Functor.obj lim Y)
    (Functor.map (liftToFinset C α ⋙ lim) β ≫
      Iso.hom
        ((fun (F : Functor.{w, v, w, u} (Discrete α) C) ↦
            (Iso.symm (limit.isoLimitCone (liftToFinsetLimitCone F)) :
              Functor.obj (liftToFinset C α ⋙ lim) F ≅ Functor.obj lim F))
          Y))
    (Iso.hom
        ((fun (F : Functor.{w, v, w, u} (Discrete α) C) ↦
            (Iso.symm (limit.isoLimitCone (liftToFinsetLimitCone F)) :
              Functor.obj (liftToFinset C α ⋙ lim) F ≅ Functor.obj lim F))
          X) ≫
      Functor.map lim β)

Tactic:
simp only [Functor.comp_obj, lim_obj, Functor.comp_map, lim_map, Iso.symm_hom]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.lim_map, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.lim_obj, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
w :
  ∀ (J : Discrete α),
    CategoryStruct.comp (Y := limit Y)
        (limMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone Y)))
        (limit.π Y J) =
      CategoryStruct.comp (Y := limit Y)
        (CategoryStruct.comp (Y := limit X) (Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone X))) (limMap β))
        (limit.π Y J)
⊢ Eq (α := limit (Functor.obj (liftToFinset C α) X) ⟶ limit Y)
    (limMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone Y)))
    (CategoryStruct.comp (Y := limit X) (Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone X))) (limMap β))

Tactic:
ext J
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete α) C
X Y : Functor.{w, v, w, u} (Discrete α) C
β : X ⟶ Y
J : Discrete α
⊢ CategoryStruct.comp (Y := limit Y)
      (limMap (Functor.map (liftToFinset C α) β) ≫ Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone Y)))
      (limit.π Y J) =
    CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit X) (Iso.inv (limit.isoLimitCone (liftToFinsetLimitCone X))) (limMap β))
      (limit.π Y J)

Tactic:
simp [liftToFinset]

Premises used: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
w :
  ∀ (j : Discrete ↥I),
    Eq (α :=
      (piObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) ⟶
        Functor.obj ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j)
      (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
        (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥I) ↦ Y.obj (↑x : Discrete α))
          (Pi.map fun (x_1 : ↥I) ↦ x.app (↑x_1 : Discrete α))
          (Iso.hom
            (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (Y.obj (↑x.as : Discrete α))))))
        (limit.π ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j))
      (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
        (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ X))
          (Iso.hom
            (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (X.obj (↑x.as : Discrete α)))))
          (limMap (Functor.whiskerLeft (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) x)))
        (limit.π ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j))
⊢ Eq (α :=
    (piObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) ⟶
      limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥I) ↦ Y.obj (↑x : Discrete α))
      (Pi.map fun (x_1 : ↥I) ↦ x.app (↑x_1 : Discrete α))
      (Iso.hom (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (Y.obj (↑x.as : Discrete α))))))
    (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ X))
      (Iso.hom (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (X.obj (↑x.as : Discrete α)))))
      (limMap (Functor.whiskerLeft (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) x)))

Tactic:
ext