no goals
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.148405
M₆ : Type ?u.148408
S : Type ?u.148411
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : AddCommMonoid M₅
inst✝¹⁰ : AddCommMonoid M₆
inst✝⁹ : Module R M
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : Module R M₅
inst✝⁴ : Module R M₆
f : M →ₗ[R] M₂
A : Type u_1
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
B : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Module R B
a₁ a₂ : A
⊢ (↑(inl R A B) (a₁ * a₂)).snd = (↑(inl R A B) a₁ * ↑(inl R A B) a₂).snd
simp