R : Type u_1
R₁ : Type ?u.159549
R₂ : Type ?u.159552
R₃ : Type ?u.159555
M : Type u_2
M₁ : Type ?u.159561
M₂ : Type ?u.159564
Mₗ₁ : Type ?u.159567
Mₗ₁' : Type ?u.159570
Mₗ₂ : Type ?u.159573
Mₗ₂' : Type ?u.159576
K : Type ?u.159579
K₁ : Type ?u.159582
K₂ : Type ?u.159585
V : Type ?u.159588
V₁ : Type ?u.159591
V₂ : Type ?u.159594
n : Type ?u.159597
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
x y : M
H1 : ↑(↑B x) y = 0
⊢ ↑I (↑(↑B x) y) = 0
R : Type u_1
R₁ : Type ?u.159549
R₂ : Type ?u.159552
R₃ : Type ?u.159555
M : Type u_2
M₁ : Type ?u.159561
M₂ : Type ?u.159564
Mₗ₁ : Type ?u.159567
Mₗ₁' : Type ?u.159570
Mₗ₂ : Type ?u.159573
Mₗ₂' : Type ?u.159576
K : Type ?u.159579
K₁ : Type ?u.159582
K₂ : Type ?u.159585
V : Type ?u.159588
V₁ : Type ?u.159591
V₂ : Type ?u.159594
n : Type ?u.159597
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
x y : M
H1 : ↑(↑B x) y = 0
⊢ ↑(↑B y) x = 0
rw [← H.eq]
no goals
R : Type u_1
R₁ : Type ?u.159549
R₂ : Type ?u.159552
R₃ : Type ?u.159555
M : Type u_2
M₁ : Type ?u.159561
M₂ : Type ?u.159564
Mₗ₁ : Type ?u.159567
Mₗ₁' : Type ?u.159570
Mₗ₂ : Type ?u.159573
Mₗ₂' : Type ?u.159576
K : Type ?u.159579
K₁ : Type ?u.159582
K₂ : Type ?u.159585
V : Type ?u.159588
V₁ : Type ?u.159591
V₂ : Type ?u.159594
n : Type ?u.159597
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
x y : M
H1 : ↑(↑B x) y = 0
⊢ ↑I (↑(↑B x) y) = 0
simp [H1]