awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
fst :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) a
⊢ ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
        ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
            (a : A × ↥(S f)) → A × ↥(S f))
          (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).1 =
    (HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).1

Tactic:
change f.bilin m m * a = Q m • a

Premises used: CliffordAlgebra.EvenHom.bilin, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
fst :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a
fst₁ fst₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) a

Tactic:
rw [Algebra.smul_def, f.contract]

Premises used: CliffordAlgebra.EvenHom.contract, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
snd :
  ∀ (m₁ : M),
    Eq.{u_3 + 1} (α := A)
      (((↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                      (a : A × ↥(S f)) → A × ↥(S f))
                    ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                        (a : A × ↥(S f)) → A × ↥(S f))
                      (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
              M →ₗ[R] A) :
            (a : M) → A)
          m₁ :
        A)
      (((↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
              M →ₗ[R] A) :
            (a : M) → A)
          m₁ :
        A)
⊢ (↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
              (a : A × ↥(S f)) → A × ↥(S f))
            ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                (a : A × ↥(S f)) → A × ↥(S f))
              (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
      M →ₗ[R] A) =
    (↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
      M →ₗ[R] A)

Tactic:
ext m₁
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
snd :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
⊢ Eq.{u_3 + 1} (α := A)
    (((↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                    (a : A × ↥(S f)) → A × ↥(S f))
                  ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                      (a : A × ↥(S f)) → A × ↥(S f))
                    (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)
    (((↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)

Tactic:
change f.bilin _ _ * g m = Q m • g m₁

Premises used: CliffordAlgebra.EvenHom.bilin, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hg

Premises used: Submodule.span_induction
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
b : A
m₃ : M
snd :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m₃ : A) b) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
      (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) b)
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((((LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₃) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R b) :
              M →ₗ[R] A) :
            (a : M) → A)
          m :
        A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
      ((((LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₃) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R b) :
              M →ₗ[R] A) :
            (a : M) → A)
          m₁ :
        A)

Tactic:
change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)

Premises used: HMul.hMul, CliffordAlgebra.EvenHom.bilin, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
b : A
m₃ : M
snd :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m₃ : A) b) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) *
      b
snd₁ :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m₃ : A) *
      b =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) *
      b
snd₂ snd₃ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) *
      b =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) *
      b
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m₃ : A) b) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
      (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) b)

Tactic:
rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]

Premises used: mul_assoc, smul_mul_assoc, CliffordAlgebra.EvenHom.contract_mid
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((0 : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((0 : (a : M) → A) m₁ : A)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
x : R
hx : M →ₗ[R] A
_c :
  Membership.mem (γ := Submodule R (M →ₗ[R] A))
    (Submodule.span R
      {f' : M →ₗ[R] A |
        ∃ (x : A) (m₂ : M),
          f' =
            (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
              (LinearMap.mulRight R x)})
    hx
ihx :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((hx : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((hx : (a : M) → A) m₁ : A)
snd :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x • hx : (a : M) → A) m₁ : A)
snd₁ :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m₁ : A))
snd₂ :
  x •
      HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((hx : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m₁ : A))
snd₃ :
  x • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((hx : (a : M) → A) m₁ : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m₁ : A))
snd₄ snd₅ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m₁ : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) (HSMul.hSMul (β := A) x ((hx : (a : M) → A) m₁ : A))
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x • hx : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x • hx : (a : M) → A) m₁ : A)

Tactic:
rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]

Premises used: LinearMap.smul_apply, mul_smul_comm, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f_1 f : EvenHom Q A
refine : CliffordAlgebra Q →ₗ[R] A
⊢ ↥(even Q) →ₗ[R] A

Tactic:
refine ?_ ∘ₗ (even Q).val.toLinearMap

Premises used: AlgHom.toLinearMap, Subalgebra.val, CliffordAlgebra.even
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
⊢ Eq.{u_3 + 1} (α := A) ((aux f : (a : ↥(even Q)) → A) 1 : A) (1 : A)

Tactic:
congr_arg Prod.fst (foldr_one _ _ _ _)

