-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
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₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n : ℕ
hm₁ : m₁' ∈ (ι Q₁).range ^ i₁n
mem :
  ∀ (r : R),
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ)
            ((algebraMap R (CliffordAlgebra Q₁) : (a : R) → CliffordAlgebra Q₁) r) :
          CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
      HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑0 : ZMod 2)) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ)
              ((algebraMap R (CliffordAlgebra Q₁) : (a : R) → CliffordAlgebra Q₁) r) :
            CliffordAlgebra Qₙ)
mem₁ :
  ∀ (x y : CliffordAlgebra Q₁) (i : ℕ),
    x ∈ (ι Q₁).range ^ i →
      y ∈ (ι Q₁).range ^ i →
        ∀
          (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 : ZMod 2)) •
                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 : ZMod 2)) •
                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 : ZMod 2)) •
              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ₙ)
mem₂ :
  ∀ (m₁ : CliffordAlgebra Q₁) (hm₁ : m₁ ∈ (ι Q₁).range) (i : ℕ) (x₁ : CliffordAlgebra Q₁) (_hx₁ : x₁ ∈ (ι Q₁).range ^ i)
    (ih₁ :
      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 : ZMod 2)) •
          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₁ * x₁) : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
      HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i.succ : ZMod 2)) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) (m₁ * 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ₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i₁n : ZMod 2)) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) m₁' : CliffordAlgebra Qₙ)

Tactic:
induction hm₁ using Submodule.pow_induction_on_left' with
    | algebraMap =>
      rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
    | add _ _ _ _ _ ihx ihy =>
      rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
    | mem_mul m₁ hm₁ i x₁ _hx₁ ih₁ =>
      obtain ⟨v₁, rfl⟩ := hm₁
      -- This is the first interesting goal.
      rw [map_mul, mul_assoc, ih₁, mul_smul_comm, map_apply_ι, Nat.cast_succ, mul_add_one,
        uzpow_add, mul_smul, ← mul_assoc, ← mul_assoc, ← smul_mul_assoc ((-1) ^ i₂)]
      clear ih₁
      congr 2
      induction hm₂ using Submodule.iSup_induction' with
      | zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
      | add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
      | mem i₂' m₂' hm₂ =>
        clear m₂
        obtain ⟨i₂n, rfl⟩ := i₂'
        dsimp only at *
        induction hm₂ using Submodule.pow_induction_on_left' with
        | algebraMap =>
          rw [AlgHom.commutes, Nat.cast_zero, uzpow_zero, one_smul, Algebra.commutes]
        | add _ _ _ _ _ ihx ihy =>
          rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
        | mem_mul m₂ hm₂ i x₂ _hx₂ ih₂ =>
          obtain ⟨v₂, rfl⟩ := hm₂
          -- This is the second interesting goal.
          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]

Premises used: add_mul, Nat.cast_succ, uzpow_zero, Algebra.algebraMap, uzpow_one, MulZeroClass.zero_mul, mul_assoc, smul_zero, map_zero, map_add, CliffordAlgebra.map_apply_ι, smul_mul_assoc, one_smul, MulZeroClass.mul_zero, map_mul, uzpow_add, Units.neg_smul, HPow.hPow, AlgHom.commutes, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, mul_smul_comm, mul_add, neg_mul, mul_neg_one, Nat.cast_zero, mul_add_one, OfNat.ofNat, SemigroupAction.mul_smul, Algebra.commutes, smul_add, Neg.neg, rfl