awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
obtain :
  ∀ (f' : F.objPreimage X ⟶ F.objPreimage Y)
    (hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)),
    G.map (f + g) = G.map f + G.map g
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨f', hf'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫
      (F.objObjPreimageIso Y).inv)

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
obtain :
  ∀ (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 + g) = G.map f + G.map g
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨g', hg'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ g ≫
      (F.objObjPreimageIso Y).inv)

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
simp :
  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)))
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
simp only [← cancel_mono (G.map (F.objObjPreimageIso Y).inv),
      ← cancel_epi (G.map (F.objObjPreimageIso X).hom),
      Preadditive.add_comp, Preadditive.comp_add, ← Functor.map_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Preadditive.add_comp, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Preadditive.comp_add, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
erw : G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')
⊢ 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)))

Tactic:
erw [← hf', ← hg', ← (F ⋙ G).map_add]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_add
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
dsimp : G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
rw rw₁ : G.map (F.map f' + F.map g') = G.map (F.map f' + F.map g')
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))

Tactic:
rw [F.map_add]

Premises used: CategoryTheory.Functor.map_add
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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₂)
rw₄ rw₅ : G.map (F.map f₁) + G.map (F.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₂)

Tactic:
rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_add, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
⊢ IsZero.{v_2, u_2} (F.obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
rw : Eq.{v_2 + 1} (α := F.obj x_1 ⟶ F.obj x_1) (𝟙 (F.obj x_1)) 0
⊢ IsZero.{v_2, u_2} (F.obj x_1)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ Eq.{v_2 + 1} (α := F.obj x_1 ⟶ F.obj x_1) (𝟙 (F.obj x_1)) 0

Tactic:
NatTrans.congr_app ((IsZero.iff_id_eq_zero _).1 hF) _

Premises used: CategoryTheory.NatTrans.congr_app, Iff.mp, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ Eq.{v_2 + 1} (α := F.obj x_1 ⟶ F.obj x_1) (𝟙 (F.obj x_1)) 0

Tactic:
exact NatTrans.congr_app ((IsZero.iff_id_eq_zero _).1 hF) _

Premises used: CategoryTheory.NatTrans.congr_app, Iff.mp, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : HasZeroObject.{v_2, u_2} D
⊢ Additive.{v_1, u_1, v_2, u_2} (C := C) (D := D) 0

Tactic:
.of_isZero (isZero_zero _)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.Additive.of_isZero
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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_1 : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F_1.Additive
E' : Type u_4
inst_7 : Category.{v_4, u_4} E'
inst_8 : Preadditive.{v_4, u_4} E'
G : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
F : Functor.{v_3, v_4, u_3, u_4} E E'
inst_9 : F.Additive
inst_10 : G.Additive
⊢ (G ⋙ obj (whiskeringRight D E E') F).Additive

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
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)))
⊢ 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)))

Tactic:
simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]

Premises used: CategoryTheory.Functor.mapBicone_ι, CategoryTheory.Functor.mapBicone_π, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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)
erw₂ erw₃ : F.map (𝟙 b.pt) = 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)))

Tactic:
erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]

Premises used: CategoryTheory.Limits.IsBilimit.total, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_sum
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
⊢ HasBinaryBiproducts.{v₁, u₁} C

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
this : HasBinaryBiproducts.{v₁, u₁} C
⊢ PreservesBinaryBiproducts F

Tactic:
have := preservesBinaryBiproducts_of_preservesBinaryProducts F
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
this_1 : HasBinaryBiproducts.{v₁, u₁} C
this : PreservesBinaryBiproducts F
⊢ F.Additive

Tactic:
Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : HasBinaryProducts.{v₁, u₁} C
inst_5 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_6 : F.PreservesZeroMorphisms
this_1 : HasBinaryBiproducts.{v₁, u₁} C
this : PreservesBinaryBiproducts F
⊢ F.Additive

Tactic:
exact Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
e : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_4 : e.functor.Additive
f g : D
f_1 g_1 : f ⟶ g
⊢ e.functor.map (e.inverse.map (f_1 + g_1)) = e.functor.map (e.inverse.map f_1 + e.inverse.map g_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ additiveFunctor C D F ↔ F.Additive

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.additiveFunctor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : AdditiveFunctor.{v_1, u_1, v_2, u_2} C D
⊢ F.obj (P := additiveFunctor C D).Additive

Tactic:
F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.additiveFunctor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ additiveFunctor C D F

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ ObjectProperty.FullSubcategory.obj (P := additiveFunctor C D) (of F) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : AdditiveFunctor.{v_1, u_1, v_2, u_2} C D
⊢ Functor.obj (forget C D) F = F.obj (P := additiveFunctor C D)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
⊢ Functor.obj (C := AdditiveFunctor.{v_1, u_1, v_2, u_2} C D) (forget C D) (of F) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 G : AdditiveFunctor.{v_1, u_1, v_2, u_2} C D
α : F ⟶ G
⊢ Functor.map (forget C D) α = α.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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 : AdditiveFunctor.{v_1, u_1, v_2, u_2} C D
⊢ F.obj (P := additiveFunctor C D).Additive

Tactic:
F.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.additiveFunctor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : leftExactFunctor C D F
⊢ PreservesFiniteLimits F

Tactic:
simp only [leftExactFunctor_iff] at h

Premises used: CategoryTheory.leftExactFunctor_iff
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : PreservesFiniteLimits F
⊢ additiveFunctor C D F

Tactic:
Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.additiveFunctor, CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : PreservesFiniteLimits F
⊢ additiveFunctor C D F

Tactic:
exact Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : rightExactFunctor C D F
⊢ PreservesFiniteColimits F

Tactic:
simp only [rightExactFunctor_iff] at h

Premises used: CategoryTheory.rightExactFunctor_iff
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : PreservesFiniteColimits F
⊢ additiveFunctor C D F

Tactic:
Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.additiveFunctor, CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : PreservesFiniteColimits F
⊢ additiveFunctor C D F

Tactic:
exact Functor.additive_of_preservesBinaryBiproducts F

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
⊢ LE.le (α := ObjectProperty (Functor.{v₁, v₂, u₁, u₂} C D)) (exactFunctor C D) (additiveFunctor C D)

Tactic:
(exactFunctor_le_leftExactFunctor C D).trans
    (leftExactFunctor_le_additiveFunctor C D)

Premises used: CategoryTheory.leftExactFunctor_le_additiveFunctor, CategoryTheory.exactFunctor_le_leftExactFunctor, LE.le.trans
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ ObjectProperty.FullSubcategory.obj (P := additiveFunctor C D) (Functor.obj (ofLeftExact C D) F) =
    F.obj (P := leftExactFunctor C D)

Tactic:
rfl

Premises used: CategoryTheory.leftExactFunctor, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
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
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ ObjectProperty.FullSubcategory.obj (P := additiveFunctor C D) (Functor.obj (ofRightExact C D) F) =
    F.obj (P := rightExactFunctor C D)

Tactic:
rfl

Premises used: rfl, CategoryTheory.rightExactFunctor