awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : 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)) =
    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)
have refine : Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
  ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
    (QuadraticMap.polar (M := M × R) (⇑(Q' Q) : (a : M × R) → R) (0, 1) ((LinearMap.inl R M R : (a : M) → M × R) m)))
  0
Tactic: refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)
-- 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
m : M
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
      (QuadraticMap.polar (M := M × R) (⇑(Q' Q) : (a : M × R) → R) (0, 1) ((LinearMap.inl R M R : (a : M) → M × R) m)))
    0
have dsimp : Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
  ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
      (HAdd.hAdd (α := R) ((Q : (a : M) → R) (0 + m) : R) (-(HAdd.hAdd (α := R) 1 0 * HAdd.hAdd (α := R) 1 0)) -
          HAdd.hAdd (α := R) ((Q : (a : M) → R) 0 : R) (-HMul.hMul (α := R) 1 1) -
        HAdd.hAdd (α := R) ((Q : (a : M) → R) m : R) (-HMul.hMul (α := R) 0 0)) :
    CliffordAlgebra (R := R) (M := M × R) (Q' Q))
  (0 : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
Tactic: dsimp [QuadraticMap.polar]
-- 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
m : M
⊢ -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) =
    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))
have 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) =
  -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 [neg_eq_iff_eq_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
m : 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)) *
      e0 Q =
    (v Q : (a : M) → CliffordAlgebra (Q' Q)) m
have 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
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
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
⊢ 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
have 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
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
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
⊢ 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
have 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
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
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
⊢ 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
have 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
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
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
⊢ 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
have 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))
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
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))
⊢ 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
have 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))
Tactic: rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_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
⊢ CliffordAlgebra Q →ₐ[R] ↥(even (Q' Q))
have refine_1 : M →ₗ[R] ↥(even (Q' Q))
Tactic: refine CliffordAlgebra.lift Q ⟨?_, fun m => ?_⟩
-- 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
refine_1 : M →ₗ[R] ↥(even (Q' Q))
⊢ CliffordAlgebra Q →ₐ[R] ↥(even (Q' Q))
have 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) sorry : (a : M) → ↥(even (Q' Q))) m :
        ↥(even (Q' Q)))
      ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) sorry : (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: refine CliffordAlgebra.lift Q ⟨?_, fun m => ?_⟩
-- 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
⊢ M →ₗ[R] ↥(even (Q' Q))
have refine_1 : M →ₗ[R] CliffordAlgebra (R := R) (M := M × R) (Q' Q)
Tactic: refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_
-- 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
refine_1 : M →ₗ[R] CliffordAlgebra (R := R) (M := M × R) (Q' Q)
⊢ M →ₗ[R] ↥(even (Q' Q))
have 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 sorry :
            { 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: refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_
-- 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
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))
have 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))
Tactic: rw [Subtype.coe_mk, pow_two]
-- 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
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)
have refine_2 : (↑(HMul.hMul (α := ↥(even (Q' Q))) (β := ↥(even (Q' Q)))
        ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) sorry : (a : M) → ↥(even (Q' Q))) m :
          ↥(even (Q' Q)))
        ((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) sorry : (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))
Tactic: ext1
-- 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
m : M
⊢ (↑((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))
have 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) sorry :
          (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: simp only [toEven, CliffordAlgebra.lift_ι_apply, ← even_toSubmodule]
-- 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
m : M
⊢ (↑((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))
have 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))
Tactic: rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
-- 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
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))
⊢ (↑((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))
have 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))
Tactic: rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
-- 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
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))
⊢ (↑((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))
have 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))
Tactic: rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
-- 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
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))
⊢ (↑((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))
have 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))
Tactic: rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]