awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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)
a₂ a₃ : Eq.{max 1 (u_1 + 1)} (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) 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)

Tactic:
rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]

Premises used: LinearMap.comp_zero, CliffordAlgebraRing.ι_eq_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
r : ℝ
⊢ (Q : (a : ℝ) → ℝ) r = -(r * r)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
r : ℝ
dsimp : (↑r : ℂ) * Complex.I * ((↑r : ℂ) * Complex.I) = (↑(-(r * r)) : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((LinearMap.toSpanSingleton ℝ ℂ Complex.I : (a : ℝ) → ℂ) r : ℂ)
      ((LinearMap.toSpanSingleton ℝ ℂ Complex.I : (a : ℝ) → ℂ) r : ℂ) =
    (algebraMap ℝ ℂ : (a : ℝ) → ℂ) ((Q : (a : ℝ) → ℝ) r : ℝ)

Tactic:
dsimp [LinearMap.toSpanSingleton, LinearMap.id]

Premises used: LinearMap.id, LinearMap.toSpanSingleton
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
r : ℝ
rw : (↑r : ℂ) * (↑r : ℂ) * (Complex.I * Complex.I) = (↑(-(r * r)) : ℂ)
⊢ (↑r : ℂ) * Complex.I * ((↑r : ℂ) * Complex.I) = (↑(-(r * r)) : ℂ)

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
r : ℝ
⊢ (↑r : ℂ) * (↑r : ℂ) * (Complex.I * Complex.I) = (↑(-(r * r)) : ℂ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
r : ℝ
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) r : CliffordAlgebra Q) = r • Complex.I

Tactic:
CliffordAlgebra.lift_ι_apply _ _ r

Premises used: CliffordAlgebra.lift_ι_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : CliffordAlgebra Q
⊢ 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:
simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]

Premises used: map_neg, one_smul, CliffordAlgebraComplex.toComplex_ι, CliffordAlgebra.involute_ι, Complex.conj_I
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : CliffordAlgebra Q
⊢ 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]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : CliffordAlgebra Q
this_1 :
  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) : ℂ) :
      ℂ)
this : toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex
⊢ Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c : ℂ) : ℂ)

Tactic:
AlgHom.congr_fun this c

Premises used: AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : CliffordAlgebra Q
this_1 :
  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) : ℂ) :
      ℂ)
this : toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex
⊢ Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c : ℂ) : ℂ)

Tactic:
exact AlgHom.congr_fun this c

Premises used: AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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) : ℂ) :
      ℂ)
suffices : toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex
⊢ Eq (α := ℂ)
    ((toComplex : (a : CliffordAlgebra Q) → ℂ)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) c : CliffordAlgebra Q) :
      ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c : ℂ) : ℂ)

Tactic:
suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by
    exact AlgHom.congr_fun this c
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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) : ℂ) :
      ℂ)
