[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
x y : CliffordAlgebra 0
⊢ x * y = y * x
[PROOFSTEP]
induction x using CliffordAlgebra.induction
[GOAL]
case h_grade0
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
r✝ : R
⊢ ↑(algebraMap R (CliffordAlgebra 0)) r✝ * y = y * ↑(algebraMap R (CliffordAlgebra 0)) r✝
case h_grade1
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
x✝ : Unit
⊢ ↑(ι 0) x✝ * y = y * ↑(ι 0) x✝
case h_mul
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ a✝² * b✝ * y = y * (a✝² * b✝)
case h_add
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ (a✝² + b✝) * y = y * (a✝² + b✝)
[PROOFSTEP]
case h_grade0 r => apply Algebra.commutes
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
r : R
⊢ ↑(algebraMap R (CliffordAlgebra 0)) r * y = y * ↑(algebraMap R (CliffordAlgebra 0)) r
[PROOFSTEP]
case h_grade0 r => apply Algebra.commutes
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
r : R
⊢ ↑(algebraMap R (CliffordAlgebra 0)) r * y = y * ↑(algebraMap R (CliffordAlgebra 0)) r
[PROOFSTEP]
apply Algebra.commutes
[GOAL]
case h_grade1
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
x✝ : Unit
⊢ ↑(ι 0) x✝ * y = y * ↑(ι 0) x✝
case h_mul
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ a✝² * b✝ * y = y * (a✝² * b✝)
case h_add
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ (a✝² + b✝) * y = y * (a✝² + b✝)
[PROOFSTEP]
case h_grade1 x => simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
x : Unit
⊢ ↑(ι 0) x * y = y * ↑(ι 0) x
[PROOFSTEP]
case h_grade1 x => simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y : CliffordAlgebra 0
x : Unit
⊢ ↑(ι 0) x * y = y * ↑(ι 0) x
[PROOFSTEP]
simp
[GOAL]
case h_mul
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ a✝² * b✝ * y = y * (a✝² * b✝)
case h_add
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ (a✝² + b✝) * y = y * (a✝² + b✝)
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
[PROOFSTEP]
rw [mul_add, add_mul, hx₁, hx₂]
[GOAL]
case h_mul
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y a✝² b✝ : CliffordAlgebra 0
a✝¹ : a✝² * y = y * a✝²
a✝ : b✝ * y = y * b✝
⊢ a✝² * b✝ * y = y * (a✝² * b✝)
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : CommRing R
src✝ : Ring (CliffordAlgebra 0) := instRing 0
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
[PROOFSTEP]
rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x : CliffordAlgebra 0
⊢ ↑reverse x = x
[PROOFSTEP]
induction x using CliffordAlgebra.induction
[GOAL]
case h_grade0
R : Type u_1
inst✝ : CommRing R
r✝ : R
⊢ ↑reverse (↑(algebraMap R (CliffordAlgebra 0)) r✝) = ↑(algebraMap R (CliffordAlgebra 0)) r✝
case h_grade1
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ ↑reverse (↑(ι 0) x✝) = ↑(ι 0) x✝
case h_mul
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_grade0 r => exact reverse.commutes _
[GOAL]
R : Type u_1
inst✝ : CommRing R
r : R
⊢ ↑reverse (↑(algebraMap R (CliffordAlgebra 0)) r) = ↑(algebraMap R (CliffordAlgebra 0)) r
[PROOFSTEP]
case h_grade0 r => exact reverse.commutes _
[GOAL]
R : Type u_1
inst✝ : CommRing R
r : R
⊢ ↑reverse (↑(algebraMap R (CliffordAlgebra 0)) r) = ↑(algebraMap R (CliffordAlgebra 0)) r
[PROOFSTEP]
exact reverse.commutes _
[GOAL]
case h_grade1
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ ↑reverse (↑(ι 0) x✝) = ↑(ι 0) x✝
case h_mul
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_grade1 x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ ↑reverse (↑(ι 0) x) = ↑(ι 0) x
[PROOFSTEP]
case h_grade1 x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ ↑reverse (↑(ι 0) x) = ↑(ι 0) x
[PROOFSTEP]
rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
[GOAL]
case h_mul
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ * x₂) = x₁ * x₂
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ * x₂) = x₁ * x₂
[PROOFSTEP]
rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
case h_add
R : Type u_1
inst✝ : CommRing R
a✝² b✝ : CliffordAlgebra 0
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ + x₂) = x₁ + x₂
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ + x₂) = x₁ + x₂
[PROOFSTEP]
rw [reverse.map_add, hx₁, hx₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ involute = AlgHom.id R (CliffordAlgebra 0)
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap involute) (ι 0)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra 0))) (ι 0)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ AlgHom.comp (↑(lift 0) { val := 0, property := (_ : ∀ (m : Unit), 0 * 0 = ↑(algebraMap R R) (↑0 m)) })
      (Algebra.ofId R (CliffordAlgebra 0)) =
    AlgHom.id R R
[PROOFSTEP]
ext x
[GOAL]
case H
R : Type u_1
inst✝ : CommRing R
x : R
⊢ ↑(AlgHom.comp (↑(lift 0) { val := 0, property := (_ : ∀ (m : Unit), 0 * 0 = ↑(algebraMap R R) (↑0 m)) })
          (Algebra.ofId R (CliffordAlgebra 0)))
      x =
    ↑(AlgHom.id R R) x
[PROOFSTEP]
exact AlgHom.commutes _ x
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ AlgHom.comp (Algebra.ofId R (CliffordAlgebra 0))
      (↑(lift 0) { val := 0, property := (_ : ∀ (m : Unit), 0 * 0 = ↑(algebraMap R R) (↑0 m)) }) =
    AlgHom.id R (CliffordAlgebra 0)
[PROOFSTEP]
ext : 1
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
⊢ LinearMap.comp
      (AlgHom.toLinearMap
        (AlgHom.comp (Algebra.ofId R (CliffordAlgebra 0))
          (↑(lift 0) { val := 0, property := (_ : ∀ (m : Unit), 0 * 0 = ↑(algebraMap R R) (↑0 m)) })))
      (ι 0) =
    LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra 0))) (ι 0)
[PROOFSTEP]
rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero]
[GOAL]
r : ℝ
⊢ ↑(LinearMap.toSpanSingleton ℝ ℂ Complex.I) r * ↑(LinearMap.toSpanSingleton ℝ ℂ Complex.I) r = ↑(algebraMap ℝ ℂ) (↑Q r)
[PROOFSTEP]
dsimp [LinearMap.toSpanSingleton, LinearMap.id]
[GOAL]
r : ℝ
⊢ ↑r * Complex.I * (↑r * Complex.I) = ↑(-(r * r))
[PROOFSTEP]
rw [mul_mul_mul_comm]
[GOAL]
r : ℝ
⊢ ↑r * ↑r * (Complex.I * Complex.I) = ↑(-(r * r))
[PROOFSTEP]
simp
[GOAL]
c : CliffordAlgebra Q
⊢ ↑toComplex (↑involute c) = ↑(starRingEnd ((fun x => ℂ) c)) (↑toComplex c)
[PROOFSTEP]
have : toComplex (involute (ι Q 1)) = conj (toComplex (ι Q 1)) := by
  simp only [involute_ι, toComplex_ι, AlgHom.map_neg, one_smul, Complex.conj_I]
