awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  -HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q) *
      e0 Q =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        (-(v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q) *
      e0 Q =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (-(v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q * e0 Q) =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (-(v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (-1 : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m
rw₄ :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (- -(v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw₅ rw₆ :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      e0 Q =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m

Tactic:
rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_neg]

Premises used: mul_assoc, neg_neg, CliffordAlgebra.EquivEven.neg_v_mul_e0, CliffordAlgebra.EquivEven.e0_mul_e0, neg_mul, mul_neg_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q)) ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m) :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
reverse_ι _

Premises used: CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((involute : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q)) ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m) :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (-(v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
involute_ι _

Premises used: CliffordAlgebra.involute_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q)) (e0 Q) = e0 Q

Tactic:
reverse_ι _

Premises used: CliffordAlgebra.EquivEven.e0, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (involute : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q)) (e0 Q) = -e0 Q

Tactic:
involute_ι _

Premises used: CliffordAlgebra.involute_ι, CliffordAlgebra.EquivEven.e0
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
refine_1 : M →ₗ[R] ↥(even (Q' Q))
refine_2 :
  ∀ (m : M),
    HMul.hMul (α := ↥(even (Q' Q))) (β := ↥(even (Q' Q)))
        ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q))) m :
          ↥(even (Q' Q)))
        ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q))) m :
          ↥(even (Q' Q))) =
      (algebraMap R ↥(even (Q' Q)) : (a : R) → ↥(even (Q' Q))) ((Q : (a : M) → R) m)
⊢ CliffordAlgebra Q →ₐ[R] ↥(even (Q' Q))

Tactic:
refine CliffordAlgebra.lift Q ⟨?_, fun m => ?_⟩

Premises used: Subtype.mk, CliffordAlgebra.lift, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
refine_1 : M →ₗ[R] CliffordAlgebra (R := R) (M := M × R) (Q' Q)
refine_1₁ :
  ∀ (m : M),
    Membership.mem (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (HPow.hPow (α := Submodule R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (β := ℕ) (LinearMap.range (ι (Q' Q)))
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 2 ⋯ :
              { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
          ℕ))
      ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
        CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ M →ₗ[R] ↥(even (Q' Q))

Tactic:
refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_

Premises used: Submodule.mem_iSup_of_mem, LinearMap.codRestrict
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] CliffordAlgebra (R := R) (M := M × R) (Q' Q)

Tactic:
exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)

Premises used: CliffordAlgebra.EquivEven.v, LinearMap.comp, LinearMap.mulLeft, CliffordAlgebra.EquivEven.e0
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
refine_1 :
  Membership.mem (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (HMul.hMul (α := Submodule R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (LinearMap.range (ι (Q' Q)))
      (LinearMap.range (ι (Q' Q))))
    ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ Membership.mem (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (HPow.hPow (α := Submodule R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (β := ℕ) (LinearMap.range (ι (Q' Q)))
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 2 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
        ℕ))
    ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
rw [Subtype.coe_mk, pow_two]

Premises used: Subtype.coe_mk, pow_two
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Membership.mem (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (HMul.hMul (α := Submodule R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (LinearMap.range (ι (Q' Q)))
      (LinearMap.range (ι (Q' Q))))
    ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)

Premises used: Submodule.mul_mem_mul, Set.Mem, LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Membership.mem (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (HMul.hMul (α := Submodule R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (LinearMap.range (ι (Q' Q)))
      (LinearMap.range (ι (Q' Q))))
    ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)

Premises used: Submodule.mul_mem_mul, LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
refine_2 :
  (↑(HMul.hMul (α := ↥(even (Q' Q))) (β := ↥(even (Q' Q)))
          ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q)))
              m :
            ↥(even (Q' Q)))
          ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q)))
              m :
            ↥(even (Q' Q)))) :
      CliffordAlgebra (Q' Q)) =
    (↑((algebraMap R ↥(even (Q' Q)) : (a : R) → ↥(even (Q' Q))) ((Q : (a : M) → R) m)) : CliffordAlgebra (Q' Q))
⊢ HMul.hMul (α := ↥(even (Q' Q))) (β := ↥(even (Q' Q)))
      ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q))) m :
        ↥(even (Q' Q)))
      ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ : (a : M) → ↥(even (Q' Q))) m :
        ↥(even (Q' Q))) =
    (algebraMap R ↥(even (Q' Q)) : (a : R) → ↥(even (Q' Q))) ((Q : (a : M) → R) m)

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
        CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m :
        CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    (↑((algebraMap R ↥(even (Q' Q)) : (a : R) → ↥(even (Q' Q))) ((Q : (a : M) → R) m)) : CliffordAlgebra (Q' Q))

Tactic:
simp [← mul_assoc, v_sq_scalar]

Premises used: mul_assoc, CliffordAlgebra.EquivEven.v_sq_scalar
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
simp :
  (↑((LinearMap.codRestrict
              ((Subalgebra.toSubmodule :
                  (a : Subalgebra R (CliffordAlgebra (Q' Q))) → Submodule R (CliffordAlgebra (Q' Q)))
                (even (Q' Q)))
              (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ :
            (a : M) → ↥(even (Q' Q)))
          m) :
      CliffordAlgebra (Q' Q)) =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra (Q' Q)) =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
simp only [toEven, CliffordAlgebra.lift_ι_apply, ← even_toSubmodule]

Premises used: CliffordAlgebra.lift_ι_apply, CliffordAlgebra.toEven, CliffordAlgebra.even_toSubmodule
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
rw :
  (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q : (a : M) → CliffordAlgebra (Q' Q)) m =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw₁ :
  Function.comp (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (⇑(LinearMap.mulLeft R (e0 Q)) : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (⇑(v Q) : (a : M) → CliffordAlgebra (Q' Q)) m =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw₂ :
  (LinearMap.mulLeft R (e0 Q) : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m) =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw₃ rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ (↑((LinearMap.codRestrict
              ((Subalgebra.toSubmodule :
                  (a : Subalgebra R (CliffordAlgebra (Q' Q))) → Submodule R (CliffordAlgebra (Q' Q)))
                (even (Q' Q)))
              (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯ :
            (a : M) → ↥(even (Q' Q)))
          m) :
      CliffordAlgebra (Q' Q)) =
    HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]

Premises used: LinearMap.mulLeft_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.codRestrict_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
x y : M × R
⊢ (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
        (a : M × R) → CliffordAlgebra Q)
      y =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
⊢ ∀ (x y : M × R),
    (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
          (a : M × R) → CliffordAlgebra Q)
        y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)

Tactic:
haveI f_apply : ∀ x y, f x y = (ι Q x.1 + algebraMap R _ x.2) * (ι Q y.1 - algebraMap R _ y.2) :=
    fun x y => by rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
          (a : M × R) → CliffordAlgebra Q)
        y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)
⊢ ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) x

Tactic:
haveI hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (algebraMap _ _ r) x := Algebra.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
          (a : M × R) → CliffordAlgebra Q)
        y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) x
⊢ ∀ (m : M × R),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q) =
      (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)

Tactic:
haveI hm :
    ∀ m : M × R,
      ι Q m.1 * ι Q m.1 - algebraMap R _ m.2 * algebraMap R _ m.2 = algebraMap R _ (Q' Q m) := by
    intro m
    rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
          (a : M × R) → CliffordAlgebra Q)
        y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) x
hm :
  ∀ (m : M × R),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q) =
      (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
refine_1 :
  ∀ (m : M × R),
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q) =
      (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
⊢ ∀ (m : M × R),
    Eq (α := CliffordAlgebra Q)
      ((((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) m : M × R →ₗ[R] CliffordAlgebra Q) :
            (a : M × R) → CliffordAlgebra Q)
          m :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m) :
        CliffordAlgebra Q)

Tactic:
simp_rw [f_apply]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x y : M × R
⊢ (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      ((((EvenHom.bilin (R := R) (M := M × R) (Q := Q' Q) (even.ι (Q' Q)) : (a : M × R) → M × R →ₗ[R] ↥(even (Q' Q)))
              x :
            M × R →ₗ[R] ↥(even (Q' Q))) :
          (a : M × R) → ↥(even (Q' Q)))
        y) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)

Tactic:
even.lift_ι (Q' Q) _ x y

Premises used: CliffordAlgebra.EquivEven.Q', CliffordAlgebra.even.lift_ι