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
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0 →ₐ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
      ((lift 0 :
          (a :
              { f : Unit →ₗ[R] R //
                ∀ (m : Unit),
                  (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                    (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
            CliffordAlgebra 0 →ₐ[R] R)
        (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
          ∀ (m : Unit),
            HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
              (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
          0 ⋯)))
    (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0))
have a : Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
  (AlgHom.toLinearMap
      (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
        ((lift 0 :
            (a :
                { f : Unit →ₗ[R] R //
                  ∀ (m : Unit),
                    (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                      (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
              CliffordAlgebra 0 →ₐ[R] R)
          (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
            ∀ (m : Unit),
              HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
            0 sorry))) ∘ₗ
    ι 0)
  (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
          ((lift 0 :
              (a :
                  { f : Unit →ₗ[R] R //
                    ∀ (m : Unit),
                      (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                        (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R)
            (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
              ∀ (m : Unit),
                HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                  (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
              0 ⋯))) ∘ₗ
      ι 0)
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0)
have a : Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
  (AlgHom.toLinearMap
      (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
        ((lift 0 :
            (a :
                { f : Unit →ₗ[R] R //
                  ∀ (m : Unit),
                    (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                      (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
              CliffordAlgebra 0 →ₐ[R] R)
          (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
            ∀ (m : Unit),
              HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
            0 sorry))) ∘ₗ
    0)
  (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ 0)
Tactic: rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
a :
  Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
          ((lift 0 :
              (a :
                  { f : Unit →ₗ[R] R //
                    ∀ (m : Unit),
                      (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                        (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R)
            (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
              ∀ (m : Unit),
                HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                  (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
              0 ⋯))) ∘ₗ
      0)
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ 0)
⊢ Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
          ((lift 0 :
              (a :
                  { f : Unit →ₗ[R] R //
                    ∀ (m : Unit),
                      (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                        (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R)
            (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
              ∀ (m : Unit),
                HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                  (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
              0 ⋯))) ∘ₗ
      ι 0)
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0)
have a₁ : Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) 0
  (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ 0)
Tactic: rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
a :
  Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
          ((lift 0 :
              (a :
                  { f : Unit →ₗ[R] R //
                    ∀ (m : Unit),
                      (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                        (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R)
            (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
              ∀ (m : Unit),
                HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                  (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
              0 ⋯))) ∘ₗ
      0)
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ 0)
a₁ :
  Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) 0
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ 0)
⊢ Eq (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0)
    (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0))
          ((lift 0 :
              (a :
                  { f : Unit →ₗ[R] R //
                    ∀ (m : Unit),
                      (f : (a : Unit) → R) m * (f : (a : Unit) → R) m =
                        (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R)
            (Subtype.mk (p := fun (f : Unit →ₗ[R] R) ↦
              ∀ (m : Unit),
                HMul.hMul (α := R) (β := R) ((f : (a : Unit) → R) m : R) ((f : (a : Unit) → R) m : R) =
                  (algebraMap R R : (a : R) → R) ((0 : (a : Unit) → R) m : R))
              0 ⋯))) ∘ₗ
      ι 0)
    (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0)
have a₂ : Eq.{max 1 (u_1 + 1)} (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) 0 0
Tactic: rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
r : ℝ
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((LinearMap.toSpanSingleton ℝ ℂ Complex.I : (a : ℝ) → ℂ) r : ℂ)
      ((LinearMap.toSpanSingleton ℝ ℂ Complex.I : (a : ℝ) → ℂ) r : ℂ) =
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Q : (a : ℝ) → ℝ) r : ℝ)
have dsimp : (↑r : ℂ) * Complex.I * ((↑r : ℂ) * Complex.I) = (↑(-(r * r)) : ℂ)
Tactic: dsimp [LinearMap.toSpanSingleton, LinearMap.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
r : ℝ
⊢ (↑r : ℂ) * Complex.I * ((↑r : ℂ) * Complex.I) = (↑(-(r * r)) : ℂ)
have rw : (↑r : ℂ) * (↑r : ℂ) * (Complex.I * Complex.I) = (↑(-(r * r)) : ℂ)
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (hypothesis)
Goal:
c : CliffordAlgebra Q
⊢ Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c : ℂ) : ℂ)
have this : Eq (α := ℂ)
  ((toComplex : (a : CliffordAlgebra Q) → ℂ)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)) :
    ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) : ℂ) :
    ℂ)
Tactic: have : toComplex (involute (ι Q 1)) = conj (toComplex (ι Q 1)) := by
    simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : CliffordAlgebra Q
this :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ)
        ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) : ℂ) :
      ℂ)
⊢ Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c : ℂ) : ℂ)
have suffices : toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex
Tactic: suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by
    exact AlgHom.congr_fun this c
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : CliffordAlgebra Q
this :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ)
        ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) : ℂ) :
      ℂ)
