-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 3 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₃ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N) (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1 + 1) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₄ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HSMul.hSMul (β := N) (HAdd.hAdd (α := ℕ) 2 1) ((Q : (a : M) → N) x : N) +
            HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₅ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N) +
              HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N) +
            HSMul.hSMul (α := ℕ) (β := N) 1 ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
rw₆ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N)
            (HAdd.hAdd (β := N) (HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) x : N)) =
    (Q : (a : M) → N) x
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    ((Q : (a : M) → N) x : N)
have rw₇ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    (HSub.hSub (β := N)
      (HAdd.hAdd (β := N) (HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x : N)) =
  (Q : (a : M) → N) x
Tactic: rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]