-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
x y : M →ₗ[R] A
_hx :
  Membership.mem (γ := Submodule R (M →ₗ[R] A))
    (Submodule.span R
      {f' : M →ₗ[R] A |
        ∃ (x : A) (m₂ : M),
          f' =
            (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
              (LinearMap.mulRight R x)})
    x
_hy :
  Membership.mem (γ := Submodule R (M →ₗ[R] A))
    (Submodule.span R
      {f' : M →ₗ[R] A |
        ∃ (x : A) (m₂ : M),
          f' =
            (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
              (LinearMap.mulRight R x)})
    y
ihx :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
ihy :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (a : M) → A) m₁ : A)
snd :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
snd₁ :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m₁ : A) ((y : (a : M) → A) m₁ : A))
snd₂ :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) +
      HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m₁ : A) ((y : (a : M) → A) m₁ : A))
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x + y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
have snd₃ : HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) +
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((y : (a : M) → A) m : A) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A) +
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (a : M) → A) m₁ : A)
Tactic: rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]