no goals
R : Type u_1
R₁ : Type ?u.296180
R₂ : Type ?u.296183
R₃ : Type ?u.296186
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.296195
Mₗ₁ : Type ?u.296198
Mₗ₁' : Type ?u.296201
Mₗ₂ : Type ?u.296204
Mₗ₂' : Type ?u.296207
K : Type ?u.296210
K₁ : Type ?u.296213
K₂ : Type ?u.296216
V : Type ?u.296219
V₁ : Type ?u.296222
V₂ : Type ?u.296225
n : Type ?u.296228
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
x✝¹ : M
x✝ : M₁
⊢ ↑(↑B' (↑0 x✝¹)) x✝ = ↑(↑B x✝¹) (↑0 x✝)
simp only [zero_apply, map_zero]