[GOAL]
c : CliffordAlgebra Q
⊢ ↑toComplex (↑involute (↑(ι Q) 1)) = ↑(starRingEnd ((fun x => ℂ) (↑(ι Q) 1))) (↑toComplex (↑(ι Q) 1))
[PROOFSTEP]
simp only [involute_ι, toComplex_ι, AlgHom.map_neg, one_smul, Complex.conj_I]
[GOAL]
c : CliffordAlgebra Q
this : ↑toComplex (↑involute (↑(ι Q) 1)) = ↑(starRingEnd ((fun x => ℂ) (↑(ι Q) 1))) (↑toComplex (↑(ι Q) 1))
⊢ ↑toComplex (↑involute c) = ↑(starRingEnd ((fun x => ℂ) c)) (↑toComplex c)
[PROOFSTEP]
suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by exact AlgHom.congr_fun this c
[GOAL]
c : CliffordAlgebra Q
this✝ : ↑toComplex (↑involute (↑(ι Q) 1)) = ↑(starRingEnd ((fun x => ℂ) (↑(ι Q) 1))) (↑toComplex (↑(ι Q) 1))
this : AlgHom.comp toComplex involute = AlgHom.comp (↑Complex.conjAe) toComplex
⊢ ↑toComplex (↑involute c) = ↑(starRingEnd ((fun x => ℂ) c)) (↑toComplex c)
[PROOFSTEP]
exact AlgHom.congr_fun this c
[GOAL]
c : CliffordAlgebra Q
this : ↑toComplex (↑involute (↑(ι Q) 1)) = ↑(starRingEnd ((fun x => ℂ) (↑(ι Q) 1))) (↑toComplex (↑(ι Q) 1))
⊢ AlgHom.comp toComplex involute = AlgHom.comp (↑Complex.conjAe) toComplex
[PROOFSTEP]
ext : 2
[GOAL]
case a.h
c : CliffordAlgebra Q
this : ↑toComplex (↑involute (↑(ι Q) 1)) = ↑(starRingEnd ((fun x => ℂ) (↑(ι Q) 1))) (↑toComplex (↑(ι Q) 1))
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp toComplex involute)) (ι Q)) 1 =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (↑Complex.conjAe) toComplex)) (ι Q)) 1
[PROOFSTEP]
exact this
[GOAL]
⊢ ↑(ι Q) 1 * ↑(ι Q) 1 = -1
[PROOFSTEP]
rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, RingHom.map_neg, RingHom.map_one]
[GOAL]
⊢ ↑{ val := ↑(ι Q) 1, property := ofComplex.proof_1 } * ↑{ val := ↑(ι Q) 1, property := ofComplex.proof_1 } = -1
[PROOFSTEP]
simp
[GOAL]
⊢ AlgHom.comp toComplex ofComplex = AlgHom.id ℝ ℂ
[PROOFSTEP]
ext1
[GOAL]
case h
⊢ ↑(AlgHom.comp toComplex ofComplex) Complex.I = ↑(AlgHom.id ℝ ℂ) Complex.I
[PROOFSTEP]
dsimp only [AlgHom.comp_apply, Subtype.coe_mk, AlgHom.id_apply]
[GOAL]
case h
⊢ ↑toComplex (↑ofComplex Complex.I) = Complex.I
[PROOFSTEP]
rw [ofComplex_I, toComplex_ι, one_smul]
[GOAL]
⊢ AlgHom.comp ofComplex toComplex = AlgHom.id ℝ (CliffordAlgebra Q)
[PROOFSTEP]
ext
[GOAL]
case a.h
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp ofComplex toComplex)) (ι Q)) 1 =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id ℝ (CliffordAlgebra Q))) (ι Q)) 1
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, Subtype.coe_mk, AlgHom.id_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply]
[GOAL]
case a.h
⊢ ↑ofComplex (↑toComplex (↑(ι Q) 1)) = ↑(ι Q) 1
[PROOFSTEP]
rw [toComplex_ι, one_smul, ofComplex_I]
[GOAL]
src✝ : Ring (CliffordAlgebra Q) := instRing Q
x y : CliffordAlgebra Q
⊢ ↑CliffordAlgebraComplex.equiv (x * y) = ↑CliffordAlgebraComplex.equiv (y * x)
[PROOFSTEP]
rw [AlgEquiv.map_mul, mul_comm, AlgEquiv.map_mul]
[GOAL]
x : CliffordAlgebra Q
⊢ ↑reverse x = x
[PROOFSTEP]
induction x using CliffordAlgebra.induction
[GOAL]
case h_grade0
r✝ : ℝ
⊢ ↑reverse (↑(algebraMap ℝ (CliffordAlgebra Q)) r✝) = ↑(algebraMap ℝ (CliffordAlgebra Q)) r✝
case h_grade1
x✝ : ℝ
⊢ ↑reverse (↑(ι Q) x✝) = ↑(ι Q) x✝
case h_mul
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add a✝² b✝ : CliffordAlgebra Q a✝¹ : ↑reverse a✝² = a✝² a✝ : ↑reverse b✝ = b✝ ⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_grade0 r => exact reverse.commutes _
[GOAL]
r : ℝ
⊢ ↑reverse (↑(algebraMap ℝ (CliffordAlgebra Q)) r) = ↑(algebraMap ℝ (CliffordAlgebra Q)) r
[PROOFSTEP]
case h_grade0 r => exact reverse.commutes _
[GOAL]
r : ℝ
⊢ ↑reverse (↑(algebraMap ℝ (CliffordAlgebra Q)) r) = ↑(algebraMap ℝ (CliffordAlgebra Q)) r
[PROOFSTEP]
exact reverse.commutes _
[GOAL]
case h_grade1
x✝ : ℝ
⊢ ↑reverse (↑(ι Q) x✝) = ↑(ι Q) x✝
case h_mul
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add a✝² b✝ : CliffordAlgebra Q a✝¹ : ↑reverse a✝² = a✝² a✝ : ↑reverse b✝ = b✝ ⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_grade1 x => rw [reverse_ι]
[GOAL]
x : ℝ
⊢ ↑reverse (↑(ι Q) x) = ↑(ι Q) x
[PROOFSTEP]
case h_grade1 x => rw [reverse_ι]
[GOAL]
x : ℝ
⊢ ↑reverse (↑(ι Q) x) = ↑(ι Q) x
[PROOFSTEP]
rw [reverse_ι]
[GOAL]
case h_mul
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² * b✝) = a✝² * b✝
case h_add a✝² b✝ : CliffordAlgebra Q a✝¹ : ↑reverse a✝² = a✝² a✝ : ↑reverse b✝ = b✝ ⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
x₁ x₂ : CliffordAlgebra Q
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ * x₂) = x₁ * x₂
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
x₁ x₂ : CliffordAlgebra Q
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ * x₂) = x₁ * x₂
[PROOFSTEP]
rw [reverse.map_mul, mul_comm, hx₁, hx₂]
[GOAL]
case h_add
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse a✝² = a✝²
a✝ : ↑reverse b✝ = b✝
⊢ ↑reverse (a✝² + b✝) = a✝² + b✝
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
[GOAL]
x₁ x₂ : CliffordAlgebra Q
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ + x₂) = x₁ + x₂
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
[GOAL]
x₁ x₂ : CliffordAlgebra Q
hx₁ : ↑reverse x₁ = x₁
hx₂ : ↑reverse x₂ = x₂
⊢ ↑reverse (x₁ + x₂) = x₁ + x₂
[PROOFSTEP]
rw [reverse.map_add, hx₁, hx₂]
[GOAL]
c : ℂ
⊢ ↑CliffordAlgebraComplex.equiv (↑ofComplex (↑(starRingEnd ℂ) c)) =
    ↑CliffordAlgebraComplex.equiv (↑involute (↑ofComplex c))
