-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
a :
  ∀ (x : M₁) (x_1 : M₂) (x_2 : M₁) (x_3 : M₂),
    Eq.{uR + 1} (α := R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (((((AlgebraTensorModule.curry
                                                  (↑(tensorDistribEquiv R) :
                                                    BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                                BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                              (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                            B₁ :
                                          BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                        (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                      B₂) :
                                  M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                              x :
                            M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                          (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                        x_1) :
                    M₁ →ₗ[R] M₂ →ₗ[R] R) :
                  (a : M₁) → M₂ →ₗ[R] R)
                x_2 :
              M₂ →ₗ[R] R) :
            (a : M₂) → R)
          x_3 :
        R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                                                BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                              (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                            B₁ :
                                          BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                        (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                      B₂) :
                                  M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                              x :
                            M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                          (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                        x_1) :
                    M₁ →ₗ[R] M₂ →ₗ[R] R) :
                  (a : M₁) → M₂ →ₗ[R] R)
                x_2 :
              M₂ →ₗ[R] R) :
            (a : M₂) → R)
          x_3 :
        R)
⊢ Eq (α := BilinForm R (M₁ ⊗[R] M₂))
    (((((AlgebraTensorModule.curry
                    (↑(tensorDistribEquiv R) : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                  BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
              B₁ :
            BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
          (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
        B₂ :
      BilinForm R (M₁ ⊗[R] M₂))
    (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                  BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
              B₁ :
            BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
          (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
        B₂ :
      BilinForm R (M₁ ⊗[R] M₂))

Tactic:
ext