awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₀ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
    biprod.fst =
  (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
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
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₁ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
    biprod.snd =
  (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
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
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₂ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
    biprod.fst =
  (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
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
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₃ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
    biprod.snd =
  (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
⊢ Eq (α := F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
      F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (lift fun (j : J) ↦ F.map (g j) : F.obj W ⟶ biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
        F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (π (F.obj ∘ f) j : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ (F.obj ∘ f) j) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (lift fun (j : J) ↦ F.map (g j)) (π (F.obj ∘ f) j)
Tactic: ext 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
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
        F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (π (F.obj ∘ f) j : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ (F.obj ∘ f) j) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (lift fun (j : J) ↦ F.map (g j)) (π (F.obj ∘ f) j)
have w : CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
      F.obj W ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
    (π (fun (x : J) ↦ F.obj (f x)) j : (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj (f j)) =
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) (lift fun (j : J) ↦ F.map (g j))
    (π (fun (x : J) ↦ F.obj (f x)) j)
Tactic: dsimp only [Function.comp_def]
-- 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
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ Eq (α := biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
      biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W)
    (desc fun (j : J) ↦ F.map (g j) : (biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j)) ⟶ F.obj W)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (ι (F.obj ∘ f) j : (F.obj ∘ f) j ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (ι (F.obj ∘ f) j) (desc fun (j : J) ↦ F.map (g j))
Tactic: ext 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
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (ι (F.obj ∘ f) j : (F.obj ∘ f) j ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (ι (F.obj ∘ f) j) (desc fun (j : J) ↦ F.map (g j))
have w : CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
    (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j :
      F.obj (f j) ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
      (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj W) =
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
    (ι.{w₁, v₂, u₂} (C := D) (fun (x : J) ↦ F.obj (f x)) j) (desc fun (j : J) ↦ F.map (g j))
Tactic: dsimp only [Function.comp_def]
-- 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
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (desc fun (j : J) ↦ F.map (g j) : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
    (F.map (desc g))
have rw : Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
  (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
      biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
  (F.map (desc g))
Tactic: rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]
-- 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
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
rw :
  Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
        biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
    (F.map (desc g))
⊢ Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (desc fun (j : J) ↦ F.map (g j) : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W))
    (F.map (desc g))
have rw₁ : Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ F.obj W) (F.map (desc g)) (F.map (desc g))
Tactic: rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]
-- 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 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ Eq (α := F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₀ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (fst : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj X) =
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) fst
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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (fst : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj X) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) fst
⊢ Eq (α := F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
have h₁ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (snd : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj Y) =
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (lift (F.map f) (F.map g)) snd
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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
have rw : Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
  (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
      F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
  (F.map (lift f g))
Tactic: rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
-- 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 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
rw :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
⊢ Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
have rw₁ : Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
  (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))))
  (F.map (lift f g))
Tactic: rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
-- 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 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
rw :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
rw₁ :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
        (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
        (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))))
    (F.map (lift f g))
⊢ Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
have rw₂ : F.map (lift f g) ≫ 𝟙 (F.obj (biprod.{v₁, u₁} X Y)) = F.map (lift f g)
Tactic: rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
-- 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 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
rw :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (Iso.hom (F.mapBiprod X Y)) :
        F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
rw₁ :
  Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
        (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
        (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))))
    (F.map (lift f g))
rw₂ : F.map (lift f g) ≫ 𝟙 (F.obj (biprod.{v₁, u₁} X Y)) = F.map (lift f g)
⊢ Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (lift (F.map f) (F.map g) : F.obj W ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y)))
    (F.map (lift f g))
have rw₃ : Eq (α := F.obj W ⟶ F.obj (biprod.{v₁, u₁} X Y)) (F.map (lift f g)) (F.map (lift f g))
Tactic: rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
-- 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 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_6 : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ Eq (α := biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
    (desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W)
have h₀ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (inl : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (Iso.inv (F.mapBiprod X Y)) (F.map (desc f g)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj W) =
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) inl (desc (F.map f) (F.map g))
Tactic: ext