-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
inst_11 : Invertible (α := A) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
rw :
  HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
          ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
              (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                      QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                    (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                  Q₁ ⊗ₜ[R]
                ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                      QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                    (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                  Q₂) :
            BilinForm A (M₁ ⊗[R] M₂))))
rw₁ :
  HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HSMul.hSMul (α := ℕ) (β := A) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
      HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
        ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
            (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                    QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                  (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                Q₁ ⊗ₜ[R]
              ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                    QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                  (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                Q₂) :
          BilinForm A (M₁ ⊗[R] M₂))
rw₂ :
  HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HAdd.hAdd (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) •
      HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
        ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
            (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                    QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                  (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                Q₁ ⊗ₜ[R]
              ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                    QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                  (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                Q₂) :
          BilinForm A (M₁ ⊗[R] M₂))
rw₃ :
  HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HSMul.hSMul (α := A) 1
      (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
        ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
            (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                    QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                  (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                Q₁ ⊗ₜ[R]
              ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                    QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                  (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                Q₂) :
          BilinForm A (M₁ ⊗[R] M₂)))
⊢ HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
          ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
              (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                      QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                    (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                  Q₁ ⊗ₜ[R]
                ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                      QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                    (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                  Q₂) :
            BilinForm A (M₁ ⊗[R] M₂))))
have rw₄ : HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
    (BilinForm.tmul
      (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
          (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
        Q₁)
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q₂)) =
  HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
    ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
        (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
              (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
            Q₁ ⊗ₜ[R]
          ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
              (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
            Q₂) :
      BilinForm A (M₁ ⊗[R] M₂))
Tactic: rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two,
    one_smul]