-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
theorem map_mul_map_of_isOrtho_of_mem_evenOdd
    {i₁ i₂ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ i₁) (hm₂ : m₂ ∈ evenOdd Q₂ i₂) :
    map f₁ m₁ * map f₂ m₂ = (-1 : ℤˣ) ^ (i₂ * i₁) • (map f₂ m₂ * map f₁ m₁)

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : 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₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₁ : m₁ ∈ evenOdd Q₁ i₁
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (map f₁) m₁ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁)

Tactic:
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₁ =>
  obtain ⟨i₁n, rfl⟩ := i₁'
  dsimp only at *
  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₁
    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₂
        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]

Result:
no goals

Proof state:
case mem.mk.mem_mul.intro.e_a.e_a.mem.mk.mem_mul.intro
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : 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₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i✝ : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ LinearMap.range (ι Q₁) ^ i✝
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n i : ℕ
x₂ : CliffordAlgebra Q₂
_hx₂ : x₂ ∈ LinearMap.range (ι Q₂) ^ i
ih₂ : (ι Qₙ) (f₁ v₁) * (map f₂) x₂ = (-1) ^ ↑i • ((map f₂) x₂ * (ι Qₙ) (f₁ v₁))
v₂ : M₂
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) ((ι Q₂) v₂ * x₂) = (-1) ^ ↑i.succ • ((map f₂) ((ι Q₂) v₂ * x₂) * (ι Qₙ) (f₁ v₁))

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]

Result:
no goals