awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
rw : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = r₁ • e0 Q * r₂ • e0 Q
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q
have rw₁ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = (r₁ * r₂) • (e0 Q * e0 Q)
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
rw : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = r₁ • e0 Q * r₂ • e0 Q
rw₁ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = (r₁ * r₂) • (e0 Q * e0 Q)
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q
have rw₂ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 =
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) (-1)
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
rw : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = r₁ • e0 Q * r₂ • e0 Q
rw₁ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = (r₁ * r₂) • (e0 Q * e0 Q)
rw₂ :
  -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 =
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) (-1)
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q
have rw₃ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 =
  -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
        Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
          CliffordAlgebra (Q' Q))
        ⋯) =
    HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)
have simp_rw : (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
    (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
      Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
      (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)))
      sorry) =
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
    HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)
Tactic: simp_rw [toEven_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw : HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
    HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
  (ι Q : (a : M) → CliffordAlgebra Q) m
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw₁ : HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
    HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
  (ι Q : (a : M) → CliffordAlgebra Q) m
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw₂ : HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
    HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
  (ι Q : (a : M) → CliffordAlgebra Q) m
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw₃ : HMul.hMul (β := CliffordAlgebra Q) (HAdd.hAdd (α := CliffordAlgebra Q) 0 1)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
  (ι Q : (a : M) → CliffordAlgebra Q) m
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₃ :
  HMul.hMul (β := CliffordAlgebra Q) (HAdd.hAdd (α := CliffordAlgebra Q) 0 1)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw₄ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
  (ι Q : (a : M) → CliffordAlgebra Q) m
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₃ :
  HMul.hMul (β := CliffordAlgebra Q) (HAdd.hAdd (α := CliffordAlgebra Q) 0 1)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₄ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
have rw₅ : Eq (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q)))
have algebraMap : ∀ (r : R),
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra (Q' Q)))
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
  | ι m =>
    simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
      reverse_ι, neg_e0_mul_v, map_neg]
  | mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
  | add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)))) :
        CliffordAlgebra (Q' Q))
      ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
          CliffordAlgebra (Q' Q)))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q)))
have ι : ∀ (m : M),
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
        CliffordAlgebra (Q' Q)))
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
  | ι m =>
    simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
      reverse_ι, neg_e0_mul_v, map_neg]
  | mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
  | add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ Eq (α := ↥(even Q'))
    ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
have simp_rw : Eq (α := ↥(even Q'))
  (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m : ↥(even Q'))
  ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
simp_rw :
  Eq (α := ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
⊢ Eq (α := ↥(even Q'))
    ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
have simp_rw₁ : Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q' : (a : M) → R) m) : ↥(even Q'))
  ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]