awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange (goal)
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
⊢ 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))
have 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))
Tactic: rw [toBaseChange_ι, ofBaseChange_tmul_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange (goal)
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))
⊢ 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))
have 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))
Tactic: rw [toBaseChange_ι, ofBaseChange_tmul_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: erw [← map_mul (RingQuot.mkAlgHom R (Rel Q))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
    ((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)
have 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)
Tactic: rw [RingQuot.mkAlgHom_rel R (Rel.of m), AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← map_mul, ι_sq_scalar, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, ι_sq_scalar, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, ι_sq_scalar, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]