Premises used: Prod.fst, congr_arg, CliffordAlgebra.foldr_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
r : R
⊢ Eq.{u_3 + 1} (α := A)
    ((aux f : (a : ↥(even Q)) → A) ((algebraMap R ↥(even Q) : (a : R) → ↥(even Q)) r : ↥(even Q)) : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
(congr_arg Prod.fst (foldr_algebraMap _ _ _ _ _)).trans (Algebra.algebraMap_eq_smul_one r).symm

Premises used: Prod.fst, congr_arg, CliffordAlgebra.foldr_algebraMap, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
x y : ↥(even Q)
obtain :
  ∀ (x : CliffordAlgebra Q) (x_property : x ∈ even Q),
    (aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property * y) =
      HMul.hMul (α := A) (β := A)
        ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property) : A)
        ((aux f : (a : ↥(even Q)) → A) y : A)
⊢ (aux f : (a : ↥(even Q)) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((aux f : (a : ↥(even Q)) → A) x : A) ((aux f : (a : ↥(even Q)) → A) y : A)

Tactic:
obtain ⟨x, x_property⟩ := x
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
y : ↥(even Q)
x : CliffordAlgebra Q
x_property : x ∈ even Q
mk :
  ∀ (val : CliffordAlgebra Q) (property : val ∈ even Q),
    (aux f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property *
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) val property) =
      HMul.hMul (α := A) (β := A)
        ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property) : A)
        ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) val property) : A)
⊢ (aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property * y) =
    HMul.hMul (α := A) (β := A)
      ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property) : A)
      ((aux f : (a : ↥(even Q)) → A) y : A)

Tactic:
cases y
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val : CliffordAlgebra Q
property : val ∈ even Q
⊢ (aux f : (a : ↥(even Q)) → A)
      (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property *
        Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) val property) =
    HMul.hMul (α := A) (β := A)
      ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x x_property) : A)
      ((aux f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) val property) : A)

Tactic:
(congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans ?_

Premises used: CliffordAlgebra.foldr_mul, Prod.fst, congr_arg, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift Q : (a : EvenHom Q A) → ↥(even Q) →ₐ[R] A) f : ↥(even Q) →ₐ[R] A) : (a : ↥(even Q)) → A)
        (((((ι Q).bilin : (a : M) → M →ₗ[R] ↥(even Q)) m₁ : M →ₗ[R] ↥(even Q)) : (a : M) → ↥(even Q)) m₂ : ↥(even Q)) :
      A)
    ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂ : A)

Tactic:
even.lift.aux_ι _ _ _

Premises used: CliffordAlgebra.even.lift.aux_ι
-- 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 × R
⊢ (Q' Q : (a : M × R) → R) m = HSub.hSub (α := R) ((Q : (a : M) → R) m.1 : R) (m.2 * m.2)

Tactic:
(sub_eq_add_neg _ _).symm

Premises used: sub_eq_add_neg, Eq.symm
-- 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
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
        ((Q' Q : (a : M × R) → R) (0, 1)) :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (-1 : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
simp
-- 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))
    ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
        ((Q' Q : (a : M × R) → R) ((LinearMap.inl R M R : (a : M) → M × R) m : M × R)) :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q))
        ((Q : (a : M) → R) m) :
      CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
simp
-- 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)) (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)

Tactic:
neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)

Premises used: CliffordAlgebra.ι_mul_ι_add_swap, neg_eq_of_add_eq_zero_right, Eq.trans
-- 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 :
  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
⊢ -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)

Tactic:
refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)

Premises used: CliffordAlgebra.ι_mul_ι_add_swap, neg_eq_of_add_eq_zero_right, Eq.trans
-- 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
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))
⊢ 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:
dsimp [QuadraticMap.polar]

Premises used: QuadraticMap.polar
-- 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))
    ((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:
simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero,
    add_sub_cancel_right, sub_self, map_zero]

Premises used: sub_self, map_zero, zero_add, MulZeroClass.mul_zero, add_sub_cancel_right, mul_one, add_zero, neg_zero
-- 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) =
    -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) =
    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]

Premises used: neg_eq_iff_eq_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
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))

Tactic:
(neg_e0_mul_v _ m).symm

Premises used: CliffordAlgebra.EquivEven.neg_e0_mul_v, Eq.symm
-- 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))
      ((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:
exact (neg_e0_mul_v _ m).symm

Premises used: CliffordAlgebra.EquivEven.neg_e0_mul_v, Eq.symm