[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b c : F ⟶ G), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ c✝ : F ⟶ G
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ c✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + b✝ + c✝) x✝ = NatTrans.app (a✝ + (b✝ + c✝)) x✝
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (0 + a✝) x✝ = NatTrans.app a✝ x✝
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + 0) x✝ = NatTrans.app a✝ x✝
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b : F ⟶ G), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ - b✝) x✝ = NatTrans.app (a✝ + -b✝) x✝
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (-a✝ + a✝) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b : F ⟶ G), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + b✝) x✝ = NatTrans.app (b✝ + a✝) x✝
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
⊢ ∀ (P Q R : C ⥤ D) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
x✝ : C
⊢ NatTrans.app ((f✝ + f'✝) ≫ g✝) x✝ = NatTrans.app (f✝ ≫ g✝ + f'✝ ≫ g✝) x✝
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
⊢ ∀ (P Q R : C ⥤ D) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
x✝ : C
⊢ NatTrans.app (f✝ ≫ (g✝ + g'✝)) x✝ = NatTrans.app (f✝ ≫ g✝ + f✝ ≫ g'✝) x✝
[PROOFSTEP]
apply comp_add
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_5, u_1} C
inst✝¹ : Category.{u_4, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
ι : Type u_3
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ app (∑ i in s, α i) X = ∑ i in s, app (α i) X
[PROOFSTEP]
simp only [← appHom_apply, map_sum]
