R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B (y + x)) (y + x) = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
⊢ -↑(↑B x) y = ↑(↑B y) x
have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B x) y + ↑(↑B y) x = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B (y + x)) (y + x) = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
simp [map_add, self_eq_zero H] at H1
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : -↑(↑B x) y = ↑(↑B y) x
⊢ -↑(↑B x) y = ↑(↑B y) x
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B x) y + ↑(↑B y) x = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
rw [add_eq_zero_iff_neg_eq] at H1
no goals
R : Type u_1
R₁ : Type u_3
R₂ : Type ?u.184837
R₃ : Type ?u.184840
M : Type ?u.184843
M₁ : Type u_2
M₂ : Type ?u.184849
Mₗ₁ : Type ?u.184852
Mₗ₁' : Type ?u.184855
Mₗ₂ : Type ?u.184858
Mₗ₂' : Type ?u.184861
K : Type ?u.184864
K₁ : Type ?u.184867
K₂ : Type ?u.184870
V : Type ?u.184873
V₁ : Type ?u.184876
V₂ : Type ?u.184879
n : Type ?u.184882
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : -↑(↑B x) y = ↑(↑B y) x
⊢ -↑(↑B x) y = ↑(↑B y) x
exact H1