R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.192555
R₃ : Type ?u.192558
M : Type ?u.192561
M₁ : Type u_3
M₂ : Type ?u.192567
Mₗ₁ : Type ?u.192570
Mₗ₁' : Type ?u.192573
Mₗ₂ : Type ?u.192576
Mₗ₂' : Type ?u.192579
K : Type ?u.192582
K₁ : Type ?u.192585
K₂ : Type ?u.192588
V : Type ?u.192591
V₁ : Type ?u.192594
V₂ : Type ?u.192597
n : Type ?u.192600
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₁
h : ↑(↑B x) y = 0
⊢ ↑(↑B y) x = 0
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.192555
R₃ : Type ?u.192558
M : Type ?u.192561
M₁ : Type u_3
M₂ : Type ?u.192567
Mₗ₁ : Type ?u.192570
Mₗ₁' : Type ?u.192573
Mₗ₂ : Type ?u.192576
Mₗ₂' : Type ?u.192579
K : Type ?u.192582
K₁ : Type ?u.192585
K₂ : Type ?u.192588
V : Type ?u.192591
V₁ : Type ?u.192594
V₂ : Type ?u.192597
n : Type ?u.192600
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
⊢ IsRefl B
intro x y h
no goals
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.192555
R₃ : Type ?u.192558
M : Type ?u.192561
M₁ : Type u_3
M₂ : Type ?u.192567
Mₗ₁ : Type ?u.192570
Mₗ₁' : Type ?u.192573
Mₗ₂ : Type ?u.192576
Mₗ₂' : Type ?u.192579
K : Type ?u.192582
K₁ : Type ?u.192585
K₂ : Type ?u.192588
V : Type ?u.192591
V₁ : Type ?u.192594
V₂ : Type ?u.192597
n : Type ?u.192600
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₁
h : ↑(↑B x) y = 0
⊢ ↑(↑B y) x = 0
rw [← neg H, h, neg_zero]