case mp
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
⊢ B = flip B

case mpr
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
⊢ IsSymm B
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
⊢ IsSymm B ↔ B = flip B
constructor <;> intro h
case mpr
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
⊢ ↑(RingHom.id R) (↑(↑B x) y) = ↑(↑B y) x
case mpr
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
⊢ IsSymm B
intro x y
no goals
case mpr
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
⊢ ↑(RingHom.id R) (↑(↑B x) y) = ↑(↑B y) x
conv_lhs => rw [h]
case mp.h.h
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
x✝¹ x✝ : M
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(flip B) x✝¹) x✝
case mp
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
⊢ B = flip B
ext
no goals
case mp.h.h
R : Type u_1
R₁ : Type ?u.168800
R₂ : Type ?u.168803
R₃ : Type ?u.168806
M : Type u_2
M₁ : Type ?u.168812
M₂ : Type ?u.168815
Mₗ₁ : Type ?u.168818
Mₗ₁' : Type ?u.168821
Mₗ₂ : Type ?u.168824
Mₗ₂' : Type ?u.168827
K : Type ?u.168830
K₁ : Type ?u.168833
K₂ : Type ?u.168836
V : Type ?u.168839
V₁ : Type ?u.168842
V₂ : Type ?u.168845
n : Type ?u.168848
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
x✝¹ x✝ : M
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(flip B) x✝¹) x✝
rw [← h, flip_apply, RingHom.id_apply]