-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
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₂
⊢ 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₂))
have 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)
Tactic: ext