[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (BilinForm.tmul B₁ B₂)
[PROOFSTEP]
rw [isSymm_iff_flip R]
[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ ↑(flipHom R) (BilinForm.tmul B₁ B₂) = BilinForm.tmul B₁ B₂
[PROOFSTEP]
apply toLin.injective
[GOAL]
case a
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ ↑toLin (↑(flipHom R) (BilinForm.tmul B₁ B₂)) = ↑toLin (BilinForm.tmul B₁ B₂)
[PROOFSTEP]
ext x₁ x₂ y₁ y₂
[GOAL]
case a.a.h.h.a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ ↑(↑(AlgebraTensorModule.curry (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(flipHom R) (BilinForm.tmul B₁ B₂)))) x₁) x₂))
          y₁)
      y₂ =
    ↑(↑(AlgebraTensorModule.curry (↑(↑(AlgebraTensorModule.curry (↑toLin (BilinForm.tmul B₁ B₂))) x₁) x₂)) y₁) y₂
[PROOFSTEP]
exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm
[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
⊢ ↑(tensorDistribEquiv R) = tensorDistrib R R
[PROOFSTEP]
ext B₁ B₂ : 3
[GOAL]
case a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂ =
    ↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂
[PROOFSTEP]
apply toLin.injective
[GOAL]
case a.h.h.a
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ↑toLin (↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂) =
    ↑toLin (↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)
[PROOFSTEP]
ext
[GOAL]
case a.h.h.a.a.h.h.a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)))
                    x✝³)
                x✝²))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂))) x✝³)
                x✝²))
          x✝¹)
      x✝
[PROOFSTEP]
exact mul_comm _ _
