awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (hypothesis)
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)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (hypothesis)
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)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
have hc : ∀ (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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)
have rw : HSub.hSub (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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: rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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
rw :
  HSub.hSub (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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)
⊢ 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)
have rw₁ : HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m.1) : CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (m.2 * m.2) : CliffordAlgebra Q) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
Tactic: rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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
rw :
  HSub.hSub (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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)
rw₁ :
  HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m.1) : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (m.2 * m.2) : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
⊢ 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)
have rw₂ : Eq (α := CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
      (HSub.hSub (α := R) ((Q : (a : M) → R) m.1 : R) (m.2 * m.2)) :
    CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m) : CliffordAlgebra Q)
Tactic: rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (hypothesis)
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
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
have refine_1 : ∀ (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: refine even.lift (Q' Q) ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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),
    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)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
have refine_2 : ∀ (m₁ m₂ m₃ : M × R),
  HMul.hMul (α := CliffordAlgebra Q) (β := 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)
      ((((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) m₂ : M × R →ₗ[R] CliffordAlgebra Q) :
            (a : M × R) → CliffordAlgebra Q)
          m₃ :
        CliffordAlgebra Q) =
    HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m₂ : R)
      ((((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) m₁ : M × R →ₗ[R] CliffordAlgebra Q) :
            (a : M × R) → CliffordAlgebra Q)
          m₃ :
        CliffordAlgebra Q)
Tactic: refine even.lift (Q' Q) ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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)
⊢ ∀ (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)
have 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)
Tactic: simp_rw [f_apply]