awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
mem :
  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ₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) i₂ •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
⊢ HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i : 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ₙ) m₂ : CliffordAlgebra Qₙ))
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x₁ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i : ZMod 2)) •
      HMul.hMul (β := CliffordAlgebra Qₙ)
        (HPow.hPow (α := ℤˣ) (-1) i₂ •
          HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
            ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
            ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ))
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x₁ : CliffordAlgebra Qₙ)

Tactic:
congr 2
-- 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
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
mem :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) i₂ •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)
mem₁ :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ) =
    HSMul.hSMul (β := CliffordAlgebra Qₙ) (HPow.hPow (α := ℤˣ) (-1) i₂) 0
mem₂ : 0 = HSMul.hSMul (β := CliffordAlgebra Qₙ) (HPow.hPow (α := ℤˣ) (-1) i₂) 0
mem₃ mem₄ : Eq (α := CliffordAlgebra Qₙ) 0 0
⊢ 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ₙ) 0 : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) i₂ •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)

Tactic:
rw [map_zero, zero_mul, mul_zero, smul_zero]

Premises used: MulZeroClass.zero_mul, smul_zero, map_zero, MulZeroClass.mul_zero
-- 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₁
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
i₂' : { n : ℕ // (↑n : ZMod 2) = i₂ }
m₂' : CliffordAlgebra Q₂
hm₂ : m₂' ∈ (ι Q₂).range ^ (↑i₂' : ℕ)
mem :
  ∀ (i₂n : ℕ)
    (hm₂ :
      m₂' ∈
        (ι Q₂).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑i₂n : ZMod 2)) i₂n ⋯) : ℕ)),
    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ₙ) m₂' : CliffordAlgebra Qₙ) =
      HPow.hPow (α := ℤˣ) (β := ZMod 2) (-1) (↑i₂n : ZMod 2) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂' : 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ₙ) m₂' : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) i₂ •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂' : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)

Tactic:
obtain ⟨i₂n, rfl⟩ := i₂'

Premises used: rfl
-- 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₁ m₁' : CliffordAlgebra Q₁
i₁n i_1 : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i_1
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
m₂ : CliffordAlgebra Q₂
hm₂ : m₂ ∈ (ι Q₂).range
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ₙ)
mem :
  ∀ (v₂ : M₂),
    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ₙ)
⊢ 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ₙ) (m₂ * 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ₙ) (m₂ * x₂) : CliffordAlgebra Qₙ)
        ((ι Qₙ : (a : N) → CliffordAlgebra Qₙ) ((f₁ : (a : M₁) → N) v₁) : CliffordAlgebra Qₙ)

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

Premises used: rfl
-- 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₁ 0
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ HPow.hPow (α := ℤˣ) (-1) (i₂ * 0) •
      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ₙ) =
    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:
simp
-- 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₁
hm₂ : m₂ ∈ evenOdd Q₂ 0
⊢ HPow.hPow (α := ℤˣ) (-1) (0 * i₁) •
      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ₙ) =
    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:
simp
-- 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₂
hm₁ : m₁ ∈ evenOdd Q₁ 1
hm₂ : m₂ ∈ evenOdd Q₂ 1
⊢ 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ₙ) =
    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:
simp [map_mul_map_of_isOrtho_of_mem_evenOdd _ _ hf _ _ hm₁ hm₂]

Premises used: CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd
-- 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
m : M₁ × M₂
⊢ HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
            ((Q₁ : (a : M₁) → R) m.1) :
          evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m.2 :
          evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) +
      HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        (-(ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m.2 :
          evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
            ((Q₂ : (a : M₂) → R) m.2) :
          evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) =
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₁ : (a : M₁) → R) m.1) :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) : (a : R) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) ((Q₂ : (a : M₂) → R) m.2) :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
rw :
  (LinearMap.coprod
          (AlgHom.toLinearMap (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
          (AlgHom.toLinearMap (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) :
        (a : M₁ × M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (m₁, m₂) =
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m₁ ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m₂ : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
⊢ (ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) =
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m₁ ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m₂ : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
rw [ofProd, lift_ι_apply]

Premises used: CliffordAlgebra.lift_ι_apply, CliffordAlgebra.ofProd
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (LinearMap.coprod
          (AlgHom.toLinearMap (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
          (AlgHom.toLinearMap (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) :
        (a : M₁ × M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (m₁, m₂) =
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m₁ ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m₂ : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
a :
  ∀ (m : M₁),
    Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂ :
            (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
                ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
a₁ :
  ∀ (m : M₂),
    Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂ :
            (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
                ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
⊢ (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
a :
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m, 0))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m, 0) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
a :
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha :
  ∀ (x : M₁),
    Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                  (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
              ι Q₁ :
            (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((AlgHom.toLinearMap
                (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                  (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
              ι Q₁ :
            (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
hb :
  ∀ (x : M₂),
    Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                  (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
              ι Q₂ :
            (a : M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((AlgHom.toLinearMap
                (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                  (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
              ι Q₂ :
            (a : M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
⊢ (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x : M₁
⊢ Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
            ι Q₁ :
          (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((AlgHom.toLinearMap
              (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
            ι Q₁ :
          (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
simp