-- 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₁ m₁' : CliffordAlgebra Q₁
i₁n i_1 : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i_1
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n i : ℕ
x₂ : CliffordAlgebra Q₂
_hx₂ : x₂ ∈ (ι Q₂).range ^ i
ih₂ :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (β := ZMod 2) (-1) (↑i : ZMod 2) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
v₂ : M₂
mem :
  HMul.hMul (α := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) v₂) :
          CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ)) =
    HPow.hPow (α := ℤˣ) (β := ZMod 2) (-1) (↑i.succ : ZMod 2) •
      HMul.hMul (β := CliffordAlgebra Qₙ)
        (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) v₂) :
            CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ))
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
mem₁ :
  HMul.hMul (α := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ)) =
    HPow.hPow (α := ℤˣ) (β := ZMod 2) (-1) (↑i.succ : ZMod 2) •
      HMul.hMul (β := CliffordAlgebra Qₙ)
        (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ))
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
mem₂ :
  HMul.hMul (α := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ)) =
    HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ZMod 2) (↑i : ZMod 2) 1) •
      HMul.hMul (β := CliffordAlgebra Qₙ)
        (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ))
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ)
          (HMul.hMul (α := CliffordAlgebra Q₂) ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) v₂ : CliffordAlgebra Q₂) x₂) :
        CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (β := ZMod 2) (-1) (↑i.succ : ZMod 2) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ)
            (HMul.hMul (α := CliffordAlgebra Q₂) ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) v₂ : CliffordAlgebra Q₂) x₂) :
          CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
have mem₃ : HMul.hMul (β := CliffordAlgebra Qₙ)
    (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ))
    ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ) =
  HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ZMod 2) (↑i : ZMod 2) 1) •
    HMul.hMul (β := CliffordAlgebra Qₙ)
      (HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₂ : (a : M₂) → N) v₂) : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) x₂ : CliffordAlgebra Qₙ))
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
Tactic: rw [map_mul, map_apply_ι, Nat.cast_succ, ← mul_assoc,
            ι_mul_ι_comm_of_isOrtho (hf _ _), neg_mul, mul_assoc, ih₂, mul_smul_comm,
            ← mul_assoc, ← Units.neg_smul, uzpow_add, uzpow_one, mul_neg_one]