awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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
⊢ 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)
have 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
Tactic: rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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
⊢ 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)
have 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
Tactic: rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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
⊢ 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)
have 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
Tactic: rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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 y : M →ₗ[R] A
_hx :
  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)})
    x
_hy :
  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)})
    y
ihx :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
ihy :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (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 + y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
have snd : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
    (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
Tactic: rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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 y : M →ₗ[R] A
_hx :
  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)})
    x
_hy :
  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)})
    y
ihx :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
ihy :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (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)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (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 + y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
have snd₁ : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
    (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
    (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m₁ : A) ((y : (a : M) → A) m₁ : A))
Tactic: rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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 y : M →ₗ[R] A
_hx :
  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)})
    x
_hy :
  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)})
    y
ihx :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
ihy :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (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)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (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)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m : A) ((y : (a : M) → A) m : A)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
      (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m₁ : A) ((y : (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 + y : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
have snd₂ : HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (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)
      ((y : (a : M) → A) m : A) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
    (HAdd.hAdd (α := A) (β := A) ((x : (a : M) → A) m₁ : A) ((y : (a : M) → A) m₁ : A))
Tactic: rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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)
⊢ 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)
have 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)
Tactic: rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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)
⊢ 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)
have 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))
Tactic: rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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))
⊢ 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)
have 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))
Tactic: rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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))
⊢ 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)
have 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))
Tactic: rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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))
⊢ 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)
have 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))
Tactic: rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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
⊢ ↥(even Q) →ₗ[R] A
have refine : CliffordAlgebra Q →ₗ[R] A
Tactic: refine ?_ ∘ₗ (even Q).val.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
x y : ↥(even Q)
⊢ (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)
have 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)
Tactic: obtain ⟨x, x_property⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (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
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
⊢ (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)
have 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)
Tactic: cases y
Cleared hypotheses: y