-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
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)
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)
x y : M
simp_rw :
  HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q' : (a : M) → N) (x + y) : N) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw₁ :
  HAdd.hAdd (β := 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 + y) : N) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp_rw₂ :
  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) (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)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N) +
        HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N))
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) (x + y) =
    HAdd.hAdd (β := N)
      (HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) x +
        HAdd.hAdd (α := (a : M) → N) (β := (a : M) → N) (⇑Q : (a : M) → N) (⇑Q' : (a : M) → N) y)
      ((((B + B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
have simp_rw₃ : 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) (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) x : N) +
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q' : (a : M) → N) y : N) +
    HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B' : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
Tactic: simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_comm]