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
v : V
⊢ HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      (((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (ι (QuadraticForm.baseChange A Q)) ∘ₗ
              (TensorProduct.mk R A V : (a : A) → V →ₗ[R] A ⊗[R] V) 1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          v :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      (((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (ι (QuadraticForm.baseChange A Q)) ∘ₗ
              (TensorProduct.mk R A V : (a : A) → V →ₗ[R] A ⊗[R] V) 1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          v :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((Q : (a : V) → R) v)

Tactic:
(CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_

Premises used: CliffordAlgebra.ι_sq_scalar, TensorProduct.tmul, OfNat.ofNat, AddCon.toQuotient, QuadraticForm.baseChange, Eq.trans
-- 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 (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ofBaseChangeAux A Q : (a : CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((ι Q : (a : V) → CliffordAlgebra Q) v) :
      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] v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))

Tactic:
CliffordAlgebra.lift_ι_apply _ _ v

Premises used: CliffordAlgebra.lift_ι_apply, TensorProduct.tmul, AddCon.toQuotient
-- 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
z : A
v : V
change :
  HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
            (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          z :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((ofBaseChangeAux A Q : (a : CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          ((ι Q : (a : V) → CliffordAlgebra Q) v) :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
⊢ 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))
        (z ⊗ₜ[R] (ι Q : (a : V) → CliffordAlgebra Q) v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))

Tactic:
change algebraMap _ _ z * ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)

Premises used: CliffordAlgebra.ι, Algebra.algebraMap, TensorProduct.tmul, CliffordAlgebra.ofBaseChangeAux, 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
z : A
change :
  HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
            (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          z :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((ofBaseChangeAux A Q : (a : CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q)) 1 :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      z
⊢ 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)) (z ⊗ₜ[R] 1) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        z :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))

Tactic:
change algebraMap _ _ z * ofBaseChangeAux A Q 1 = _

Premises used: Algebra.algebraMap, CliffordAlgebra.ofBaseChangeAux, OfNat.ofNat, DFunLike.coe
-- 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
z : A
rw :
  HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
            (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          z :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      (1 : CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      z
rw₁ rw₂ :
  Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        z :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        z :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
⊢ HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
            (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          z :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      ((ofBaseChangeAux A Q : (a : CliffordAlgebra Q) → CliffordAlgebra (QuadraticForm.baseChange A Q)) 1 :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      z

Tactic:
rw [map_one, mul_one]

Premises used: map_one, mul_one
-- 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
refine :
  ∀ (m : A ⊗[R] V),
    HMul.hMul (α := A ⊗[R] CliffordAlgebra Q) (β := A ⊗[R] CliffordAlgebra Q)
        (((TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) : A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
              (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q)
            m :
          A ⊗[R] CliffordAlgebra Q)
        (((TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) : A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
              (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q)
            m :
          A ⊗[R] CliffordAlgebra Q) =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q) : (a : A) → A ⊗[R] CliffordAlgebra Q)
        ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) m)
⊢ { f : A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q //
    ∀ (m : A ⊗[R] V),
      HMul.hMul (α := A ⊗[R] CliffordAlgebra Q) (β := A ⊗[R] CliffordAlgebra Q)
          ((f : (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q) m : A ⊗[R] CliffordAlgebra Q)
          ((f : (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q) m : A ⊗[R] CliffordAlgebra Q) =
        (algebraMap A (A ⊗[R] CliffordAlgebra Q) : (a : A) → A ⊗[R] CliffordAlgebra Q)
          ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) m) }

Tactic:
refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
-- 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
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Invertible (α := A ⊗[R] CliffordAlgebra Q) 2 :=
  Invertible.copy (r := (algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2)
    (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2 :
      Invertible (α := A ⊗[R] CliffordAlgebra Q)
        ((algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2))
    2 ⋯
hpure_tensor :
  ∀ (v w : V),
    HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
      ((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                    LinearMap.BilinMap A (A ⊗[R] V) A) :
                  (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
                (1 ⊗ₜ[R] v) :
              A ⊗[R] V →ₗ[A] A) :
            (a : A ⊗[R] V) → A)
          (1 ⊗ₜ[R] w) ⊗ₜ[R]
        1
⊢ HAdd.hAdd (α := A ⊗[R] V →ₗ[A] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
      (LinearMap.compl₂ (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q))
          (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
        TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q))
      (LinearMap.compl₂ (LinearMap.flip (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)))
          (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
        TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) =
    LinearMap.compr₂ (QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q))
      (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q))

Tactic:
TensorProduct.AlgebraTensorModule.curry_injective ?_

Premises used: TensorProduct.AlgebraTensorModule.curry_injective
-- 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
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Invertible (α := A ⊗[R] CliffordAlgebra Q) 2 :=
  Invertible.copy (r := (algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2)
    (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2 :
      Invertible (α := A ⊗[R] CliffordAlgebra Q)
        ((algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2))
    2 ⋯
hpure_tensor :
  ∀ (v w : V),
    HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
      ((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                    LinearMap.BilinMap A (A ⊗[R] V) A) :
                  (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
                (1 ⊗ₜ[R] v) :
              A ⊗[R] V →ₗ[A] A) :
            (a : A ⊗[R] V) → A)
          (1 ⊗ₜ[R] w) ⊗ₜ[R]
        1
v w : V
⊢ HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
    QuadraticMap.polar (M := A ⊗[R] V) (⇑(QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → A) (1 ⊗ₜ[R] v)
        (1 ⊗ₜ[R] w) ⊗ₜ[R]
      1

Tactic:
hpure_tensor v w

Premises used: QuadraticMap.polar
-- 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
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Invertible (α := A ⊗[R] CliffordAlgebra Q) 2 :=
  Invertible.copy (r := (algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2)
    (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2 :
      Invertible (α := A ⊗[R] CliffordAlgebra Q)
        ((algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2))
    2 ⋯
hpure_tensor :
  ∀ (v w : V),
    HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
      ((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                    LinearMap.BilinMap A (A ⊗[R] V) A) :
                  (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
                (1 ⊗ₜ[R] v) :
              A ⊗[R] V →ₗ[A] A) :
            (a : A ⊗[R] V) → A)
          (1 ⊗ₜ[R] w) ⊗ₜ[R]
        1
v w : V
⊢ HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
    QuadraticMap.polar (M := A ⊗[R] V) (⇑(QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → A) (1 ⊗ₜ[R] v)
        (1 ⊗ₜ[R] w) ⊗ₜ[R]
      1

Tactic:
exact hpure_tensor v w
-- 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
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Invertible (α := A ⊗[R] CliffordAlgebra Q) 2 :=
  Invertible.copy (r := (algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2)
    (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2 :
      Invertible (α := A ⊗[R] CliffordAlgebra Q)
        ((algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2))
    2 ⋯
suffices :
  ∀ (v w : V),
    HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
        (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
            ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
      ((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                    LinearMap.BilinMap A (A ⊗[R] V) A) :
                  (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
                (1 ⊗ₜ[R] v) :
              A ⊗[R] V →ₗ[A] A) :
            (a : A ⊗[R] V) → A)
          (1 ⊗ₜ[R] w) ⊗ₜ[R]
        1
⊢ ∀ (m : A ⊗[R] V),
    HMul.hMul (α := A ⊗[R] CliffordAlgebra Q) (β := A ⊗[R] CliffordAlgebra Q)
        (((TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) : A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
              (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q)
            m :
          A ⊗[R] CliffordAlgebra Q)
        (((TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) : A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
              (a : A ⊗[R] V) → A ⊗[R] CliffordAlgebra Q)
            m :
          A ⊗[R] CliffordAlgebra Q) =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q) : (a : A) → A ⊗[R] CliffordAlgebra Q)
        ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) m)

Tactic:
suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) =
        QuadraticMap.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by
      -- the crux is that by converting to a statement about linear maps instead of quadratic forms,
      -- we then have access to all the partially-applied `ext` lemmas.
      rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
      refine TensorProduct.AlgebraTensorModule.curry_injective ?_
      ext v w
      dsimp
      exact hpure_tensor v w
-- 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
z : A
v : V
⊢ Eq (α := A ⊗[R] CliffordAlgebra 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))
          (z ⊗ₜ[R] v)) :
      A ⊗[R] CliffordAlgebra Q)
    (z ⊗ₜ[R] (ι Q : (a : V) → CliffordAlgebra Q) v : A ⊗[R] CliffordAlgebra Q)

Tactic:
CliffordAlgebra.lift_ι_apply _ _ _

Premises used: CliffordAlgebra.lift_ι_apply, Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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 :
  ∀ (v : V),
    Eq (α := A ⊗[R] CliffordAlgebra Q)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap (AlgHom.comp (toBaseChange A Q) involute) ∘ₗ ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] A ⊗[R] CliffordAlgebra Q) :
                (a : A) → V →ₗ[R] A ⊗[R] CliffordAlgebra Q)
              1 :
            (a : V) → A ⊗[R] CliffordAlgebra Q)
          v :
        A ⊗[R] CliffordAlgebra Q)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap
                        (AlgHom.comp
                          (Algebra.TensorProduct.map (AlgHom.id A A) involute :
                            A ⊗[R] CliffordAlgebra Q →ₐ[A] A ⊗[R] CliffordAlgebra Q)
                          (toBaseChange A Q :
                            CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A]
                              A ⊗[R] CliffordAlgebra Q)) ∘ₗ
                      ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] A ⊗[R] CliffordAlgebra Q) :
                (a : A) → V →ₗ[R] A ⊗[R] CliffordAlgebra Q)
              1 :
            (a : V) → A ⊗[R] CliffordAlgebra Q)
          v :
        A ⊗[R] CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] A ⊗[R] CliffordAlgebra Q)
    (AlgHom.comp (toBaseChange A Q) involute)
    (AlgHom.comp
      (Algebra.TensorProduct.map (AlgHom.id A A) involute : A ⊗[R] CliffordAlgebra Q →ₐ[A] A ⊗[R] CliffordAlgebra Q)
      (toBaseChange A Q :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] A ⊗[R] CliffordAlgebra Q))

Tactic:
ext v