-- 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
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
x y : CliffordAlgebra Q₁
hx :
  Membership.mem (γ := Submodule R (CliffordAlgebra Q₁))
    (⨆ (i : { n : ℕ // (↑n : ZMod 2) = i₁ }), (ι Q₁).range ^ (↑i : ℕ)) x
hy :
  Membership.mem (γ := Submodule R (CliffordAlgebra Q₁))
    (⨆ (i : { n : ℕ // (↑n : ZMod 2) = i₁ }), (ι Q₁).range ^ (↑i : ℕ)) y
ihx :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
ihy :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
add :
  HMul.hMul (β := CliffordAlgebra Qₙ)
      (HAdd.hAdd (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        (HAdd.hAdd (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
add₁ :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) +
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        (HAdd.hAdd (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
add₂ :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) +
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
add₃ :
  HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
add₄ :
  HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
      HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ))
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) (x + y) : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) (x + y) : CliffordAlgebra Qₙ)
have add₅ : HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ) =
  HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x : CliffordAlgebra Qₙ) +
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) y : CliffordAlgebra Qₙ)
Tactic: rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]