awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := 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 β))
have 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 β))
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
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 α)
⊢ 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 β))
have 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 β))
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
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
⊢ 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)
have 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)))
Tactic: dsimp
-- 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
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ 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)))
have 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))
Tactic: 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 : 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
⊢ 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 := ⋯ } }
have 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 := sorry } })
      (limit.π (liftToFinsetObj F) j)
Tactic: apply limit.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 : 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 α))ᵒᵖ
⊢ 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))
have 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))
Tactic: simp only [limit.cone_x, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
      limit.cone_π, finiteSubproductsCone_pt, finiteSubproductsCone_π_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 : 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 α))ᵒᵖ
⊢ 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))
have 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))
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 : 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)) ⟶
      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))
have 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 α) sorry))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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
⊢ 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 β)
have 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 β))
Tactic: simp only [Functor.comp_obj, lim_obj, Functor.comp_map, lim_map, Iso.symm_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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
⊢ 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 β))
have 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)
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 : HasFiniteProducts.{v, u} C
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
⊢ 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)))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → c₂.pt ⟶ f b
have refine_1 : c₂.pt ⟶ f 0
Tactic: refine Fin.cases ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
refine_1 : c₂.pt ⟶ f 0
⊢ (b : Fin (n + 1)) → c₂.pt ⟶ f b
have refine_2 : (i : Fin n) → c₂.pt ⟶ f i.succ
Tactic: refine Fin.cases ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone.{0, v, 0, u} (Discrete.functor f)
⊢ s.pt ⟶ (extendFan c₁ c₂).pt
have apply : Functor.obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
    { as := 0 : Discrete (Fin (n + 1)) } ⟶
  c₁.pt
Tactic: apply (BinaryFan.IsLimit.lift' t₂ (s.π.app ⟨0⟩) _).1