R : Type u_1
R₁ : Type ?u.164233
R₂ : Type ?u.164236
R₃ : Type ?u.164239
M : Type u_2
M₁ : Type ?u.164245
M₂ : Type ?u.164248
Mₗ₁ : Type ?u.164251
Mₗ₁' : Type ?u.164254
Mₗ₂ : Type ?u.164257
Mₗ₂' : Type ?u.164260
K : Type ?u.164263
K₁ : Type ?u.164266
K₂ : Type ?u.164269
V : Type ?u.164272
V₁ : Type ?u.164275
V₂ : Type ?u.164278
n : Type ?u.164281
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
p : Submodule R M
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑I (↑(↑B ↑x✝¹) ↑x✝) = ↑(↑B ↑x✝) ↑x✝¹
R : Type u_1
R₁ : Type ?u.164233
R₂ : Type ?u.164236
R₃ : Type ?u.164239
M : Type u_2
M₁ : Type ?u.164245
M₂ : Type ?u.164248
Mₗ₁ : Type ?u.164251
Mₗ₁' : Type ?u.164254
Mₗ₂ : Type ?u.164257
Mₗ₂' : Type ?u.164260
K : Type ?u.164263
K₁ : Type ?u.164266
K₂ : Type ?u.164269
V : Type ?u.164272
V₁ : Type ?u.164275
V₂ : Type ?u.164278
n : Type ?u.164281
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
p : Submodule R M
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑I (↑(↑(domRestrict₁₂ B p p) x✝¹) x✝) = ↑(↑(domRestrict₁₂ B p p) x✝) x✝¹
simp_rw [domRestrict₁₂_apply]
no goals
R : Type u_1
R₁ : Type ?u.164233
R₂ : Type ?u.164236
R₃ : Type ?u.164239
M : Type u_2
M₁ : Type ?u.164245
M₂ : Type ?u.164248
Mₗ₁ : Type ?u.164251
Mₗ₁' : Type ?u.164254
Mₗ₂ : Type ?u.164257
Mₗ₂' : Type ?u.164260
K : Type ?u.164263
K₁ : Type ?u.164266
K₂ : Type ?u.164269
V : Type ?u.164272
V₁ : Type ?u.164275
V₂ : Type ?u.164278
n : Type ?u.164281
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
p : Submodule R M
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑I (↑(↑B ↑x✝¹) ↑x✝) = ↑(↑B ↑x✝) ↑x✝¹
exact H _ _