awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)

Tactic:
simp_rw [changeForm_algebraMap]

Premises used: CliffordAlgebra.changeForm_algebraMap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) x
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₂ add₃ : x + y = x + y
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y

Tactic:
rw [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
    (hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
    (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M) (hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x),
    (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x

Tactic:
induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]

Premises used: LinearMap.zero_apply, Algebra.algebraMap, sub_zero, CliffordAlgebra.changeForm_ι_mul, map_zero, map_add, CliffordAlgebra.changeForm_algebraMap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Eq (α := CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) (changeForm ⋯) LinearMap.id

Tactic:
LinearMap.ext <| changeForm_self_apply

Premises used: CliffordAlgebra.changeForm_self_apply, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
r : R
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'')
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q'')

Tactic:
simp_rw [changeForm_algebraMap]

Premises used: CliffordAlgebra.changeForm_algebraMap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
⊢ changeForm h' ∘ₗ changeForm h = changeForm ⋯

Tactic:
LinearMap.ext <| changeForm_changeForm _ h'

Premises used: LinearMap.ext, CliffordAlgebra.changeForm_changeForm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
simp_rw : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x

Tactic:
simp_rw [(add_neg_cancel B), changeForm_self_apply]

Premises used: add_neg_cancel, CliffordAlgebra.changeForm_self_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q)
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) =
    x

Tactic:
exact (changeForm_changeForm _ _ x).trans <|
        by simp_rw [(add_neg_cancel B), changeForm_self_apply]

Premises used: Eq.trans, CliffordAlgebra.changeForm_changeForm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q'
simp_rw : (changeForm ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q') x = x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q') x = x

Tactic:
simp_rw [(neg_add_cancel B), changeForm_self_apply]

Premises used: CliffordAlgebra.changeForm_self_apply, neg_add_cancel
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q'
⊢ (changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
      ((changeForm ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q) x) =
    x

Tactic:
exact (changeForm_changeForm _ _ x).trans <|
        by simp_rw [(neg_add_cancel B), changeForm_self_apply]

Premises used: Eq.trans, CliffordAlgebra.changeForm_changeForm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ (changeFormEquiv h).symm = changeFormEquiv ⋯

Tactic:
LinearEquiv.ext fun _ => rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
inst_3 : Nontrivial R
inst_4 : Invertible (α := R) 2
⊢ Nontrivial (CliffordAlgebra Q)

Tactic:
(equivExterior Q).symm.injective.nontrivial

Premises used: LinearEquiv.symm, CliffordAlgebra.equivExterior, Function.Injective.nontrivial, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := Unit →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) (ι 0) 0

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
y : CliffordAlgebra (R := R) (M := Unit) 0
r : R
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
      y =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
      ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
apply Algebra.commutes

Premises used: Algebra.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
y : CliffordAlgebra (R := R) (M := Unit) 0
x : Unit
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0) y =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
      ((ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
add : (x₁ + x₂) * y = y * x₁ + y * x₂
add₁ : x₁ * y + x₂ * y = y * x₁ + y * x₂
add₂ : y * x₁ + x₂ * y = y * x₁ + y * x₂
add₃ add₄ : y * x₁ + y * x₂ = y * x₁ + y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)

Tactic:
rw [mul_add, add_mul, hx₁, hx₂]

Premises used: add_mul, mul_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
mul₁ : x₁ * (y * x₂) = y * (x₁ * x₂)
mul₂ : x₁ * y * x₂ = y * (x₁ * x₂)
mul₃ : y * x₁ * x₂ = y * (x₁ * x₂)
mul₄ mul₅ : y * x₁ * x₂ = y * x₁ * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)

Tactic:
rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
x y : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
        y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0) y =
      HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) y
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
add :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0) (hx₁ : x₁ * y = y * x₁) (hx₂ : x₂ * y = y * x₂),
    (x₁ + x₂) * y = y * (x₁ + x₂)
