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
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
mul₁ : x₁ * (y * x₂) = y * (x₁ * x₂)
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
have mul₂ : x₁ * y * x₂ = y * (x₁ * x₂)
Tactic: rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
mul₁ : x₁ * (y * x₂) = y * (x₁ * x₂)
mul₂ : x₁ * y * x₂ = y * (x₁ * x₂)
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
have mul₃ : y * x₁ * x₂ = y * (x₁ * x₂)
Tactic: rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
mul₁ : x₁ * (y * x₂) = y * (x₁ * x₂)
mul₂ : x₁ * y * x₂ = y * (x₁ * x₂)
mul₃ : y * x₁ * x₂ = y * (x₁ * x₂)
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
have mul₄ : y * x₁ * x₂ = y * x₁ * x₂
Tactic: rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : CliffordAlgebra (R := R) (M := Unit) 0
⊢ x * y = y * x
have algebraMap : ∀ (r : R),
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
      y =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
      ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
        y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
⊢ x * y = y * x
have ι : ∀ (x : Unit),
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0) y =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
      ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
        y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0) y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
⊢ x * y = y * x
have add : ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0) (hx₁ : x₁ * y = y * x₁) (hx₂ : x₂ * y = y * x₂),
  (x₁ + x₂) * y = y * (x₁ + x₂)
Tactic: induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
        y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0) y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
add :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0) (hx₁ : x₁ * y = y * x₁) (hx₂ : x₂ * y = y * x₂),
    (x₁ + x₂) * y = y * (x₁ + x₂)
⊢ x * y = y * x
have mul : ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0) (hx₁ : x₁ * y = y * x₁) (hx₂ : x₂ * y = y * x₂),
  x₁ * x₂ * y = y * (x₁ * x₂)
Tactic: induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : Unit
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
have ι : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
  ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((0 : (a : Unit) → CliffordAlgebra 0) x) :
    CliffordAlgebra (R := R) (M := Unit) 0)
  ((0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : Unit
ι :
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
have ι₁ : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0) ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) 0) 0
Tactic: rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : Unit
ι :
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
ι₁ :
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0) ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) 0)
    0
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
have ι₂ : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0) 0 0
Tactic: rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
have mul : HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
have mul₁ : HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
have mul₂ : HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₂ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
have mul₃ : x₁ * x₂ = x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂
have add : HAdd.hAdd (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
  x₁ + x₂
Tactic: rw [reverse.map_add, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
add :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂
have add₁ : HAdd.hAdd (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
  x₁ + x₂
Tactic: rw [reverse.map_add, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
add :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ + x₂
add₁ :
  HAdd.hAdd (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂
have add₂ : x₁ + x₂ = x₁ + x₂
Tactic: rw [reverse.map_add, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : CliffordAlgebra (R := R) (M := Unit) 0
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x = x
have algebraMap : ∀ (r : R),
  Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
      CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x = x
have ι : ∀ (x : Unit),
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x = x
have mul : ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
  (hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁)
  (hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂),
  (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
x : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
mul :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
    (hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁)
    (hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂),
    (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x = x
have add : ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
  (hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁)
  (hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂),
  (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0 →ₐ[R] CliffordAlgebra (R := R) (M := Unit) 0) involute
    (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0))
have a : ∀ (x : Unit),
  Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((AlgHom.toLinearMap involute ∘ₗ ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0 : (a : Unit) → CliffordAlgebra 0)
        x :
      CliffordAlgebra (R := R) (M := Unit) 0)
Tactic: ext