no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.537847
inst✝¹³ : Monoid R'
R'' : Type ?u.537853
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type ?u.537868
S : Type ?u.537871
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
r : R
x : M ⊗[R] N
p : M
q : N
⊢ ↑(liftAux f) (r • p ⊗ₜ[R] q) = r • ↑(liftAux f) (p ⊗ₜ[R] q)
simp_rw [← tmul_smul, liftAux_tmul, (f p).map_smul]
no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.537847
inst✝¹³ : Monoid R'
R'' : Type ?u.537853
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type ?u.537868
S : Type ?u.537871
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
r : R
x p q : M ⊗[R] N
ih1 : ↑(liftAux f) (r • p) = r • ↑(liftAux f) p
ih2 : ↑(liftAux f) (r • q) = r • ↑(liftAux f) q
⊢ ↑(liftAux f) (r • (p + q)) = r • ↑(liftAux f) (p + q)
simp_rw [smul_add, (liftAux f).map_add, ih1, ih2, smul_add]