awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
rw :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₁ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₂ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    (star
        ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
          ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
have rw₃ : star q =
  star
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
      ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q))
Tactic: rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
rw :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₁ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₂ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    (star
        ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
          ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₃ :
  star q =
    star
      ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q))
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
have rw₄ : star q = star q
Tactic: rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw : HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₁ : HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₂ : HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₃ : HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₄ : HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
    (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
    ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₅ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₆ : (r₁ * r₂) •
    HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
      ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₆ :
  (r₁ * r₂) •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
        ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₇ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
    ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) ((0 : (a : R) → R) 1)) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₆ :
  (r₁ * r₂) •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
        ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₇ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) ((0 : (a : R) → R) 1)) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₈ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
    ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) 0) =
  0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]