a :
  Eq (α := ℂ) (((toComplex.comp involute).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
    ((((↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
⊢ toComplex.comp involute = (↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex

Tactic:
ext : 2
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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.comp involute).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
    ((((↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)

Tactic:
this
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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.comp involute).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)
    ((((↑Complex.conjAe : ℂ →ₐ[ℝ] ℂ).comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → ℂ) 1 : ℂ)

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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)
rw₄ rw₅ : Eq (α := CliffordAlgebra Q) (-1) (-1)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) =
    -1

Tactic:
rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, map_neg, map_one]

Premises used: CliffordAlgebra.ι_sq_scalar, map_neg, map_one, CliffordAlgebraComplex.Q_apply, one_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
⊢ (↑(Subtype.mk (p := fun (I' : CliffordAlgebra Q) ↦ I' * I' = -1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
            ofComplex._proof_1) :
        CliffordAlgebra Q) *
      (↑(Subtype.mk (p := fun (I' : CliffordAlgebra Q) ↦ I' * I' = -1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
            ofComplex._proof_1) :
        CliffordAlgebra Q) =
    -1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
h : Eq (α := ℂ) ((toComplex.comp ofComplex : (a : ℂ) → ℂ) Complex.I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) Complex.I : ℂ)
⊢ toComplex.comp ofComplex = AlgHom.id ℝ ℂ

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
h : (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) = Complex.I
h₁ : HSMul.hSMul (α := ℝ) 1 Complex.I = Complex.I
h₂ h₃ : Complex.I = Complex.I
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) Complex.I : CliffordAlgebra Q) =
    Complex.I

Tactic:
rw [ofComplex_I, toComplex_ι, one_smul]

Premises used: CliffordAlgebraComplex.ofComplex_I, one_smul, CliffordAlgebraComplex.toComplex_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : ℂ
⊢ (toComplex : (a : CliffordAlgebra Q) → ℂ) ((ofComplex : (a : ℂ) → CliffordAlgebra Q) c : CliffordAlgebra Q) = c

Tactic:
AlgHom.congr_fun toComplex_comp_ofComplex c

Premises used: CliffordAlgebraComplex.toComplex_comp_ofComplex, AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
a :
  Eq (α := CliffordAlgebra Q) (((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
    ((AlgHom.toLinearMap (AlgHom.id ℝ (CliffordAlgebra Q)) ∘ₗ ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
⊢ ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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)
a₂ a₃ : Eq (α := CliffordAlgebra Q) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)
⊢ Eq (α := CliffordAlgebra Q)
    ((ofComplex : (a : ℂ) → CliffordAlgebra Q)
      ((toComplex : (a : CliffordAlgebra Q) → ℂ) ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)))
    ((ι Q : (a : ℝ) → CliffordAlgebra Q) 1)

Tactic:
rw [toComplex_ι, one_smul, ofComplex_I]

Premises used: CliffordAlgebraComplex.ofComplex_I, one_smul, CliffordAlgebraComplex.toComplex_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
c : CliffordAlgebra Q
⊢ (ofComplex : (a : ℂ) → CliffordAlgebra Q) ((toComplex : (a : CliffordAlgebra Q) → ℂ) c) = c

Tactic:
AlgHom.congr_fun ofComplex_comp_toComplex c

Premises used: AlgHom.congr_fun, CliffordAlgebraComplex.ofComplex_comp_toComplex
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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)
rw₂ 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 : ℂ)
⊢ Eq (α := ℂ) ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (x * y) : ℂ)
    ((CliffordAlgebraComplex.equiv : (a : CliffordAlgebra Q) → ℂ) (y * x) : ℂ)

Tactic:
rw [map_mul, mul_comm, map_mul]

Premises used: map_mul, mul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
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:
reverse.commutes _

Premises used: CliffordAlgebra.reverse.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
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:
exact reverse.commutes _

Premises used: CliffordAlgebra.reverse.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
x : ℝ
ι ι₁ :
  Eq (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((CliffordAlgebra.ι Q : (a : ℝ) → CliffordAlgebra Q) x : CliffordAlgebra Q)
⊢ 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)

Tactic:
rw [reverse_ι]

Premises used: CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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₂
mul₃ mul₄ : x₁ * x₂ = x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x₁ * x₂) = x₁ * x₂

Tactic:
rw [reverse.map_mul, mul_comm, hx₁, hx₂]

Premises used: CliffordAlgebra.reverse.map_mul, mul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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₂
add₂ add₃ : x₁ + x₂ = x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x₁ + x₂) = x₁ + x₂

Tactic:
rw [reverse.map_add, hx₁, hx₂]

Premises used: LinearMap.map_add, CliffordAlgebra.reverse
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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₂
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₂
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 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₂]

Premises used: LinearMap.map_add, CliffordAlgebra.ι, CliffordAlgebra.reverse, Algebra.algebraMap, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse.commutes, mul_comm, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
⊢ Eq (α := CliffordAlgebra Q →ₗ[ℝ] CliffordAlgebra Q) reverse LinearMap.id

Tactic:
LinearMap.ext reverse_apply

Premises used: LinearMap.ext, CliffordAlgebraComplex.reverse_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
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) :
          ℂ) :
      ℂ)
rw₄ rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 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) :
      ℂ)

Tactic:
rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]

Premises used: CliffordAlgebraComplex.equiv_apply, CliffordAlgebraComplex.toComplex_involute, CliffordAlgebraComplex.toComplex_ofComplex
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ (Q c₁ c₂ : (a : R × R) → R) v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
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₂)))
⊢ 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₂))

Tactic:
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]

Premises used: CliffordAlgebra.ι_sq_scalar, Algebra.algebraMap_eq_smul_one, CliffordAlgebraQuaternion.Q_apply