awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
x : CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)
⊢ Eq (α := A ⊗[R] CliffordAlgebra Q)
    (((TensorProduct.AlgebraTensorModule.map (↑(LinearEquiv.refl A A) : A →ₗ[A] A)
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap reverseOp) :
            A ⊗[R] CliffordAlgebra Q →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q) x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q) x) :
      A ⊗[R] CliffordAlgebra Q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
h :
  ∀ (v : V),
    Eq (α := A ⊗[R] CliffordAlgebra Q)
      ((AlgHom.toLinearMap
                (AlgHom.comp
                  (AlgHom.restrictScalars R
                    (AlgHom.comp (B := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
                      (toBaseChange A Q) (ofBaseChange A Q)))
                  Algebra.TensorProduct.includeRight) ∘ₗ
              ι Q :
            (a : V) → A ⊗[R] CliffordAlgebra Q)
          v :
        A ⊗[R] CliffordAlgebra Q)
      ((AlgHom.toLinearMap
                (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] CliffordAlgebra Q)))
                  Algebra.TensorProduct.includeRight) ∘ₗ
              ι Q :
            (a : V) → A ⊗[R] CliffordAlgebra Q)
          v :
        A ⊗[R] CliffordAlgebra Q)
⊢ Eq (α := A ⊗[R] CliffordAlgebra Q →ₐ[A] A ⊗[R] CliffordAlgebra Q)
    (AlgHom.comp (B := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (toBaseChange A Q)
      (ofBaseChange A Q))
    (AlgHom.id A (A ⊗[R] CliffordAlgebra Q))

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
v : V
⊢ Eq (α := A ⊗[R] CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              (AlgHom.comp
                (AlgHom.restrictScalars R
                  (AlgHom.comp (B := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
                    (toBaseChange A Q) (ofBaseChange A Q)))
                Algebra.TensorProduct.includeRight) ∘ₗ
            ι Q :
          (a : V) → A ⊗[R] CliffordAlgebra Q)
        v :
      A ⊗[R] CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] CliffordAlgebra Q)))
                Algebra.TensorProduct.includeRight) ∘ₗ
            ι Q :
          (a : V) → A ⊗[R] CliffordAlgebra Q)
        v :
      A ⊗[R] CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
x : A ⊗[R] CliffordAlgebra Q
⊢ (toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
      ((ofBaseChange A Q : (a : A ⊗[R] CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q)) x) =
    x

Tactic:
AlgHom.congr_fun (toBaseChange_comp_ofBaseChange A Q :) x

Premises used: Quotient.liftOn', AddCon.liftOn, CliffordAlgebra.toBaseChange_comp_ofBaseChange, AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
a :
  ∀ (x : V),
    Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap (AlgHom.comp (ofBaseChange A Q) (toBaseChange A Q)) ∘ₗ
                      ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
                (a : A) → V →ₗ[R] CliffordAlgebra (QuadraticForm.baseChange A Q))
              1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          x :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap
                        (AlgHom.id A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))) ∘ₗ
                      ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
                (a : A) → V →ₗ[R] CliffordAlgebra (QuadraticForm.baseChange A Q))
              1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          x :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
