awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₆ :
  (r₁ * r₂) •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
        ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₇ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) ((0 : (a : R) → R) 1)) =
    0
rw₈ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) 0) =
    0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₉ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂) 0 = 0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₆ :
  (r₁ * r₂) •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
        ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₇ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) ((0 : (a : R) → R) 1)) =
    0
rw₈ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) 0) =
    0
rw₉ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂) 0 = 0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
have rw₁₀ : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := R) 0) 0 0
Tactic: rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]
-- 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
x x_1 x_2 : M
⊢ (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 + x_1) x_2 =
    HAdd.hAdd (α := ↥(even 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 x_2)
      ((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)
have simp : 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) +
      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))
    sorry =
  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))
      sorry +
    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))
      sorry
Tactic: simp only [map_add, add_mul]
-- 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
x : R
x_1 x_2 : M
⊢ (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 • x_1) 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)
have 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))
    sorry =
  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))
      sorry
Tactic: simp only [map_smul, smul_mul_assoc]
-- 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
x x_1 x_2 : M
⊢ (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 (x_1 + x_2) =
    HAdd.hAdd (α := ↥(even 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 x_1)
      ((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 x_2)
have simp : 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))
    sorry =
  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))
      sorry +
    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))
      sorry
Tactic: simp only [map_add, mul_add]
-- 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
x : R
x_1 x_2 : M
⊢ (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)
have 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))
    sorry =
  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))
      sorry
Tactic: simp only [map_smul, mul_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
m₁ m₂ m₃ : M
⊢ 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)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m₂ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
have rw : 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)) =
  HMul.hMul (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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))
Tactic: rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_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
m₁ m₂ m₃ : M
rw :
  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)) =
    HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m₂ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
have rw₁ : HMul.hMul (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q)) =
  HMul.hMul (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) 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))
Tactic: rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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
⊢ f = g
have h₁ : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
Tactic: rw [EvenHom.ext_iff] at h
Cleared hypotheses: h
-- 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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g
have 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)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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)
    ((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)
have 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)))
Tactic: have := congr_arg₂ (· + ·) ihx ihy
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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)
    ((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)
have 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)))
Tactic: have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih