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.417280
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.417310
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.417698
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.418089
ι'' : Type ?u.418092
M₂ : Type ?u.418095
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.418125
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
⊢ ↑f (update (update v j (v i)) i (v j)) + ↑f v = 0
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.417280
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.417310
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.417698
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.418089
ι'' : Type ?u.418092
M₂ : Type ?u.418095
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.418125
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
⊢ ↑f (v ∘ ↑(Equiv.swap i j)) + ↑f v = 0
rw [Equiv.comp_swap_eq_update]
case h.e'_2
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.417280
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.417310
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.417698
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.418089
ι'' : Type ?u.418092
M₂ : Type ?u.418095
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.418125
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
⊢ ↑f (update (update v j (v i)) i (v j)) + ↑f v = ↑f (update (update v i (v i + v j)) j (v i + v j))
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.417280
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.417310
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.417698
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.418089
ι'' : Type ?u.418092
M₂ : Type ?u.418095
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.418125
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
⊢ ↑f (update (update v j (v i)) i (v j)) + ↑f v = 0
convert f.map_update_update v hij (v i + v j)
no goals
case h.e'_2
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.417280
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
M' : Type ?u.417310
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
N' : Type ?u.417698
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R N'
ι : Type u_1
ι' : Type ?u.418089
ι'' : Type ?u.418092
M₂ : Type ?u.418095
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type ?u.418125
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
⊢ ↑f (update (update v j (v i)) i (v j)) + ↑f v = ↑f (update (update v i (v i + v j)) j (v i + v j))
simp [f.map_update_self _ hij, f.map_update_self _ hij.symm,
  Function.update_comm hij (v i + v j) (v _) v, Function.update_comm hij.symm (v i) (v i) v]