no goals
R : Type u_4
inst✝¹⁵ : Semiring R
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_2
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type ?u.411142
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.411172
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.411560
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.411951
ι'' : Type ?u.411954
M₂ : Type ?u.411957
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.411987
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
f f' : AlternatingMap R M N ι
g g₂ : AlternatingMap R M N' ι
g' : AlternatingMap R M' N' ι
v : ι → M
v' : ι → M'
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ update v i (v j) i = update v i (v j) j
rw [Function.update_same, Function.update_noteq hij.symm]