awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
rw :
  (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) a) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          a :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q) a
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          a :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw₁ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        a :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        a :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (α := CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
have rw : (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) (r • b) :
        Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
      (a : Module.Dual R M) → CliffordAlgebra Q)
    d =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
Tactic: rw [← Algebra.smul_def, LinearMap.map_smul₂, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
rw :
  (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) (r • b) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (α := CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
have rw₁ : HSMul.hSMul (β := CliffordAlgebra Q) r
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
Tactic: rw [← Algebra.smul_def, LinearMap.map_smul₂, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (β := CliffordAlgebra Q) a
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw : (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) a) :
        Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
      (a : Module.Dual R M) → CliffordAlgebra Q)
    d =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: rw [← Algebra.commutes, contractRight_algebraMap_mul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
rw :
  (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (α := CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) a) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (β := CliffordAlgebra Q) a
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw₁ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: rw [← Algebra.commutes, contractRight_algebraMap_mul, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) x :
            CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
        (1, 0) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have simp_rw : HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 -
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
Tactic: simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
simp_rw :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) x :
            CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
        (1, 0) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have simp_rw₁ : HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 - 0 =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
Tactic: simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
simp_rw :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
simp_rw₁ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 - 0 =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) x :
            CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
        (1, 0) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have simp_rw₂ : HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) x : R) 1 =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)
Tactic: simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have refine : ∀ (m : M) (x fx : CliffordAlgebra Q),
  (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) m :
          CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
        (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) m :
              CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
          (x, fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) fx
Tactic: refine (foldr'_ι _ _ ?_ _ _).trans <| by
    simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((ι Q : (a : M) → CliffordAlgebra Q) x) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have rw : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x))) :
    CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
Tactic: rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x))) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((ι Q : (a : M) → CliffordAlgebra Q) x) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have rw₁ : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
    CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
Tactic: rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x))) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((ι Q : (a : M) → CliffordAlgebra Q) x) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have rw₂ : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)) :
    CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
Tactic: rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x))) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
rw₂ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x)) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((ι Q : (a : M) → CliffordAlgebra Q) x) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
have rw₃ : Eq (α := CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((d : (a : M) → R) x) : CliffordAlgebra Q)
Tactic: rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]