[PROOFSTEP]
rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (1, 0) = c₁ • 1
[PROOFSTEP]
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((1, 0).fst * (1, 0).fst) + c₂ * ((1, 0).snd * (1, 0).snd)) =
    ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₁
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(ι (Q c₁ c₂)) (0, 1) * ↑(ι (Q c₁ c₂)) (0, 1) = c₂ • 1
[PROOFSTEP]
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((0, 1).fst * (0, 1).fst) + c₂ * ((0, 1).snd * (0, 1).snd)) =
    ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₂
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(ι (Q c₁ c₂)) (0, 1) * ↑(ι (Q c₁ c₂)) (1, 0) = -(↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (0, 1))
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticForm.polar]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) (↑(Q c₁ c₂) ((0, 1) + (1, 0)) - ↑(Q c₁ c₂) (0, 1) - ↑(Q c₁ c₂) (1, 0)) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v₁ v₂ : R × R
⊢ (fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 }) (v₁ + v₂) =
    (fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 }) v₁ +
      (fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 }) v₂
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
v : R × R
⊢ AddHom.toFun
      { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
        map_add' :=
          (_ :
            ∀ (v₁ v₂ : R × R),
              { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
      (r • v) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
          map_add' :=
            (_ :
              ∀ (v₁ v₂ : R × R),
                { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                  { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
        v
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
v : R × R
⊢ { re := 0, imI := (r • v).fst, imJ := (r • v).snd, imK := 0 } =
    { re := r * 0, imI := r * v.fst, imJ := r * v.snd, imK := r * 0 }
[PROOFSTEP]
rw [mul_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
v : R × R
⊢ { re := 0, imI := (r • v).fst, imJ := (r • v).snd, imK := 0 } =
    { re := 0, imI := r * v.fst, imJ := r * v.snd, imK := 0 }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ ↑{
            toAddHom :=
              { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                map_add' :=
                  (_ :
                    ∀ (v₁ v₂ : R × R),
                      { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                        { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) },
            map_smul' :=
              (_ :
                ∀ (r : R) (v : R × R),
                  AddHom.toFun
                      { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                        map_add' :=
                          (_ :
                            ∀ (v₁ v₂ : R × R),
                              { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                                { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
                      (r • v) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                          map_add' :=
                            (_ :
                              ∀ (v₁ v₂ : R × R),
                                { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                                  { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
                        v) }
        v *
      ↑{
            toAddHom :=
              { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                map_add' :=
                  (_ :
                    ∀ (v₁ v₂ : R × R),
                      { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                        { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) },
            map_smul' :=
              (_ :
                ∀ (r : R) (v : R × R),
                  AddHom.toFun
                      { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                        map_add' :=
                          (_ :
                            ∀ (v₁ v₂ : R × R),
                              { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                                { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
                      (r • v) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := fun v => { re := 0, imI := v.fst, imJ := v.snd, imK := 0 },
                          map_add' :=
                            (_ :
                              ∀ (v₁ v₂ : R × R),
                                { re := 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 } =
                                  { re := 0 + 0, imI := v₁.fst + v₂.fst, imJ := v₁.snd + v₂.snd, imK := 0 + 0 }) }
                        v) }
        v =
    ↑(algebraMap R ℍ[R,c₁,c₂]) (↑(Q c₁ c₂) v)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
      imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
      imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
      imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 } =
    ↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.re =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).re
case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imI =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imI
case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imJ =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imJ
case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imK =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imK
[PROOFSTEP]
all_goals dsimp; ring
[GOAL]
case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.re =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).re
[PROOFSTEP]
dsimp
[GOAL]
case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0 = c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd)
[PROOFSTEP]
ring
[GOAL]
case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imI =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imI
[PROOFSTEP]
dsimp
[GOAL]
case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd = 0
[PROOFSTEP]
ring
[GOAL]
case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imJ =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imJ
[PROOFSTEP]
dsimp
[GOAL]
case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst = 0
[PROOFSTEP]
ring
[GOAL]
case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.fst * v.fst + c₂ * v.snd * v.snd - c₁ * c₂ * 0 * 0,
        imI := 0 * v.fst + v.fst * 0 - c₂ * v.snd * 0 + c₂ * 0 * v.snd,
        imJ := 0 * v.snd + c₁ * v.fst * 0 + v.snd * 0 - c₁ * 0 * v.fst,
        imK := 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 }.imK =
    (↑(c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd))).imK
[PROOFSTEP]
dsimp
[GOAL]
case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + v.fst * v.snd - v.snd * v.fst + 0 * 0 = 0
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ ↑toQuaternion (star c) = star (↑toQuaternion c)
[PROOFSTEP]
simp only [CliffordAlgebra.star_def']
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ ↑toQuaternion (↑involute (↑reverse c)) = star (↑toQuaternion c)
[PROOFSTEP]
induction c using CliffordAlgebra.induction
[GOAL]
case h_grade0
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r✝ : R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r✝))) =
    star (↑toQuaternion (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r✝))
case h_grade1
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x✝ : R × R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(ι (Q c₁ c₂)) x✝))) = star (↑toQuaternion (↑(ι (Q c₁ c₂)) x✝))
case h_mul
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² * b✝))) = star (↑toQuaternion (a✝² * b✝))
case h_add
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² + b✝))) = star (↑toQuaternion (a✝² + b✝))
[PROOFSTEP]
case h_grade0 r =>
  simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap, QuaternionAlgebra.star_coe]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))) =
    star (↑toQuaternion (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))