mul :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0) (hx₁ : x₁ * y = y * x₁) (hx₂ : x₂ * y = y * x₂),
    x₁ * x₂ * y = y * (x₁ * x₂)
⊢ x * y = y * x

Tactic:
induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]

Premises used: add_mul, CliffordAlgebra.ι, Algebra.algebraMap, mul_assoc, mul_add, Algebra.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
      CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
reverse.commutes _

Premises used: CliffordAlgebra.reverse.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
      CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
exact reverse.commutes _

Premises used: CliffordAlgebra.reverse.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
x : Unit
ι :
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) ((0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
ι₁ :
  Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0) ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) 0)
    0
ι₂ ι₃ : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0) 0 0
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
        ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
      CliffordAlgebra (R := R) (M := Unit) 0)
    ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]

Premises used: LinearMap.zero_apply, CliffordAlgebra.reverse, LinearMap.map_zero, CliffordAlgebraRing.ι_eq_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
mul :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₂ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ * x₂
mul₃ mul₄ : x₁ * x₂ = x₁ * x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (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:
R : Type u_1
inst : CommRing R
x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁
hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂
add :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := Unit) 0) (β := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ : CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ + x₂
add₁ :
  HAdd.hAdd (β := CliffordAlgebra (R := R) (M := Unit) 0) x₁
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ : CliffordAlgebra (R := R) (M := Unit) 0) =
    x₁ + x₂
add₂ add₃ : x₁ + x₂ = x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂

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

Premises used: LinearMap.map_add, CliffordAlgebra.reverse
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
x : CliffordAlgebra (R := R) (M := Unit) 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := Unit) 0) : (a : R) → CliffordAlgebra 0) r :
        CliffordAlgebra (R := R) (M := Unit) 0)
ι :
  ∀ (x : Unit),
    Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0)
          ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x) :
        CliffordAlgebra (R := R) (M := Unit) 0)
      ((CliffordAlgebra.ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
mul :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
    (hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁)
    (hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂),
    (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ * x₂) = x₁ * x₂
add :
  ∀ (x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0)
    (hx₁ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₁ = x₁)
    (hx₂ : (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x₂ = x₂),
    (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) (x₁ + x₂) = x₁ + x₂
⊢ (reverse : (a : CliffordAlgebra 0) → CliffordAlgebra 0) x = x

Tactic:
induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]

Premises used: LinearMap.map_add, LinearMap.zero_apply, CliffordAlgebra.ι, CliffordAlgebra.reverse, Algebra.algebraMap, LinearMap.map_zero, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse.commutes, CliffordAlgebraRing.ι_eq_zero, mul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := Unit) 0 →ₗ[R] CliffordAlgebra (R := R) (M := Unit) 0) reverse
    LinearMap.id

Tactic:
LinearMap.ext reverse_apply

Premises used: LinearMap.ext, CliffordAlgebraRing.reverse_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
a :
  ∀ (x : Unit),
    Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
      ((AlgHom.toLinearMap involute ∘ₗ ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
      ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0 :
            (a : Unit) → CliffordAlgebra 0)
          x :
        CliffordAlgebra (R := R) (M := Unit) 0)
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0 →ₐ[R] CliffordAlgebra (R := R) (M := Unit) 0) involute
    (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
x : Unit
⊢ Eq (α := CliffordAlgebra (R := R) (M := Unit) 0)
    ((AlgHom.toLinearMap involute ∘ₗ ι 0 : (a : Unit) → CliffordAlgebra 0) x : CliffordAlgebra (R := R) (M := Unit) 0)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := Unit) 0)) ∘ₗ ι 0 : (a : Unit) → CliffordAlgebra 0)
        x :
      CliffordAlgebra (R := R) (M := Unit) 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R →ₐ[R] R)
    (AlgHom.comp (B := 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 ⋯))
      (Algebra.ofId R (CliffordAlgebra (R := R) (M := Unit) 0)))
    (AlgHom.id R R)

Tactic:
ext
-- 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)
⊢ 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))

Tactic:
ext : 1