-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
a :
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        (HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
a₁ :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
    (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
a₂ :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
    (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a₃ : HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, 0) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
  (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
Tactic: rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
      map_zero, zero_add]