-- 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:
case mem.mk.mem_mul.intro.e_a.e_a.mem.mk.algebraMap
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 : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) ((algebraMap R (CliffordAlgebra Q₂)) r✝) =
    (-1) ^ ↑0 • ((map f₂) ((algebraMap R (CliffordAlgebra Q₂)) r✝) * (ι Qₙ) (f₁ v₁))

Tactic:
rw [AlgHom.commutes, Nat.cast_zero, uzpow_zero, one_smul, Algebra.commutes]

Result:
no goals

Proof state:
case mem.mk.mem_mul.intro.e_a.e_a.mem.mk
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 : ℕ
hm₂ : m₂' ∈ LinearMap.range (ι Q₂) ^ i₂n
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) m₂' = (-1) ^ ↑i₂n • ((map f₂) m₂' * (ι Qₙ) (f₁ v₁))

Tactic:
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
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₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ LinearMap.range (ι Q₁) ^ i
v₁ : M₁
i₂' : { n // ↑n = i₂ }
m₂' : CliffordAlgebra Q₂
hm₂ : m₂' ∈ LinearMap.range (ι Q₂) ^ ↑i₂'
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) m₂' = (-1) ^ i₂ • ((map f₂) m₂' * (ι Qₙ) (f₁ v₁))

Tactic:
clear m₂

Result:
case mem.mk.mem_mul.intro.e_a.e_a.mem
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₁
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ LinearMap.range (ι Q₁) ^ i
v₁ : M₁
i₂' : { n // ↑n = i₂ }
m₂' : CliffordAlgebra Q₂
hm₂ : m₂' ∈ LinearMap.range (ι Q₂) ^ ↑i₂'
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) m₂' = (-1) ^ i₂ • ((map f₂) m₂' * (ι Qₙ) (f₁ v₁))

Proof state:
case mem.mk.mem_mul.intro.e_a.e_a.mem.mk.mem_mul
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 : ℕ
m₂ : CliffordAlgebra Q₂
hm₂ : m₂ ∈ LinearMap.range (ι Q₂)
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₁))
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) (m₂ * x₂) = (-1) ^ ↑i.succ • ((map f₂) (m₂ * x₂) * (ι Qₙ) (f₁ v₁))

Tactic:
obtain ⟨v₂, rfl⟩ := hm₂

Result:
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₁))

Proof state:
case mem.mk.mem_mul
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₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n : ℕ
m₁ : CliffordAlgebra Q₁
hm₁ : m₁ ∈ LinearMap.range (ι Q₁)
i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ LinearMap.range (ι Q₁) ^ i
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
⊢ (map f₁) (m₁ * x₁) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * (map f₁) (m₁ * x₁))

Tactic:
obtain ⟨v₁, rfl⟩ := hm₁

Result:
case 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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ LinearMap.range (ι Q₁) ^ i
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (map f₁) ((ι Q₁) v₁ * x₁) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * (map f₁) ((ι Q₁) v₁ * x₁))