-- 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
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 : ℕ
hm₁ : m₁' ∈ LinearMap.range (ι Q₁) ^ i₁n
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * ↑i₁n) • ((map f₂) m₂ * (map f₁) m₁')

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₁
  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
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 : ℕ
hm₁ : m₁' ∈ LinearMap.range (ι Q₁) ^ ↑⟨i₁n, ⋯⟩
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * ↑i₁n) • ((map f₂) m₂ * (map f₁) m₁')

Tactic:
dsimp only at *

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

Proof state:
case mem.mk.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι Q₁) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι Q₁) ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (map f₁) (x✝ + y✝) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) (x✝ + y✝))

Tactic:
rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]

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:
dsimp only at *

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

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

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₂ =>
  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