awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
mul₂ :
  HMul.hMul (β := CliffordAlgebra Q) x₁
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
    x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (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:
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 add : HAdd.hAdd (α := 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_add, 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₂
add :
  HAdd.hAdd (α := 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 add₁ : HAdd.hAdd (β := CliffordAlgebra Q) x₁ ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
  x₁ + x₂
Tactic: rw [reverse.map_add, 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₂
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₁ : CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
    x₁ + x₂
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) x₁
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x₂ : CliffordAlgebra Q) =
    x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (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:
x : CliffordAlgebra Q
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have algebraMap : ∀ (r : ℝ),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [reverse_ι]
  | 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:
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : ℝ),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have ι : ∀ (x : ℝ),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [reverse_ι]
  | 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:
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : ℝ),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r : CliffordAlgebra Q)
ι :
  ∀ (x : ℝ),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have mul : ∀ (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₂
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [reverse_ι]
  | 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:
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : ℝ),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap ℝ (CliffordAlgebra Q) : (a : ℝ) → CliffordAlgebra Q) r : CliffordAlgebra Q)
ι :
  ∀ (x : ℝ),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
mul :
  ∀ (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₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have add : ∀ (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₂
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [reverse_ι]
  | 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:
c : ℂ
⊢ Eq (α := ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
have rw : Eq (α := ℂ)
  ((toComplex : (a : CliffordAlgebra Q) → ℂ)
      ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
    ℂ)
  ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
        CliffordAlgebra Q) :
    ℂ)
Tactic: rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : ℂ
rw :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
⊢ Eq (α := ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
have rw₁ : Eq (α := ℂ)
  ((toComplex : (a : CliffordAlgebra Q) → ℂ)
      ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
    ℂ)
  ((toComplex : (a : CliffordAlgebra Q) → ℂ)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
        CliffordAlgebra Q) :
    ℂ)
Tactic: rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : ℂ
rw :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
rw₁ :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
⊢ Eq (α := ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
have rw₂ : Eq (α := ℂ)
  ((toComplex : (a : CliffordAlgebra Q) → ℂ)
      ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
    ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
        ℂ) :
    ℂ)
Tactic: rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : ℂ
rw :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
rw₁ :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
rw₂ :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ)
        ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
          ℂ) :
      ℂ)
⊢ Eq (α := ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
have rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
        ℂ) :
    ℂ)
Tactic: rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
c : ℂ
rw :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
rw₁ :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
rw₂ :
  Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ)
        ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
          ℂ) :
      ℂ)
rw₃ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ)
        ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
          ℂ) :
      ℂ)
⊢ Eq (α := ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((ofComplex : (a : ℂ) → CliffordAlgebra Q) ((starRingEnd ℂ : (a : ℂ) → ℂ) c) : CliffordAlgebra Q) :
      ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c) :
          CliffordAlgebra Q) :
      ℂ)
have rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ)
Tactic: rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) =
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) c₁ 1 +
      HSMul.hSMul (α := R) (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) 0
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
have rw : (algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
    (c₁ * HMul.hMul (α := R) (1, 0).1 (1, 0).1 + c₂ * HMul.hMul (α := R) (1, 0).2 (1, 0).2) =
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) c₁ :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (HSMul.hSMul (α := R) (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) 0
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)))
Tactic: rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) =
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) c₂ 1
have rw : Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
  ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
      (c₁ * HMul.hMul (α := R) (0, 1).1 (0, 1).1 + c₂ * HMul.hMul (α := R) (0, 1).2 (0, 1).2) :
    CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
  ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) c₂ :
    CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
Tactic: rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) =
    HSMul.hSMul (α := R) (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) 0
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) -
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
have rw : Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
  ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
      (HSub.hSub (β := R)
        (HSub.hSub (α := R) (β := R) ((Q c₁ c₂ : (a : R × R) → R) (HAdd.hAdd (α := R × R) (0, 1) (1, 0)) : R)
          ((Q c₁ c₂ : (a : R × R) → R) (0, 1) : R))
        ((Q c₁ c₂ : (a : R × R) → R) (1, 0) : R)) :
    CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
  (0 : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
Tactic: rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ r : R
v : R × R
⊢ { re := 0, imI := (r • v).1, imJ := (r • v).2, imK := 0 } =
    HSMul.hSMul (α := R) (β := ℍ[R,c₁,c₂]) ((RingHom.id R : (a : R) → R) r : R)
      { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }
have dsimp : Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
  { re := r * 0, imI := r * v.1, imJ := r * v.2, imK := r * 0 }
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ r : R
v : R × R
⊢ Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
    { re := r * 0, imI := r * v.1, imJ := r * v.2, imK := r * 0 }
have rw : Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
  { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ HMul.hMul (α := ℍ[R,c₁,c₂]) (β := ℍ[R,c₁,c₂])
      (({ toFun := fun (v : R × R) ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }, map_add' := ⋯,
              map_smul' := ⋯ : R × R →ₗ[R] ℍ[R,c₁,c₂] } :
            (a : R × R) → ℍ[R,c₁,c₂])
          v :
        ℍ[R,c₁,c₂])
      (({ toFun := fun (v : R × R) ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }, map_add' := ⋯,
              map_smul' := ⋯ : R × R →ₗ[R] ℍ[R,c₁,c₂] } :
            (a : R × R) → ℍ[R,c₁,c₂])
          v :
        ℍ[R,c₁,c₂]) =
    (algebraMap R ℍ[R,c₁,c₂] : (a : R) → ℍ[R,c₁,c₂]) ((Q c₁ c₂ : (a : R × R) → R) v)
have dsimp : Eq (α := ℍ[R,c₁,c₂])
  { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
    imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
    imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
    imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 }
  (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ Eq (α := ℍ[R,c₁,c₂])
    { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
      imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
      imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
      imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 }
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
have re : re (a := c₁) (b := 0) (c := c₂)
    { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
      imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
      imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
      imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
  re (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
Tactic: ext