awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ G.map
      (HAdd.hAdd (α := F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y))
        (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y))
        (Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y))) =
    HAdd.hAdd (α := G.obj (F.obj (F.objPreimage X)) ⟶ G.obj (F.obj (F.objPreimage Y)))
      (G.map (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))
      (G.map (Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)))
have erw : G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')
Tactic: erw [← hf', ← hg', ← (F ⋙ G).map_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')
have dsimp : G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))
have rw : G.map (F.map f' + F.map g') = G.map (F.map f' + F.map g')
Tactic: rw [F.map_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : G.Additive
inst_7 : (F ⋙ G).Additive
inst_8 : G.Faithful
x x_1 : C
f₁ f₂ : x ⟶ x_1
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
have rw : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁ + F.map f₂)
Tactic: rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : G.Additive
inst_7 : (F ⋙ G).Additive
inst_8 : G.Faithful
x x_1 : C
f₁ f₂ : x ⟶ x_1
rw : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁ + F.map f₂)
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
have rw₁ : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁) + G.map (F.map f₂)
Tactic: rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : G.Additive
inst_7 : (F ⋙ G).Additive
inst_8 : G.Faithful
x x_1 : C
f₁ f₂ : x ⟶ x_1
rw : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁ + F.map f₂)
rw₁ : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁) + G.map (F.map f₂)
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
have rw₂ : (F ⋙ G).map f₁ + (F ⋙ G).map f₂ = G.map (F.map f₁) + G.map (F.map f₂)
Tactic: rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : G.Additive
inst_7 : (F ⋙ G).Additive
inst_8 : G.Faithful
x x_1 : C
f₁ f₂ : x ⟶ x_1
rw : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁ + F.map f₂)
rw₁ : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁) + G.map (F.map f₂)
rw₂ : (F ⋙ G).map f₁ + (F ⋙ G).map f₂ = G.map (F.map f₁) + G.map (F.map f₂)
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
have rw₃ : G.map (F.map f₁) + (F ⋙ G).map f₂ = G.map (F.map f₁) + G.map (F.map f₂)
Tactic: rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : G.Additive
inst_7 : (F ⋙ G).Additive
inst_8 : G.Faithful
x x_1 : C
f₁ f₂ : x ⟶ x_1
rw : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁ + F.map f₂)
rw₁ : (F ⋙ G).map (f₁ + f₂) = G.map (F.map f₁) + G.map (F.map f₂)
rw₂ : (F ⋙ G).map f₁ + (F ⋙ G).map f₂ = G.map (F.map f₁) + G.map (F.map f₂)
rw₃ : G.map (F.map f₁) + (F ⋙ G).map f₂ = G.map (F.map f₁) + G.map (F.map f₂)
⊢ G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
have rw₄ : G.map (F.map f₁) + G.map (F.map f₂) = G.map (F.map f₁) + G.map (F.map f₂)
Tactic: rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : HasZeroObject.{v_1, u_1} C
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : HasZeroObject.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : HasZeroObject.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : HasZeroObject.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₃ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : IsZero F
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ IsZero.{v_2, u_2} (F.obj x_1)
have rw : Eq.{v_2 + 1} (α := F.obj x_1 ⟶ F.obj x_1) (𝟙 (F.obj x_1)) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Additive
J : Type
h : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v₁, u₁} f
hb : b.IsBilimit
⊢ Eq.{v₂ + 1} (α := Bicone.pt (F.mapBicone b) ⟶ Bicone.pt (F.mapBicone b))
    (∑ j : J, Bicone.π (F.mapBicone b) j ≫ Bicone.ι (F.mapBicone b) j) (𝟙 (Bicone.pt (F.mapBicone b)))
have simp_rw : Eq.{v₂ + 1} (α := Bicone.pt (F.mapBicone b) ⟶ Bicone.pt (F.mapBicone b)) (∑ x : J, F.map (b.π x ≫ b.ι x))
  (𝟙 (Bicone.pt (F.mapBicone b)))
Tactic: simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Additive
J : Type
h : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v₁, u₁} f
hb : b.IsBilimit
⊢ Eq.{v₂ + 1} (α := Bicone.pt (F.mapBicone b) ⟶ Bicone.pt (F.mapBicone b)) (∑ x : J, F.map (b.π x ≫ b.ι x))
    (𝟙 (Bicone.pt (F.mapBicone b)))
have erw : F.map (∑ a : J, b.π a ≫ b.ι a) = 𝟙 (Bicone.pt (F.mapBicone b))
Tactic: erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Additive
J : Type
h : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v₁, u₁} f
hb : b.IsBilimit
erw : F.map (∑ a : J, b.π a ≫ b.ι a) = 𝟙 (Bicone.pt (F.mapBicone b))
⊢ Eq.{v₂ + 1} (α := Bicone.pt (F.mapBicone b) ⟶ Bicone.pt (F.mapBicone b)) (∑ x : J, F.map (b.π x ≫ b.ι x))
    (𝟙 (Bicone.pt (F.mapBicone b)))
have erw₁ : F.map (∑ a : J, b.π a ≫ b.ι a) = F.map (𝟙 b.pt)
Tactic: erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Additive
J : Type
h : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v₁, u₁} f
hb : b.IsBilimit
erw : F.map (∑ a : J, b.π a ≫ b.ι a) = 𝟙 (Bicone.pt (F.mapBicone b))
erw₁ : F.map (∑ a : J, b.π a ≫ b.ι a) = F.map (𝟙 b.pt)
⊢ Eq.{v₂ + 1} (α := Bicone.pt (F.mapBicone b) ⟶ Bicone.pt (F.mapBicone b)) (∑ x : J, F.map (b.π x ≫ b.ι x))
    (𝟙 (Bicone.pt (F.mapBicone b)))
have erw₂ : F.map (𝟙 b.pt) = F.map (𝟙 b.pt)
Tactic: erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g
have rw : F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₁ : CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₂ : CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
    (F.map (biprod.desc f g)) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₃ : CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₃ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₄ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
    (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (Iso.inv (F.mapBiprod X X))
        (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
          (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
          (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) :
      biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₃ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
    F.map f + F.map g
rw₄ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (Iso.inv (F.mapBiprod X X))
          (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y) =
    F.map f + F.map g
⊢ F.map (f + g) = F.map f + F.map g
have rw₅ : CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)))
    (biprod.desc (F.map f) (F.map g)) =
  F.map f + F.map g
Tactic: rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]