-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
x_1 x_2 : M₂
a :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
a₁ :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
a₂ :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
⊢ HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
have a₃ : HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
  HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
Tactic: rw [← TensorProduct.tmul_add, h, h, h]