⊢ Eq (α :=
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A]
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    (AlgHom.comp (ofBaseChange A Q) (toBaseChange A Q))
    (AlgHom.id A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
x : V
a :
  Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ofBaseChange A Q : (a : A ⊗[R] CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
          ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
            (1 ⊗ₜ[R] x))) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((((TensorProduct.AlgebraTensorModule.curry
                  (AlgHom.toLinearMap (AlgHom.comp (ofBaseChange A Q) (toBaseChange A Q)) ∘ₗ
                    ι (QuadraticForm.baseChange A Q)) :
                A →ₗ[A] V →ₗ[R] CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
              (a : A) → V →ₗ[R] CliffordAlgebra (QuadraticForm.baseChange A Q))
            1 :
          (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        x :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((((TensorProduct.AlgebraTensorModule.curry
                  (AlgHom.toLinearMap
                      (AlgHom.id A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))) ∘ₗ
                    ι (QuadraticForm.baseChange A Q)) :
                A →ₗ[A] V →ₗ[R] CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
              (a : A) → V →ₗ[R] CliffordAlgebra (QuadraticForm.baseChange A Q))
            1 :
          (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        x :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))

Tactic:
change ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x)))
    = ι (Q.baseChange A) (1 ⊗ₜ[R] x)

Premises used: CliffordAlgebra.ι, CliffordAlgebra.toBaseChange, TensorProduct.tmul, OfNat.ofNat, CliffordAlgebra.ofBaseChange, DFunLike.coe, QuadraticForm.baseChange
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
x : V
a :
  Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ofBaseChange A Q : (a : A ⊗[R] CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        (1 ⊗ₜ[R] (ι Q : (a : V) → CliffordAlgebra Q) x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
a₁ a₂ :
  Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ofBaseChange A Q : (a : A ⊗[R] CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
          ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
            (1 ⊗ₜ[R] x))) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))

Tactic:
rw [toBaseChange_ι, ofBaseChange_tmul_ι]

Premises used: CliffordAlgebra.ofBaseChange_tmul_ι, CliffordAlgebra.toBaseChange_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
x : CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)
⊢ (ofBaseChange A Q : (a : A ⊗[R] CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q) x) =
    x

Tactic:
AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q :) x

Premises used: Quotient.liftOn', AddCon.liftOn, AlgHom.congr_fun, CliffordAlgebra.ofBaseChange_comp_toBaseChange
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Semiring.toNatAlgebra = instAlgebra' Q

Tactic:
rfl

Premises used: CliffordAlgebra, RingQuot.smul, instRingCliffordAlgebra._aux_6, instRingCliffordAlgebra._aux_1, instRingCliffordAlgebra._aux_7, instRingCliffordAlgebra._aux_2, RingQuot.natCast, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Ring.toIntAlgebra (CliffordAlgebra Q) = instAlgebra' Q

Tactic:
rfl

Premises used: CliffordAlgebra, RingQuot.smul, RingQuot.intCast, instRingCliffordAlgebra._aux_6, instRingCliffordAlgebra._aux_1, instRingCliffordAlgebra._aux_7, instRingCliffordAlgebra._aux_2, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
Q_1 : QuadraticForm R_1 M_1
R : Type u_3
S : Type u_4
A : Type u_5
M : Type u_6
inst_3 : CommSemiring R
inst_4 : CommSemiring S
inst_5 : AddCommGroup M
inst_6 : CommRing A
inst_7 : Algebra R A
inst_8 : Algebra S A
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module A M
Q : QuadraticForm A M
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower S A M
⊢ SMulCommClass R S (CliffordAlgebra Q)

Tactic:
RingQuot.instSMulCommClass _

Premises used: CliffordAlgebra, RingQuot.instSMulCommClass
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
Q_1 : QuadraticForm R_1 M_1
R : Type u_3
S : Type u_4
A : Type u_5
M : Type u_6
inst_3 : CommSemiring R
inst_4 : CommSemiring S
inst_5 : AddCommGroup M
inst_6 : CommRing A
inst_7 : SMul R S
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : Module R M
inst_11 : Module S M
inst_12 : Module A M
inst_13 : IsScalarTower R A M
inst_14 : IsScalarTower S A M
inst_15 : IsScalarTower R S A
Q : QuadraticForm A M
⊢ IsScalarTower R S (CliffordAlgebra Q)

Tactic:
RingQuot.instIsScalarTower _

Premises used: CliffordAlgebra, RingQuot.instIsScalarTower
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
erw :
  Eq (α := CliffordAlgebra Q)
    ((RingQuot.mkAlgHom R (Rel Q) : (a : TensorAlgebra R M) → RingQuot (Rel Q))
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)) :
      RingQuot (Rel Q))
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((RingQuot.mkAlgHom R (Rel Q) : (a : TensorAlgebra R M) → RingQuot (Rel Q))
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m) :
        RingQuot (Rel Q))
      ((RingQuot.mkAlgHom R (Rel Q) : (a : TensorAlgebra R M) → RingQuot (Rel Q))
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m) :
        RingQuot (Rel Q)) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m)

