[GOAL]
R : Type u_1
inst✝⁸ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁷ : Category.{?u.28793, u_2} C
inst✝⁶ : Category.{?u.28797, u_3} D
inst✝⁵ : Preadditive C
inst✝⁴ : Linear R C
inst✝³ : Preadditive D
inst✝² : Linear R D
e : C ≌ D
inst✝¹ : Functor.Additive e.functor
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.inverse.map (f • r) = f • e.inverse.map r
[PROOFSTEP]
apply e.functor.map_injective
[GOAL]
case a
R : Type u_1
inst✝⁸ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁷ : Category.{?u.28793, u_2} C
inst✝⁶ : Category.{?u.28797, u_3} D
inst✝⁵ : Preadditive C
inst✝⁴ : Linear R C
inst✝³ : Preadditive D
inst✝² : Linear R D
e : C ≌ D
inst✝¹ : Functor.Additive e.functor
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)
[PROOFSTEP]
simp
