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 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')
⊢ 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') (0 : CliffordAlgebra Q')
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
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')
⊢ 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₃ : Eq (α := CliffordAlgebra Q') ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
  ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
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
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')
have 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) sorry : (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: rw [foldr_ι]
-- 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₂ : M
⊢ (changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
      ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q')
          ((((B : (a : M) → M →ₗ[R] R) m₁ : M →ₗ[R] R) : (a : M) → R) m₂) :
        CliffordAlgebra Q')
have rw : 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') ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
        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') ((ι Q : (a : M) → CliffordAlgebra Q) m₂)) :
      CliffordAlgebra Q') =
  HSub.hSub (β := CliffordAlgebra Q')
    (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
    ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q')
        ((((B : (a : M) → M →ₗ[R] R) m₁ : M →ₗ[R] R) : (a : M) → R) m₂) :
      CliffordAlgebra Q')
Tactic: rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι]
-- 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
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ 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)
          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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q')
have algebraMap : ∀ (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: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]
  | add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx =>
    simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, map_smul]
    rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]
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
x y : CliffordAlgebra Q
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  x + y
Tactic: rw [map_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
x y : CliffordAlgebra Q
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add₁ : HAdd.hAdd (β := CliffordAlgebra Q) x
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  x + y
Tactic: rw [map_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
x y : CliffordAlgebra Q
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) x
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add₂ : x + y = x + y
Tactic: rw [map_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
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul : HSub.hSub (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
              ((0 : (a : M) → M →ₗ[R] R) m) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      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 : QuadraticForm R M
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul₁ : HSub.hSub (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
              ((0 : (a : M) → M →ₗ[R] R) m) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      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 : QuadraticForm R M
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₁ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul₂ : HSub.hSub (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
    (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) 0 :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      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 : QuadraticForm R M
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₁ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₂ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) 0 :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul₃ : HSub.hSub (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
    ((0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]