awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
zero :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
zero₁ :
  0 =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
have zero₂ : 0 = HSMul.hSMul (β := CliffordAlgebra Qₙ) (HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁)) 0
Tactic: rw [map_zero, zero_mul, mul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
zero :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
zero₁ :
  0 =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
zero₂ : 0 = HSMul.hSMul (β := CliffordAlgebra Qₙ) (HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁)) 0
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
have zero₃ : Eq (α := CliffordAlgebra Qₙ) 0 0
Tactic: rw [map_zero, zero_mul, mul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
i₁' : { n : ℕ // (↑n : ZMod 2) = i₁ }
m₁' : CliffordAlgebra Q₁
hm₁ : m₁' ∈ (ι Q₁).range ^ (↑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ₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * 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ₙ)
have mem : ∀ (i₁n : ℕ)
  (hm₁ :
    m₁' ∈ (ι Q₁).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑i₁n : ZMod 2)) i₁n sorry) : ℕ)),
  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: obtain ⟨i₁n, rfl⟩ := i₁'
Cleared hypotheses: i₁, i₁', hm₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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 : ℕ
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ₙ)
have mem : HMul.hMul (α := 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ₙ)
      ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
Tactic: rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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 : ℕ
r : R
mem :
  HMul.hMul (α := 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ₙ)
        ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
⊢ 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ₙ)
have mem₁ : HMul.hMul (α := 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) •
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
      ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
Tactic: rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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 : ℕ
r : R
mem :
  HMul.hMul (α := 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ₙ)
        ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
mem₁ :
  HMul.hMul (α := 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) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
⊢ 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ₙ)
have mem₂ : HMul.hMul (α := 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 (α := ℤˣ) (β := ZMod 2) (-1) 0 •
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
      ((algebraMap R (CliffordAlgebra Qₙ) : (a : R) → CliffordAlgebra Qₙ) r : CliffordAlgebra Qₙ)
Tactic: rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁_1 : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
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ₙ)
      ((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ₙ)
have mem : ∀ (v₁ : M₁),
  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ₙ)
      ((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ₙ)
            (HMul.hMul (α := CliffordAlgebra Q₁) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) v₁ : CliffordAlgebra Q₁) x₁) :
          CliffordAlgebra Qₙ)
Tactic: obtain ⟨v₁, rfl⟩ := hm₁
Cleared hypotheses: m₁, hm₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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
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ₙ)
v₁ : M₁
⊢ 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ₙ)
      ((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ₙ)
            (HMul.hMul (α := CliffordAlgebra Q₁) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) v₁ : CliffordAlgebra Q₁) x₁) :
          CliffordAlgebra Qₙ)
have mem : 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: 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₂)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁
⊢ 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ₙ)
have 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ₙ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
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₁
⊢ 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ₙ)
have 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ₙ)
Tactic: rw [map_zero, zero_mul, mul_zero, smul_zero]