-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p q : Module.Dual R M × M
rw :
  ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₁ :
  (p.1 + q.1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₂ :
  (p.1 + q.1 : (a : M) → R) (p.2 + q.2) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) (p.2 + q.2) : R) ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₄ :
  HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R))
      ((q.1 : (a : M) → R) (p.2 + q.2) : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₅ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
    HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)
rw₆ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
    HAdd.hAdd (β := R)
      (HAdd.hAdd (α := R) ((p.1 : (a : M) → R) p.2 : R)
        (HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R)))
      ((q.1 : (a : M) → R) q.2 : R)
rw₇ :
  HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R) +
      HAdd.hAdd (α := R) (β := R) ((q.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R) =
    HAdd.hAdd (β := R)
      (HAdd.hAdd (α := R) ((p.1 : (a : M) → R) p.2 : R)
        (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) q.2 : R) ((q.1 : (a : M) → R) p.2 : R)))
      ((q.1 : (a : M) → R) q.2 : R)
⊢ ((p + q).1 : (a : M) → R) (p + q).2 =
    HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((q.1 : (a : M) → R) q.2 : R))
      ((((LinearMap.dualProd R M : (a : Module.Dual R M × M) → Module.Dual R M × M →ₗ[R] R) p :
              Module.Dual R M × M →ₗ[R] R) :
            (a : Module.Dual R M × M) → R)
          q :
        R)
have rw₈ : HAdd.hAdd (β := R)
    (HAdd.hAdd (β := R) (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) p.2 : R) ((p.1 : (a : M) → R) q.2 : R))
      ((q.1 : (a : M) → R) p.2 : R))
    ((q.1 : (a : M) → R) q.2 : R) =
  HAdd.hAdd (β := R)
    (HAdd.hAdd (α := R) ((p.1 : (a : M) → R) p.2 : R)
      (HAdd.hAdd (α := R) (β := R) ((p.1 : (a : M) → R) q.2 : R) ((q.1 : (a : M) → R) p.2 : R)))
    ((q.1 : (a : M) → R) q.2 : R)
Tactic: rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
        map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
        add_assoc]