Tactic:
erw [← map_mul (RingQuot.mkAlgHom R (Rel Q))]

Premises used: CliffordAlgebra.Rel, RingQuot.mkAlgHom, map_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (RingQuot (Rel Q)) : (a : R) → RingQuot (Rel Q)) ((Q : (a : M) → R) m) : RingQuot (Rel Q))
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((RingQuot.mkAlgHom R (Rel Q) : (a : TensorAlgebra R M) → RingQuot (Rel Q))
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)) :
      RingQuot (Rel Q))
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q)

Tactic:
rw [RingQuot.mkAlgHom_rel R (Rel.of m), AlgHom.commutes]

Premises used: CliffordAlgebra.Rel.of, RingQuot.mkAlgHom_rel, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra Q)
    ((algebraMap R (RingQuot (Rel Q)) : (a : R) → RingQuot (Rel Q)) ((Q : (a : M) → R) m) : RingQuot (Rel Q))
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
rw :
  Eq.{u_3 + 1} (α := A)
    ((g : (a : CliffordAlgebra Q) → A)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) :
      A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
rw₁ :
  Eq.{u_3 + 1} (α := A)
    ((g : (a : CliffordAlgebra Q) → A)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) :
      A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
⊢ HMul.hMul (α := A) (β := A)
      ((g : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A)
      ((g : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)

Tactic:
rw [← map_mul, ι_sq_scalar, AlgHom.commutes]

Premises used: CliffordAlgebra.ι_sq_scalar, map_mul, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f :
  { f : M →ₗ[R] A //
    ∀ (m : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }
x y : TensorAlgebra R M
h : Rel Q x y
of :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := A)
      ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
              TensorAlgebra R M →ₐ[R] A) :
            (a : TensorAlgebra R M) → A)
          (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)) :
        A)
      ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
              TensorAlgebra R M →ₐ[R] A) :
            (a : TensorAlgebra R M) → A)
          ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) ((Q : (a : M) → R) m) : TensorAlgebra R M) :
        A)
⊢ Eq.{u_3 + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
            TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        x :
      A)
    ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
            TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        y :
      A)

Tactic:
induction h
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f :
  { f : M →ₗ[R] A //
    ∀ (m : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }
x y : TensorAlgebra R M
m : M
of :
  Eq.{u_3 + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
            TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)) :
      A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
of₁ :
  HMul.hMul (α := A) (β := A)
      ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
              TensorAlgebra R M →ₐ[R] A) :
            (a : TensorAlgebra R M) → A)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M) :
        A)
      ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
              TensorAlgebra R M →ₐ[R] A) :
            (a : TensorAlgebra R M) → A)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M) :
        A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
of₂ :
  HMul.hMul (α := A) (β := A) (((↑f : M →ₗ[R] A) : (a : M) → A) m : A) (((↑f : M →ₗ[R] A) : (a : M) → A) m : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
of₃ of₄ :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
            TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)) :
      A)
    ((((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A) :
            TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) ((Q : (a : M) → R) m) : TensorAlgebra R M) :
      A)

Tactic:
rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]

Premises used: TensorAlgebra.lift_ι_apply, map_mul, Subtype.prop, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
rw :
  HMul.hMul (α := A) (β := A)
      ((F.toLinearMap : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A)
      ((F.toLinearMap : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
rw₁ :
  HMul.hMul (α := A) (β := A)
      ((F : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A)
      ((F : (a : CliffordAlgebra Q) → A) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A)
⊢ HMul.hMul (α := A) (β := A) ((F.toLinearMap ∘ₗ ι Q : (a : M) → A) m : A)
      ((F.toLinearMap ∘ₗ ι Q : (a : M) → A) m : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)

Tactic:
rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]

Premises used: LinearMap.comp_apply, AlgHom.toLinearMap_apply, CliffordAlgebra.comp_ι_sq_scalar