[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ (fun X => r • NatTrans.app α X) Y = (fun X => r • NatTrans.app α X) X ≫ G.map f
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun X => r • NatTrans.app α X) Y✝ = (fun X => r • NatTrans.app α X) X✝ ≫ G.map f✝
[PROOFSTEP]
rw [comp_smul, smul_comp, α.naturality]
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (b : F ⟶ G), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
b✝ : F ⟶ G
⊢ 1 • b✝ = b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (1 • b✝) x✝ = NatTrans.app b✝ x✝
[PROOFSTEP]
apply one_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x y : R) (b : F ⟶ G), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝ y✝ : R
b✝ : F ⟶ G
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝¹ y✝ : R
b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app ((x✝¹ * y✝) • b✝) x✝ = NatTrans.app (x✝¹ • y✝ • b✝) x✝
[PROOFSTEP]
apply mul_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝ : C
⊢ NatTrans.app (a✝ • 0) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply smul_zero
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (a : R) (x y : F ⟶ G), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝ y✝ : F ⟶ G
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝¹ y✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ • (x✝¹ + y✝)) x✝ = NatTrans.app (a✝ • x✝¹ + a✝ • y✝) x✝
[PROOFSTEP]
apply smul_add
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (r s : R) (x : F ⟶ G), (r + s) • x = r • x + s • x
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r✝ s✝ : R
x✝ : F ⟶ G
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r✝ s✝ : R
x✝¹ : F ⟶ G
x✝ : C
⊢ NatTrans.app ((r✝ + s✝) • x✝¹) x✝ = NatTrans.app (r✝ • x✝¹ + s✝ • x✝¹) x✝
[PROOFSTEP]
apply add_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x : F ⟶ G), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝ : F ⟶ G
⊢ 0 • x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝¹ : F ⟶ G
x✝ : C
⊢ NatTrans.app (0 • x✝¹) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply zero_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((r✝ • f✝) ≫ g✝) x✝ = NatTrans.app (r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
apply smul_comp
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app (f✝ ≫ (r✝ • g✝)) x✝ = NatTrans.app (r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
apply comp_smul
