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 : Module.Dual R M
r : R
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)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)

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

Premises used: smul_zero, CliffordAlgebra.foldr'_algebraMap, 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
r : R
⊢ ∀ (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
r : R
⊢ ∀ (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
r : R
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)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))) :
      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)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)
rw₂ : Eq (α := CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 0) 0
rw₃ rw₄ : Eq (α := CliffordAlgebra Q) 0 0
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)

Tactic:
rw [contractRight_eq, reverse.commutes, contractLeft_algebraMap, map_zero]

Premises used: CliffordAlgebra.contractRight_eq, map_zero, CliffordAlgebra.reverse.commutes, CliffordAlgebra.contractLeft_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 : Module.Dual R 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)
      1)
    0

Tactic:
simpa only [map_one] using contractLeft_algebraMap Q d 1

Premises used: map_one, OfNat.ofNat, CliffordAlgebra.contractLeft_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 : Module.Dual R M
⊢ Eq (α := CliffordAlgebra Q)
    (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) 1 :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d :
      CliffordAlgebra Q)
    (0 : CliffordAlgebra Q)

Tactic:
simpa only [map_one] using contractRight_algebraMap Q d 1

Premises used: CliffordAlgebra.contractRight_algebraMap, map_one, OfNat.ofNat
-- 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
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)
    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)
    (0 : CliffordAlgebra Q)

Tactic:
simp_rw [contractLeft_algebraMap, map_zero]

Premises used: map_zero, CliffordAlgebra.contractLeft_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 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)
algebraMap₁ : Eq (α := CliffordAlgebra Q) 0 (-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)

Tactic:
simp_rw [contractLeft_algebraMap, map_zero, neg_zero]

Premises used: map_zero, neg_zero, CliffordAlgebra.contractLeft_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
B : BilinForm R M
v : M
x : CliffordAlgebra Q
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
⊢ (((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

Tactic:
simp only [changeFormAux_apply_apply]

Premises used: CliffordAlgebra.changeFormAux_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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
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
⊢ 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

Tactic:
dsimp only [← BilinMap.toQuadraticMap_apply]

Premises used: LinearMap.BilinMap.toQuadraticMap_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 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
rw₂ rw₃ : HSMul.hSMul (α := 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

Tactic:
rw [h, QuadraticMap.sub_apply, sub_sub_cancel]

Premises used: QuadraticMap.sub_apply, sub_sub_cancel
-- 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
⊢ BilinMap.toQuadraticMap 0 = Q - Q

Tactic:
(sub_self _).symm

Premises used: sub_self, LinearMap.BilinMap.toQuadraticMap, Eq.symm
-- 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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
⊢ BilinMap.toQuadraticMap (B + B') = Q'' - Q

Tactic:
(congr_arg₂ (· + ·) h h').trans <| sub_add_sub_cancel' _ _ _

Premises used: sub_add_sub_cancel', HAdd.hAdd, LinearMap.BilinMap.toQuadraticMap, Eq.trans, congr_arg₂
-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ BilinMap.toQuadraticMap (-B) = Q - Q'

Tactic:
(congr_arg Neg.neg h).trans <| neg_sub _ _

Premises used: neg_sub, congr_arg, LinearMap.BilinMap.toQuadraticMap, Neg.neg, 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
inst_3 : Invertible (α := R) 2
⊢ BilinMap.toQuadraticMap
      (((QuadraticMap.associated.{u1, u2, u1} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
          (a : QuadraticMap R M R) → BilinMap R M R)
        (-Q)) =
    0 - Q

Tactic:
simp [QuadraticMap.toQuadraticMap_associated]

Premises used: QuadraticMap.toQuadraticMap_associated
-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
r : R
⊢ Eq (α := CliffordAlgebra Q')
    ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q')
    ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q') r : CliffordAlgebra Q')

Tactic:
(foldr_algebraMap _ _ _ _ _).trans <| Eq.symm <| Algebra.algebraMap_eq_smul_one r

Premises used: Algebra.algebraMap_eq_smul_one, CliffordAlgebra.foldr_algebraMap, Eq.symm, 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ Eq (α := CliffordAlgebra Q') ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') 1) 1

Tactic:
simpa using changeForm_algebraMap h (1 : R)

Premises used: CliffordAlgebra.changeForm_algebraMap, OfNat.ofNat
-- 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 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
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')
rw₂ :
  (ι Q' : (a : M) → CliffordAlgebra Q') m =
    HSub.hSub (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q') (0 : CliffordAlgebra Q')
rw₃ rw₄ :
  Eq (α := CliffordAlgebra Q') ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
    ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
⊢ 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')

Tactic:
rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]

Premises used: sub_zero, CliffordAlgebra.changeFormAux_apply_apply, mul_one, CliffordAlgebra.contractLeft_one
-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
rw :
  (((changeFormAux Q' B : (a : M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') m :
          CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
        (a : CliffordAlgebra Q') → CliffordAlgebra Q')
      (((foldr Q (changeFormAux Q' B) ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q') 1 :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q')
        x) =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q'))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q')
⊢ (((foldr Q (changeFormAux Q' B) ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q')
            (((foldr Q (changeFormAux Q' B) ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q')
                  1 :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q')
              x) :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q') :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q')
      ((ι Q : (a : M) → CliffordAlgebra Q) m) =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q'))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q')

Tactic:
rw [foldr_ι]

Premises used: CliffordAlgebra.foldr_ι
-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ (((changeFormAux Q' B : (a : M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') m :
          CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
        (a : CliffordAlgebra Q') → CliffordAlgebra Q')
      (((foldr Q (changeFormAux Q' B) ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q') 1 :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q')
        x) =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q'))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q')

Tactic:
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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
r : R
⊢ Eq (α := CliffordAlgebra Q')
    ((changeForm h : (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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q')

Tactic:
simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]

Premises used: map_zero, CliffordAlgebra.changeForm_algebraMap, CliffordAlgebra.contractLeft_algebraMap