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
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)
          ((reverse : (a : CliffordAlgebra Q) → 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)
    (0 : 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)
          ((reverse : (a : CliffordAlgebra Q) → 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)
    (0 : 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)
          ((((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)
    (0 : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] 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) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)
have rw₃ : Eq (α := CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 0) 0
Tactic: rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_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 : Module.Dual R M
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)
          ((reverse : (a : CliffordAlgebra Q) → 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)
    (0 : 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)
          ((reverse : (a : CliffordAlgebra Q) → 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)
    (0 : 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)
          ((((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)
    (0 : CliffordAlgebra Q)
rw₃ : Eq (α := CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 0) 0
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] 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) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)
have rw₄ : Eq (α := CliffordAlgebra Q) 0 0
Tactic: rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_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 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)
        ((((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)
    (-(((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (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)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
have algebraMap : 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)
    0)
  (-(((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      0)
Tactic: simp_rw [contractLeft_algebraMap, map_zero, neg_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 d' : Module.Dual R M
r : R
algebraMap :
  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)
      0)
    (-(((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        0)
⊢ 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)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.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)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
have algebraMap₁ : Eq (α := CliffordAlgebra Q) 0 (-0)
Tactic: simp_rw [contractLeft_algebraMap, map_zero, neg_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 d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ 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)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x) :
      CliffordAlgebra Q)
    (-(((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (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)
            x) :
      CliffordAlgebra Q)
have algebraMap : ∀ (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)
        ((((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)
    (-(((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (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)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [contractLeft_algebraMap, map_zero, neg_zero]
  | add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]
  | ι_mul _ _ hx =>
    simp only [contractLeft_ι_mul, map_sub, map_smul]
    rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]
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' : Module.Dual R M
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] 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) :
            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)
                ((((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') :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
      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)
          ((((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)
  (-(((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] 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') :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
    CliffordAlgebra Q)
Tactic: rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse,
    reverse_reverse, contractLeft_comm, map_neg]
-- 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
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (((changeFormAux Q B : (a : M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((changeFormAux Q B : (a : M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        x) =
    HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) v : R)
        ((((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) v : R) •
      x
have simp : HSub.hSub (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
      (HSub.hSub (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                  ((B : (a : M) → Module.Dual R M) v) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            x :
          CliffordAlgebra Q)))
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
              ((B : (a : M) → Module.Dual R M) v) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HSub.hSub (β := CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                    ((B : (a : M) → Module.Dual R M) v) :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              x :
            CliffordAlgebra Q)) :
      CliffordAlgebra Q) =
  HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) v : R)
      ((((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) v : R) •
    x
Tactic: simp only [changeFormAux_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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R)
        ((((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) m : R) •
      x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
have dsimp : HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((BilinMap.toQuadraticMap B : (a : M) → R) m : R) • x =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
Tactic: dsimp only [← BilinMap.toQuadraticMap_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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((BilinMap.toQuadraticMap B : (a : M) → R) m : R) • x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
have rw : HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((Q' - Q : (a : M) → R) m : R) • x =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
Tactic: rw [h, QuadraticMap.sub_apply, sub_sub_cancel]
-- 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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
rw :
  HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((Q' - Q : (a : M) → R) m : R) • x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
⊢ HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((BilinMap.toQuadraticMap B : (a : M) → R) m : R) • x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
have rw₁ : HSub.hSub (α := R) ((Q' : (a : M) → R) m : R)
      (HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((Q : (a : M) → R) m : R)) •
    x =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
Tactic: rw [h, QuadraticMap.sub_apply, sub_sub_cancel]
-- 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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
rw :
  HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((Q' - Q : (a : M) → R) m : R) • x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
rw₁ :
  HSub.hSub (α := R) ((Q' : (a : M) → R) m : R)
        (HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((Q : (a : M) → R) m : R)) •
      x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
⊢ HSub.hSub (α := R) (β := R) ((Q' : (a : M) → R) m : R) ((BilinMap.toQuadraticMap B : (a : M) → R) m : R) • x =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
have rw₂ : HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x = HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
Tactic: rw [h, QuadraticMap.sub_apply, sub_sub_cancel]
-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ Eq (α := CliffordAlgebra Q') ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
    ((((changeFormAux Q' B : (a : M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') m :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        1 :
      CliffordAlgebra Q')
have rw : (ι Q' : (a : M) → CliffordAlgebra Q') m =
  HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q') (1 : CliffordAlgebra Q') -
    (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
            ((B : (a : M) → Module.Dual R M) m) :
          CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
        (a : CliffordAlgebra Q') → CliffordAlgebra Q')
      1
Tactic: rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
rw :
  (ι Q' : (a : M) → CliffordAlgebra Q') m =
    HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q') (1 : CliffordAlgebra Q') -
      (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
              ((B : (a : M) → Module.Dual R M) m) :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        1
⊢ Eq (α := CliffordAlgebra Q') ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
    ((((changeFormAux Q' B : (a : M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') m :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        1 :
      CliffordAlgebra Q')
have rw₁ : (ι Q' : (a : M) → CliffordAlgebra Q') m =
  HSub.hSub (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
    ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
              ((B : (a : M) → Module.Dual R M) m) :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        1 :
      CliffordAlgebra Q')
Tactic: rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]