⊢ toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex
have a : Eq (α := ℂ) (((toComplex.comp involute).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
  ((((↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1
have rw : Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) ((Q : (a : ℝ) → ℝ) 1))
  (-1)
Tactic: rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
rw :
  Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) ((Q : (a : ℝ) → ℝ) 1))
    (-1)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1
have rw₁ : Eq (α := CliffordAlgebra Q)
  ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-HMul.hMul (α := ℝ) 1 1) : CliffordAlgebra Q)
  (-1 : CliffordAlgebra Q)
Tactic: rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
rw :
  Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) ((Q : (a : ℝ) → ℝ) 1))
    (-1)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-HMul.hMul (α := ℝ) 1 1) : CliffordAlgebra Q)
    (-1 : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1
have rw₂ : Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-1)) (-1)
Tactic: rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
rw :
  Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) ((Q : (a : ℝ) → ℝ) 1))
    (-1)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-HMul.hMul (α := ℝ) 1 1) : CliffordAlgebra Q)
    (-1 : CliffordAlgebra Q)
rw₂ : Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-1)) (-1)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1
have rw₃ : Eq (α := CliffordAlgebra Q) (-(algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) 1) (-1)
Tactic: rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
rw :
  Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) ((Q : (a : ℝ) → ℝ) 1))
    (-1)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-HMul.hMul (α := ℝ) 1 1) : CliffordAlgebra Q)
    (-1 : CliffordAlgebra Q)
rw₂ : Eq (α := CliffordAlgebra Q) ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) (-1)) (-1)
rw₃ : Eq (α := CliffordAlgebra Q) (-(algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) 1) (-1)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1
have rw₄ : Eq (α := CliffordAlgebra Q) (-1) (-1)
Tactic: rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
⊢ toComplex.comp ofComplex = AlgHom.id ℝ ℂ
have h : Eq (α := ℂ) ((toComplex.comp ofComplex : (a : ℂ) → ℂ) Complex.I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) Complex.I : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q) =
    Complex.I
have h : (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) = Complex.I
Tactic: rw [ofComplex_I, toComplex_ι, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
h : (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) = Complex.I
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q) =
    Complex.I
have h₁ : HSMul.hSMul (α := ℝ) 1 Complex.I = Complex.I
Tactic: rw [ofComplex_I, toComplex_ι, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
h : (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) = Complex.I
h₁ : HSMul.hSMul (α := ℝ) 1 Complex.I = Complex.I
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q) =
    Complex.I
have h₂ : Complex.I = Complex.I
Tactic: rw [ofComplex_I, toComplex_ι, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
⊢ ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)
have a : Eq (α := CliffordAlgebra Q) (((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
  ((AlgHom.toLinearMap (AlgHom.id ℝ (CliffordAlgebra Q)) ∘ₗ ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
⊢ Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)))
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
have a : Eq (α := CliffordAlgebra Q)
  ((ofComplex : (a : ℂ) → CliffordAlgebra Q) (HSMul.hSMul (α := ℝ) 1 Complex.I) : CliffordAlgebra Q)
  ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
Tactic: rw [toComplex_ι, one_smul, ofComplex_I]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
a :
  Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q) (HSMul.hSMul (α := ℝ) 1 Complex.I) : CliffordAlgebra Q)
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)))
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
have a₁ : Eq (α := CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q)
  ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
Tactic: rw [toComplex_ι, one_smul, ofComplex_I]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
a :
  Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q) (HSMul.hSMul (α := ℝ) 1 Complex.I) : CliffordAlgebra Q)
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
a₁ :
  Eq (α := CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q)
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)))
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
have a₂ : Eq (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
Tactic: rw [toComplex_ι, one_smul, ofComplex_I]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x y : CliffordAlgebra Q
⊢ Eq (α := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (x * y) : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x) : ℂ)
have rw : HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ) =
  (CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x)
Tactic: rw [map_mul, mul_comm, map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x y : CliffordAlgebra Q
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ)
      ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ) =
    (CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x)
⊢ Eq (α := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (x * y) : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x) : ℂ)
have rw₁ : HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ) =
  (CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x)
Tactic: rw [map_mul, mul_comm, map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x y : CliffordAlgebra Q
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ)
      ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ) =
    (CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ)
      ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ) =
    (CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x)
⊢ Eq (α := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (x * y) : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x) : ℂ)
have rw₂ : HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) y : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) x : ℂ)
Tactic: rw [map_mul, mul_comm, map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x : ℝ
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
have ι : Eq (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
  ((ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: rw [reverse_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x₁ x₂ : CliffordAlgebra Q
hx₁ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ = x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x₁ * x₂) = x₁ * x₂
have mul : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x₁ x₂ : CliffordAlgebra Q
hx₁ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x₁ * x₂) = x₁ * x₂
have mul₁ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
x₁ x₂ : CliffordAlgebra Q
hx₁ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q) =
    x₁ * x₂
mul₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x₁ * x₂) = x₁ * x₂
have mul₂ : HMul.hMul (β := CliffordAlgebra Q) x₁ ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
  x₁ * x₂
Tactic: rw [reverse.map_mul, mul_comm, hx₁, hx₂]