awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this :
  Eq (α := (Opposite.unop (limit K) ⟶ i.left) ⟶ A.obj (K.obj j))
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)) (i.hom.app (limit K) ≫ A.map (limit.π K j))
⊢ Eq (α := obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶ (K ⋙ A).obj j)
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j))
    (NatTrans.app
        (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) i ≫
      CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
        ((fun (X : CostructuredArrow yoneda A) ↦
            (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
              (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
          i)
        (NatTrans.app
            (Functor.map
              (coyoneda ⋙
                obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
              (limit.π K j))
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j))
have h : ∀ (x : Opposite.unop (limit K) ⟶ i.left),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)))
      x =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
            (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K))))
            i ≫
          CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
            ((fun (X : CostructuredArrow yoneda A) ↦
                (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
                  (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
              i)
            (NatTrans.app
                (Functor.map
                  (coyoneda ⋙
                    obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
                  (limit.π K j))
                i ≫
              ((functorToInterchangeIso A K).inv.app j).app i ≫
                ((flipFunctorToInterchange A K).hom.app i).app j ≫
                  (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ Eq (α := F.obj X ⟶ Abelian.image (F.map f))
    (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (Abelian.factorThruImage f)) (Iso.hom (iso F f)))
    (Abelian.factorThruImage (F.map f))
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
    (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (Abelian.factorThruImage f)) (Iso.hom (iso F f)))
    (equalizer.ι (cokernel.π (F.map f)) 0) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
    (Abelian.factorThruImage (F.map f)) (equalizer.ι (cokernel.π (F.map f)) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := Abelian.coimage (F.map f) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (Iso.inv (iso F f)) (F.map (Abelian.factorThruCoimage f)))
    (Abelian.factorThruCoimage (F.map f))
have h : CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
    (coequalizer.π (kernel.ι (F.map f)) 0)
    (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (Iso.inv (iso F f)) (F.map (Abelian.factorThruCoimage f))) =
  CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
    (coequalizer.π (kernel.ι (F.map f)) 0) (Abelian.factorThruCoimage (F.map f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G
have apply : IsLimit (F := pair X Y ⋙ G) (G.mapCone (BinaryFan.mk (P := prod.{v₁, u₁} X Y) prod.fst prod.snd))
Tactic: apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
⊢ IsLimit (F := pair X Y ⋙ G) (G.mapCone (BinaryFan.mk (P := prod.{v₁, u₁} X Y) prod.fst prod.snd))
have apply : IsLimit (F := pair (G.obj X) (G.obj Y))
  (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd))
Tactic: apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
⊢ IsLimit (F := pair (G.obj X) (G.obj Y))
    (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd))
have refine : IsIso (X :=
  Cone.pt (F := pair (G.obj X) (G.obj Y))
    (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))
  (Y := Cone.pt.{0, v₂, 0, u₂} (F := pair (G.obj X) (G.obj Y)) (limit.cone (pair (G.obj X) (G.obj Y))))
  (IsLimit.lift (limit.isLimit (pair (G.obj X) (G.obj Y)))
    (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))
Tactic: refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ Eq (α := prod.{v₂, u₂} (G.obj X) (G.obj Y) ⟶ G.obj X)
    (CategoryStruct.comp (Y := G.obj (prod.{v₁, u₁} X Y)) (Iso.inv (iso G X Y)) (G.map prod.fst)) prod.fst
have rw : 𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.fst =
  CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.fst
Tactic: rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ Eq (α := prod.{v₂, u₂} (G.obj X) (G.obj Y) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (prod.{v₁, u₁} X Y)) (Iso.inv (iso G X Y)) (G.map prod.snd)) prod.snd
have rw : 𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.snd =
  CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.snd
Tactic: rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasBinaryProducts.{v₂, u₂} D
i : ∀ {X Y : C}, IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
⊢ PreservesLimit K G
have this : PreservesLimit
  (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
    (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
  G
Tactic: have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesLimitPair.of_iso_prod_comparison ..
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₂, u₂} D
i :
  ∀ {X Y : C},
    IsIso (X := coprod.{v₂, u₂} (G.obj X) (G.obj Y)) (Y := G.obj (coprod.{v₁, u₁} X Y)) (coprodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
⊢ PreservesColimit K G
have this : PreservesColimit
  (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
    (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
  G
Tactic: have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
⊢ F.map (b.ι j) ≫ F.map (b.π j') = if h : j = j' then eqToHom ⋯ else 0
have rw : F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom sorry else 0
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
have pos : ∀ (h : j = j'), F.map (b.ι j ≫ b.π j') = eqToHom sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
pos : ∀ (h : j = j'), F.map (b.ι j ≫ b.π j') = eqToHom ⋯
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
have neg : ∀ (h : ¬j = j'), F.map (b.ι j ≫ b.π j') = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
h : j = j'
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯
have pos : F.map (b.ι j ≫ b.π j) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: j', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j : J
⊢ F.map (b.ι j ≫ b.π j) = eqToHom ⋯
have pos : Eq.{v₂ + 1} (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j) (𝟙 (F.obj (f j))) (𝟙 ((F.obj ∘ f) j))
Tactic: simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
h : ¬j = j'
⊢ F.map (b.ι j ≫ b.π j') = 0
have neg : Eq (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j') (F.map 0) 0
Tactic: rw [bicone_ι_π_ne _ h, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
h : ¬j = j'
neg : Eq (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j') (F.map 0) 0
⊢ F.map (b.ι j ≫ b.π j') = 0
have neg₁ : Eq.{v₂ + 1} (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j') 0 0
Tactic: rw [bicone_ι_π_ne _ h, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).π.app
      j =
    Iso.hom
        (Iso.refl
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app j
have left : Eq (α :=
  obj.{0, v₂, 0, u₂}
      (obj (const (Discrete WalkingPair))
        (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    obj.{0, v₂, 0, u₂}
      (pair
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.left : Discrete WalkingPair })
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.right : Discrete WalkingPair }))
      { as := WalkingPair.left : Discrete WalkingPair })
  ((obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
          (Bicone.toCone (F.mapBicone b.toBicone))).π.app
    { as := WalkingPair.left })
  (Iso.hom
      (Iso.refl
        (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
    (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        j ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt) =
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app j
have left : Eq (α :=
  obj.{0, v₂, 0, u₂}
      (pair
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.left : Discrete WalkingPair })
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.right : Discrete WalkingPair }))
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
  ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
      { as := WalkingPair.left : Discrete WalkingPair } ≫
    Iso.hom
      (Iso.refl
        (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
  ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })
⊢ (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        j ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt) =
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app j
have right : Eq (α :=
  obj.{0, v₂, 0, u₂}
      (pair
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.left : Discrete WalkingPair })
        (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
          { as := WalkingPair.right : Discrete WalkingPair }))
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
  ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
      { as := WalkingPair.right : Discrete WalkingPair } ≫
    Iso.hom
      (Iso.refl
        (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
  ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f) (F.biproductComparison f) =
    𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
have w : ∀ (j j_1 : J),
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (biproduct.ι (F.obj ∘ f) j_1)
      (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f)
          (F.biproductComparison f))
        (biproduct.π (F.obj ∘ f) j)) =
    biproduct.ι (F.obj ∘ f) j_1 ≫ 𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) ≫ biproduct.π (F.obj ∘ f) j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f) (F.biproductComparison f) =
    𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
have w : ∀ (j j_1 : J),
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (biproduct.ι (F.obj ∘ f) j_1)
      (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f)
          (F.biproductComparison f))
        (biproduct.π (F.obj ∘ f) j)) =
    biproduct.ι (F.obj ∘ f) j_1 ≫ 𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) ≫ biproduct.π (F.obj ∘ f) j
Tactic: classical
    ext
    simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]