[PROOFSTEP]
case h_grade0 r =>
  simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap, QuaternionAlgebra.star_coe]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))) =
    star (↑toQuaternion (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))
[PROOFSTEP]
simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap, QuaternionAlgebra.star_coe]
[GOAL]
case h_grade1
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x✝ : R × R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(ι (Q c₁ c₂)) x✝))) = star (↑toQuaternion (↑(ι (Q c₁ c₂)) x✝))
case h_mul
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² * b✝))) = star (↑toQuaternion (a✝² * b✝))
case h_add
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² + b✝))) = star (↑toQuaternion (a✝² + b✝))
[PROOFSTEP]
case h_grade1 x =>
  rw [reverse_ι, involute_ι, toQuaternion_ι, AlgHom.map_neg, toQuaternion_ι, QuaternionAlgebra.neg_mk, star_mk,
    neg_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x : R × R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(ι (Q c₁ c₂)) x))) = star (↑toQuaternion (↑(ι (Q c₁ c₂)) x))
[PROOFSTEP]
case h_grade1 x =>
  rw [reverse_ι, involute_ι, toQuaternion_ι, AlgHom.map_neg, toQuaternion_ι, QuaternionAlgebra.neg_mk, star_mk,
    neg_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x : R × R
⊢ ↑toQuaternion (↑involute (↑reverse (↑(ι (Q c₁ c₂)) x))) = star (↑toQuaternion (↑(ι (Q c₁ c₂)) x))
[PROOFSTEP]
rw [reverse_ι, involute_ι, toQuaternion_ι, AlgHom.map_neg, toQuaternion_ι, QuaternionAlgebra.neg_mk, star_mk, neg_zero]
[GOAL]
case h_mul
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² * b✝))) = star (↑toQuaternion (a✝² * b✝))
case h_add
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² + b✝))) = star (↑toQuaternion (a✝² + b✝))
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : ↑toQuaternion (↑involute (↑reverse x₁)) = star (↑toQuaternion x₁)
hx₂ : ↑toQuaternion (↑involute (↑reverse x₂)) = star (↑toQuaternion x₂)
⊢ ↑toQuaternion (↑involute (↑reverse (x₁ * x₂))) = star (↑toQuaternion (x₁ * x₂))
[PROOFSTEP]
case h_mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : ↑toQuaternion (↑involute (↑reverse x₁)) = star (↑toQuaternion x₁)
hx₂ : ↑toQuaternion (↑involute (↑reverse x₂)) = star (↑toQuaternion x₂)
⊢ ↑toQuaternion (↑involute (↑reverse (x₁ * x₂))) = star (↑toQuaternion (x₁ * x₂))
[PROOFSTEP]
simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul]
[GOAL]
case h_add
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
a✝² b✝ : CliffordAlgebra (Q c₁ c₂)
a✝¹ : ↑toQuaternion (↑involute (↑reverse a✝²)) = star (↑toQuaternion a✝²)
a✝ : ↑toQuaternion (↑involute (↑reverse b✝)) = star (↑toQuaternion b✝)
⊢ ↑toQuaternion (↑involute (↑reverse (a✝² + b✝))) = star (↑toQuaternion (a✝² + b✝))
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : ↑toQuaternion (↑involute (↑reverse x₁)) = star (↑toQuaternion x₁)
hx₂ : ↑toQuaternion (↑involute (↑reverse x₂)) = star (↑toQuaternion x₂)
⊢ ↑toQuaternion (↑involute (↑reverse (x₁ + x₂))) = star (↑toQuaternion (x₁ + x₂))
[PROOFSTEP]
case h_add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : ↑toQuaternion (↑involute (↑reverse x₁)) = star (↑toQuaternion x₁)
hx₂ : ↑toQuaternion (↑involute (↑reverse x₂)) = star (↑toQuaternion x₂)
⊢ ↑toQuaternion (↑involute (↑reverse (x₁ + x₂))) = star (↑toQuaternion (x₁ + x₂))
[PROOFSTEP]
simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ AlgHom.comp ofQuaternion toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))
[PROOFSTEP]
ext : 1
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion)) (ι (Q c₁ c₂)) =
    LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂))
