[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
r : ℕ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.rightComp X g).map_nsmul f r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
f : X ⟶ Y
r : ℕ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.leftComp Z f).map_nsmul g r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
r : ℤ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.rightComp X g).map_zsmul f r
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y Z : C
f : X ⟶ Y
r : ℤ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
exact (Preadditive.leftComp Z f).map_zsmul g r
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X : C
⊢ Module R (End X)
[PROOFSTEP]
dsimp [End]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X : C
⊢ Module R (X ⟶ X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), (fun g => f ≫ g) (x + y) = (fun g => f ≫ g) x + (fun g => f ≫ g) y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (r : R) (x : Y ⟶ Z),
    AddHom.toFun { toFun := fun g => f ≫ g, map_add' := (_ : ∀ (a a_1 : Y ⟶ Z), f ≫ (a + a_1) = f ≫ a + f ≫ a_1) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := fun g => f ≫ g, map_add' := (_ : ∀ (a a_1 : Y ⟶ Z), f ≫ (a + a_1) = f ≫ a + f ≫ a_1) } x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (fun f => f ≫ g) (x + y) = (fun f => f ≫ g) x + (fun f => f ≫ g) y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (r : R) (x : X ⟶ Y),
    AddHom.toFun { toFun := fun f => f ≫ g, map_add' := (_ : ∀ (a a_1 : X ⟶ Y), (a + a_1) ≫ g = a ≫ g + a_1 ≫ g) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := fun f => f ≫ g, map_add' := (_ : ∀ (a a_1 : X ⟶ Y), (a + a_1) ≫ g = a ≫ g + a_1 ≫ g) } x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'
[PROOFSTEP]
rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H 
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • g = r • g'
⊢ g = g'
[PROOFSTEP]
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'
[PROOFSTEP]
rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H 
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : r • g = r • g'
⊢ g = g'
[PROOFSTEP]
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H
[GOAL]
C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{?u.35990, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
src✝ : (X ⟶ W) →ₗ[k] Y ⟶ Z := comp (rightComp k Y f₂.hom) (leftComp k W f₁.symm.hom)
x : X ⟶ W
⊢ ↑(comp (leftComp k W f₁.hom) (rightComp k Y f₂.symm.hom))
      (AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : X ⟶ W),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id k) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
simp only [Iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply, leftComp_apply,
  rightComp_apply, Category.assoc, Iso.hom_inv_id, Category.comp_id, Iso.hom_inv_id_assoc]
[GOAL]
C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{?u.35990, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
src✝ : (X ⟶ W) →ₗ[k] Y ⟶ Z := comp (rightComp k Y f₂.hom) (leftComp k W f₁.symm.hom)
x : Y ⟶ Z
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : k) (x : X ⟶ W),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id k) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(comp (leftComp k W f₁.hom) (rightComp k Y f₂.symm.hom)) x) =
    x
[PROOFSTEP]
simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply, leftComp_apply,
  LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (x y : X ⟶ Y), (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝ y✝ : X ⟶ Y
⊢ (fun f => leftComp S Z f) (x✝ + y✝) = (fun f => leftComp S Z f) x✝ + (fun f => leftComp S Z f) y✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝¹ y✝ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ ↑((fun f => leftComp S Z f) (x✝¹ + y✝)) x✝ = ↑((fun f => leftComp S Z f) x✝¹ + (fun f => leftComp S Z f) y✝) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (r : S) (x : X ⟶ Y),
    AddHom.toFun
        { toFun := fun f => leftComp S Z f,
          map_add' :=
            (_ :
              ∀ (x y : X ⟶ Y),
                (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
        (r • x) =
      ↑(RingHom.id S) r •
        AddHom.toFun
          { toFun := fun f => leftComp S Z f,
            map_add' :=
              (_ :
                ∀ (x y : X ⟶ Y),
                  (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
          x
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
r✝ : S
x✝ : X ⟶ Y
⊢ AddHom.toFun
      { toFun := fun f => leftComp S Z f,
        map_add' :=
          (_ :
            ∀ (x y : X ⟶ Y),
              (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
      (r✝ • x✝) =
    ↑(RingHom.id S) r✝ •
      AddHom.toFun
        { toFun := fun f => leftComp S Z f,
          map_add' :=
            (_ :
              ∀ (x y : X ⟶ Y),
                (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
r✝ : S
x✝¹ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ ↑(AddHom.toFun
          { toFun := fun f => leftComp S Z f,
            map_add' :=
              (_ :
                ∀ (x y : X ⟶ Y),
                  (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
          (r✝ • x✝¹))
      x✝ =
    ↑(↑(RingHom.id S) r✝ •
          AddHom.toFun
            { toFun := fun f => leftComp S Z f,
              map_add' :=
                (_ :
                  ∀ (x y : X ⟶ Y),
                    (fun f => leftComp S Z f) (x + y) = (fun f => leftComp S Z f) x + (fun f => leftComp S Z f) y) }
            x✝¹)
      x✝
[PROOFSTEP]
simp
