-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (a • x + y) : N) ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₁ :
  HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (a • x) : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N))
        ((Q : (a : M) → N) (a • x) : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₂ :
  HSub.hSub (β := N)
      (HAdd.hAdd (β := N)
          (HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) (a • x) : M →ₗ[R] N) : (a : M) → N) y : N) -
        HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
simp_rw₃ :
  HSub.hSub (β := N)
      (HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N) +
          HSMul.hSMul (β := N) a ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) -
        HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    a •
      HSub.hSub (β := N)
        (HSub.hSub (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
have simp_rw₄ : HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N) +
      HSMul.hSMul (β := N) a ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) -
    HAdd.hAdd (β := N) (HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)) ((Q : (a : M) → N) y : N) =
  a •
    (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) -
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
Tactic: simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]