[PROOFSTEP]
dsimp
  -- before we end up with two goals and have to do this twice
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap ofQuaternion) (AlgHom.toLinearMap toQuaternion)) (ι (Q c₁ c₂)) =
    LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂))
[PROOFSTEP]
ext
[GOAL]
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(LinearMap.comp
          (LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap ofQuaternion) (AlgHom.toLinearMap toQuaternion))
            (ι (Q c₁ c₂)))
          (LinearMap.inl R R R))
      1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂)))
          (LinearMap.inl R R R))
      1
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(LinearMap.comp
          (LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap ofQuaternion) (AlgHom.toLinearMap toQuaternion))
            (ι (Q c₁ c₂)))
          (LinearMap.inr R R R))
      1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂)))
          (LinearMap.inr R R R))
      1
[PROOFSTEP]
all_goals
  dsimp
  rw [toQuaternion_ι]
  dsimp
  simp only [toQuaternion_ι, zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]
[GOAL]
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(LinearMap.comp
          (LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap ofQuaternion) (AlgHom.toLinearMap toQuaternion))
            (ι (Q c₁ c₂)))
          (LinearMap.inl R R R))
      1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂)))
          (LinearMap.inl R R R))
      1
[PROOFSTEP]
dsimp
[GOAL]
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑ofQuaternion (↑toQuaternion (↑(ι (Q c₁ c₂)) (1, 0))) = ↑(ι (Q c₁ c₂)) (1, 0)
[PROOFSTEP]
rw [toQuaternion_ι]
[GOAL]
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑ofQuaternion { re := 0, imI := (1, 0).fst, imJ := (1, 0).snd, imK := 0 } = ↑(ι (Q c₁ c₂)) (1, 0)
[PROOFSTEP]
dsimp
[GOAL]
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 1 • ↑(ι (Q c₁ c₂)) (1, 0) + 0 • ↑(ι (Q c₁ c₂)) (0, 1) +
      0 • (↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (0, 1)) =
    ↑(ι (Q c₁ c₂)) (1, 0)
