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 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)
⊢ HSMul.hSMul (α := R) ((d₁ + d₂ : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        (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)) =
    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) +
      (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))
have ι_mul : HSMul.hSMul (α := R) ((d₁ + d₂ : (a : M) → R) m : R) x -
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
  HSMul.hSMul (α := R) ((d₁ : (a : M) → R) m : R) x + 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₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
Tactic: rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]
-- 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 d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (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)
have algebraMap : ∀ (r : R),
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero, zero_add]
      | add _ _ hx hy => rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]
Cleared hypotheses: x
-- 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 d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
          CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
          CliffordAlgebra Q)
⊢ (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)
have add : ∀ (x y : CliffordAlgebra Q)
  (hx :
    (foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
  (hy :
    (foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)),
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero, zero_add]
      | add _ _ hx hy => rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]
Cleared hypotheses: x
-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
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)
have rw : (foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
  HSMul.hSMul (β := CliffordAlgebra Q) c
    ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: rw [LinearMap.smul_apply, RingHom.id_apply]
-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
r : R
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((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)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
have algebraMap : HSMul.hSMul (β := CliffordAlgebra Q) r 0 = c • HSMul.hSMul (β := CliffordAlgebra Q) r 0
Tactic: simp_rw [foldr'_algebraMap, smul_zero]
-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x y : CliffordAlgebra Q
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)
hy :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
have add : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  HSMul.hSMul (β := CliffordAlgebra Q) c
    ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
Tactic: rw [map_add, map_add, smul_add, hx, hy]
-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x y : CliffordAlgebra Q
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)
hy :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
have add₁ : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  c •
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
Tactic: rw [map_add, map_add, smul_add, hx, hy]
-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x y : CliffordAlgebra Q
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)
hy :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
add₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    c •
      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) y : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
have add₂ : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
Tactic: rw [map_add, map_add, smul_add, hx, hy]
-- 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_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)
⊢ (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)
have ι_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) sorry 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) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
Tactic: rw [foldr'_ι_mul, foldr'_ι_mul, hx]
-- 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_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)
⊢ (((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)
have ι_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) sorry 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) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
Tactic: dsimp only [contractLeftAux_apply_apply]
-- 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_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)
⊢ 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))
have ι_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) sorry 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) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
Tactic: rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]