-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
        (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
        (Q₁.tmul Q₃) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
have a : ∀ (m₁ : M₁) (m₃ : M₃) (m₁' : M₁) (m₃' : M₃),
  Eq.{uR + 1} (α := R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
                                    (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))) :
                                M₁ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                              (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R)
                            m₁ :
                          M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                        (a : M₃) → M₁ ⊗[R] M₃ →ₗ[R] R)
                      m₃) :
                  M₁ →ₗ[R] M₃ →ₗ[R] R) :
                (a : M₁) → M₃ →ₗ[R] R)
              m₁' :
            M₃ →ₗ[R] R) :
          (a : M₃) → R)
        m₃' :
      R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
                                    (Q₁.tmul Q₃)) :
                                M₁ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                              (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R)
                            m₁ :
                          M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                        (a : M₃) → M₁ ⊗[R] M₃ →ₗ[R] R)
                      m₃) :
                  M₁ →ₗ[R] M₃ →ₗ[R] R) :
                (a : M₁) → M₃ →ₗ[R] R)
              m₁' :
            M₃ →ₗ[R] R) :
          (a : M₃) → R)
        m₃' :
      R)
Tactic: ext m₁ m₃ m₁' m₃'