[PROOFSTEP]
simp only [toQuaternion_ι, zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]
[GOAL]
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(LinearMap.comp
          (LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap ofQuaternion) (AlgHom.toLinearMap toQuaternion))
            (ι (Q c₁ c₂)))
          (LinearMap.inr R R R))
      1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (Q c₁ c₂)))) (ι (Q c₁ c₂)))
          (LinearMap.inr R R R))
      1
[PROOFSTEP]
dsimp
[GOAL]
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑ofQuaternion (↑toQuaternion (↑(ι (Q c₁ c₂)) (0, 1))) = ↑(ι (Q c₁ c₂)) (0, 1)
[PROOFSTEP]
rw [toQuaternion_ι]
[GOAL]
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑ofQuaternion { re := 0, imI := (0, 1).fst, imJ := (0, 1).snd, imK := 0 } = ↑(ι (Q c₁ c₂)) (0, 1)
[PROOFSTEP]
dsimp
[GOAL]
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 0 • ↑(ι (Q c₁ c₂)) (1, 0) + 1 • ↑(ι (Q c₁ c₂)) (0, 1) +
      0 • (↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (0, 1)) =
    ↑(ι (Q c₁ c₂)) (0, 1)
[PROOFSTEP]
simp only [toQuaternion_ι, zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ AlgHom.comp toQuaternion ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂]
[PROOFSTEP]
apply QuaternionAlgebra.lift.symm.injective
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑QuaternionAlgebra.lift.symm (AlgHom.comp toQuaternion ofQuaternion) =
    ↑QuaternionAlgebra.lift.symm (AlgHom.id R ℍ[R,c₁,c₂])
