awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
ι_mul :
  (((contractLeftAux Q (d₁ + 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,
        HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := 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)
          (x, (foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        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)
          (x, (foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
        CliffordAlgebra Q)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]

Premises used: CliffordAlgebra.foldr'_ι_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
rw :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (foldr' Q (contractLeftAux Q d) ⋯ 0) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q)

Tactic:
rw [LinearMap.smul_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
r : R
algebraMap : HSMul.hSMul (β := CliffordAlgebra Q) r 0 = c • HSMul.hSMul (β := CliffordAlgebra Q) r 0
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)

Tactic:
simp_rw [foldr'_algebraMap, smul_zero]

Premises used: smul_zero, CliffordAlgebra.foldr'_algebraMap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
ι_mul :
  (((contractLeftAux Q (c • 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,
        HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((((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, (foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
        CliffordAlgebra Q)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, hx]

Premises used: CliffordAlgebra.foldr'_ι_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
ι_mul :
  HSMul.hSMul (α := R) ((c • d : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        (HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    c •
      (HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
⊢ (((contractLeftAux Q (c • 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,
        HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((((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, (foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)

Tactic:
dsimp only [contractLeftAux_apply_apply]

Premises used: CliffordAlgebra.contractLeftAux_apply_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      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) x)) :
      CliffordAlgebra Q)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : 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) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) b) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            b :
          CliffordAlgebra Q)

Tactic:
foldr'_ι_mul _ _ ?_ _ _ _

Premises used: CliffordAlgebra.foldr'_ι_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
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
⊢ (((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) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) b) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            b :
          CliffordAlgebra Q)

Tactic:
refine foldr'_ι_mul _ _ ?_ _ _ _

Premises used: CliffordAlgebra.foldr'_ι_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ∀ (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:
fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Premises used: CliffordAlgebra.contractLeftAux_contractLeftAux
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ∀ (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:
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Premises used: CliffordAlgebra.contractLeftAux_contractLeftAux
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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)
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)
⊢ 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)

Tactic:
simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]

Premises used: sub_zero, MulZeroClass.mul_zero, Algebra.algebraMap_eq_smul_one, CliffordAlgebra.contractLeftAux_apply_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
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
⊢ 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)

Tactic:
refine (foldr'_ι _ _ ?_ _ _).trans <| by
    simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
      Algebra.algebraMap_eq_smul_one]

Premises used: CliffordAlgebra.foldr'_ι, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ∀ (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:
fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Premises used: CliffordAlgebra.contractLeftAux_contractLeftAux
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ∀ (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:
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Premises used: CliffordAlgebra.contractLeftAux_contractLeftAux
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]

Premises used: CliffordAlgebra.contractRight_eq, CliffordAlgebra.reverse.commutes, CliffordAlgebra.contractLeft_ι, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ 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)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)

Tactic:
(foldr'_algebraMap _ _ ?_ _ _).trans <| smul_zero _

Premises used: smul_zero, CliffordAlgebra.foldr'_algebraMap, Eq.trans