-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ HMul.hMul (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((LinearMap.coprod
              (AlgHom.toLinearMap (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
                (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
              (AlgHom.toLinearMap (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
                (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) :
            (a : M₁ × M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          m :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((LinearMap.coprod
              (AlgHom.toLinearMap (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
                (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
              (AlgHom.toLinearMap (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
                (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) :
            (a : M₁ × M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          m :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((QuadraticMap.prod Q₁ Q₂ : (a : M₁ × M₂) → R) m)
have simp_rw : HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₁ : (a : M₁) → R) m.1) :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m.2 :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) +
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (-(ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m.2 :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₂ : (a : M₂) → R) m.2) :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) =
  HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₁ : (a : M₁) → R) m.1) :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₂ : (a : M₂) → R) m.2) :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
Tactic: simp_rw [LinearMap.coprod_apply, LinearMap.coe_comp, Function.comp_apply,
        AlgHom.toLinearMap_apply, QuadraticMap.prod_apply, Submodule.coe_subtype,
        GradedTensorProduct.includeLeft_apply, GradedTensorProduct.includeRight_apply, map_add,
        add_mul, mul_add, GradedTensorProduct.algebraMap_def,
        GradedTensorProduct.tmul_one_mul_one_tmul, GradedTensorProduct.tmul_one_mul_coe_tmul,
        GradedTensorProduct.tmul_coe_mul_one_tmul, GradedTensorProduct.tmul_coe_mul_coe_tmul,
        LinearMap.codRestrict_apply, one_mul, uzpow_one, Units.neg_smul, one_smul, ι_sq_scalar,
        mul_one, ← GradedTensorProduct.algebraMap_def, ← GradedTensorProduct.algebraMap_def']