[PROOFSTEP]
ext1
[GOAL]
case a.hi
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (↑QuaternionAlgebra.lift.symm (AlgHom.comp toQuaternion ofQuaternion)).i =
    (↑QuaternionAlgebra.lift.symm (AlgHom.id R ℍ[R,c₁,c₂])).i
[PROOFSTEP]
dsimp [QuaternionAlgebra.Basis.lift]
[GOAL]
case a.hj
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (↑QuaternionAlgebra.lift.symm (AlgHom.comp toQuaternion ofQuaternion)).j =
    (↑QuaternionAlgebra.lift.symm (AlgHom.id R ℍ[R,c₁,c₂])).j
[PROOFSTEP]
dsimp [QuaternionAlgebra.Basis.lift]
[GOAL]
case a.hi
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑toQuaternion
      (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 1 • ↑(ι (Q c₁ c₂)) (1, 0) + 0 • ↑(ι (Q c₁ c₂)) (0, 1) +
        0 • (↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (0, 1))) =
    { re := 0, imI := 1, imJ := 0, imK := 0 }
[PROOFSTEP]
simp
[GOAL]
case a.hj
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ↑toQuaternion
      (↑(algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 0 • ↑(ι (Q c₁ c₂)) (1, 0) + 1 • ↑(ι (Q c₁ c₂)) (0, 1) +
        0 • (↑(ι (Q c₁ c₂)) (1, 0) * ↑(ι (Q c₁ c₂)) (0, 1))) =
    { re := 0, imI := 0, imJ := 1, imK := 0 }
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
⊢ ↑CliffordAlgebraQuaternion.equiv (↑ofQuaternion (star q)) = ↑CliffordAlgebraQuaternion.equiv (star (↑ofQuaternion q))
[PROOFSTEP]
rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion, toQuaternion_ofQuaternion]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
⊢ ↑(ι 0) r₁ * ↑(ι 0) r₂ = 0
[PROOFSTEP]
rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul, LinearMap.map_smul, smul_mul_smul,
  ι_sq_scalar, QuadraticForm.zero_apply, RingHom.map_zero, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ AlgHom.comp (↑(CliffordAlgebra.lift 0) { val := inrHom R R, property := (_ : ∀ (m : R), inr m * inr m = 0) })
      (↑DualNumber.lift { val := ↑(ι 0) 1, property := (_ : ↑(ι 0) 1 * ↑(ι 0) 1 = 0) }) =
    AlgHom.id R R[ε]
[PROOFSTEP]
ext : 1
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ↑(AlgHom.comp (↑(CliffordAlgebra.lift 0) { val := inrHom R R, property := (_ : ∀ (m : R), inr m * inr m = 0) })
          (↑DualNumber.lift { val := ↑(ι 0) 1, property := (_ : ↑(ι 0) 1 * ↑(ι 0) 1 = 0) }))
      ε =
    ↑(AlgHom.id R R[ε]) ε
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ AlgHom.comp (↑DualNumber.lift { val := ↑(ι 0) 1, property := (_ : ↑(ι 0) 1 * ↑(ι 0) 1 = 0) })
      (↑(CliffordAlgebra.lift 0) { val := inrHom R R, property := (_ : ∀ (m : R), inr m * inr m = 0) }) =
    AlgHom.id R (CliffordAlgebra 0)
[PROOFSTEP]
ext : 2
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp (↑DualNumber.lift { val := ↑(ι 0) 1, property := (_ : ↑(ι 0) 1 * ↑(ι 0) 1 = 0) })
              (↑(CliffordAlgebra.lift 0) { val := inrHom R R, property := (_ : ∀ (m : R), inr m * inr m = 0) })))
          (ι 0))
      1 =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra 0))) (ι 0)) 1
[PROOFSTEP]
simp