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
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x x_1 x_2 : M
⊢ Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q))
        ⋯ +
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯

Tactic:
rfl
-- 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
x : R
x_1 x_2 : M
simp :
  Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (x •
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    x •
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯
⊢ (fun (m₁ m₂ : M) ↦
        Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
          ⋯)
      x_1 (x • x_2) =
    HSMul.hSMul (β := ↥(even Q)) x
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
            ⋯)
        x_1 x_2)

Tactic:
simp only [map_smul, mul_smul_comm]

Premises used: mul_smul_comm, map_smul
-- 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
m₁ m₂ m₃ : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- 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 g : ↥(even Q) →ₐ[R] A
h : (ι Q).compr₂ f = (ι Q).compr₂ g
⊢ ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin

Tactic:
rw [EvenHom.ext_iff] at h

Premises used: CliffordAlgebra.EvenHom.ext_iff
-- 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
H :
  ∀ (x : CliffordAlgebra Q) (hx : x ∈ even Q),
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
⊢ f = g

Tactic:
ext ⟨x, hx⟩
-- 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
r : R
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
          ↥(even Q)) :
      A)
    ((g : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
          ↥(even Q)) :
      A)

Tactic:
(f.commutes r).trans (g.commutes r).symm

Premises used: Set.Mem, AlgHom.commutes, Eq.symm, 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
r : R
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
          ↥(even Q)) :
      A)
    ((g : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
          ↥(even Q)) :
      A)

Tactic:
exact (f.commutes r).trans (g.commutes r).symm

Premises used: AlgHom.commutes, Eq.symm, 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
ihy :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))

Tactic:
have := congr_arg₂ (· + ·) ihx ihy
-- 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
ihy :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
this :
  Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)

Tactic:
(map_add f _ _).trans (this.trans <| (map_add g _ _).symm)

Premises used: Set.Mem, map_add, Eq.symm, 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
ihy :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
this :
  Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))
    ((fun (x1 x2 : A) ↦ x1 + x2)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx))
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy)))
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)

Tactic:
exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)

Premises used: map_add, Eq.symm, 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ f).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ g).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))

Tactic:
have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
-- 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
this :
  Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ f).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ g).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
            x)
          ⋯) :
      A)
    ((g : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
            x)
          ⋯) :
      A)

Tactic:
(map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)

Premises used: Set.Mem, map_mul, Eq.symm, 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih :
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
this :
  Eq.{u_3 + 1} (α := A)
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ f).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))
    ((fun (x1 x2 : A) ↦ x1 * x2) ((((((ι Q).compr₂ g).bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx)))
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
            x)
          ⋯) :
      A)
    ((g : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
            x)
          ⋯) :
      A)

Tactic:
exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)

Premises used: map_mul, Eq.symm, 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
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
rw :
  HAdd.hAdd (α := 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) *
      a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
rw₁ rw₂ :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (m₁ + m₂) : A) a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1

Tactic:
rw [map_add, add_mul]

Premises used: add_mul, map_add
-- 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 : EvenHom Q A
c : R
m : M
a : A × ↥(S f)
m₃ : M
rw :
  HSMul.hSMul (β := A) c ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) * a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
rw₁ rw₂ :
  c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (c • m) : A) a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1

Tactic:
rw [map_smul, smul_mul_assoc]

Premises used: smul_mul_assoc, map_smul
-- 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
x : 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))
        ((((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))
          x)).1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₂ : A) x.1

Tactic:
rfl

Premises used: rfl
-- 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₃ : M
x : 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))
                ((((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))
                  x)).2 :
          M →ₗ[R] A) :
        (a : M) → A)
      m₃ =
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A)
      (((↑x.2 : M →ₗ[R] A) : (a : M) → A) m₂ : A)

Tactic:
rfl

Premises used: rfl
-- 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
x : A × ↥(S f)
obtain :
  ∀ (a : A) (g : M →ₗ[R] A) (hg : g ∈ 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))
        ((((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)) =
      HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)
⊢ (((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))
        x) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x

Tactic:
obtain ⟨a, ⟨g, hg⟩⟩ := 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
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
fst :
  ((((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
snd :
  (↑((((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)
⊢ (((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)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)

Tactic:
ext : 2