awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
ι :
  ∀ (m : M),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m) :
        CliffordAlgebra Q)
      (-(CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 1) (_hy : y ∈ evenOdd Q 1)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x)
    (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
have ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 1)
  (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x),
  (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
Tactic: induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
Cleared hypotheses: h
-- 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
v : M
x fx : CliffordAlgebra Q
⊢ (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
          CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x,
        (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
              CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
          (x, fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have simp : HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: simp 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 : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have rw : HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx)) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
    zero_add]
-- 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
v : M
x fx : CliffordAlgebra Q
rw :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
⊢ HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have rw₁ : HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
        fx) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
    zero_add]
-- 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
v : M
x fx : CliffordAlgebra Q
rw :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₁ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
          fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
⊢ HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have rw₂ : HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
      HMul.hMul (α := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) v) : CliffordAlgebra Q)
        fx) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
    zero_add]
-- 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
v : M
x fx : CliffordAlgebra Q
rw :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₁ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
          fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₂ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) v) : CliffordAlgebra Q)
          fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
⊢ HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have rw₃ : HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
      HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
    zero_add]
-- 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
r : R
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((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 =
  HSMul.hSMul (β := CliffordAlgebra Q) r 0 + HSMul.hSMul (β := CliffordAlgebra Q) r 0
Tactic: simp_rw [foldr'_algebraMap, smul_zero, zero_add]
-- 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
r : R
algebraMap :
  HSMul.hSMul (β := CliffordAlgebra Q) r 0 =
    HSMul.hSMul (β := CliffordAlgebra Q) r 0 + HSMul.hSMul (β := CliffordAlgebra Q) r 0
⊢ (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)
have algebraMap₁ : 0 = HAdd.hAdd (α := CliffordAlgebra Q) 0 0
Tactic: simp_rw [foldr'_algebraMap, smul_zero, zero_add]
-- 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 y : CliffordAlgebra Q
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)
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
      ((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 (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  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: rw [map_add, map_add, map_add, add_add_add_comm, 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 d' d₁ d₂ : Module.Dual R M
x y : CliffordAlgebra Q
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)
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
      ((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 (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y :
        CliffordAlgebra Q) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
      ((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 (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((foldr' Q (contractLeftAux Q (d₁ + d₂)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  HAdd.hAdd (β := 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) y : CliffordAlgebra Q))
    ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
Tactic: rw [map_add, map_add, map_add, add_add_add_comm, 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 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)
⊢ (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)
have ι_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₁) 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)) =
  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₁) sorry 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₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
Tactic: rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]