awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
simp_rw :
  Eq (α := ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₁ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q' : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
⊢ Eq (α := ↥(even Q'))
    ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
have simp_rw₂ : Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((-Q : (a : M) → R) m) : ↥(even Q'))
  ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
simp_rw :
  Eq (α := ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₁ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q' : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₂ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((-Q : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
⊢ Eq (α := ↥(even Q'))
    ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
have simp_rw₃ : Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) (-(Q : (a : M) → R) m) : ↥(even Q'))
  ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
simp_rw :
  Eq (α := ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₁ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q' : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₂ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((-Q : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
simp_rw₃ :
  Eq (α := ↥(even Q')) (-(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) (-(Q : (a : M) → R) m) : ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
⊢ Eq (α := ↥(even Q'))
    ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m :
      ↥(even Q'))
    ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
have simp_rw₄ : Eq (α := ↥(even Q')) (- -(algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
  ((algebraMap R ↥(even Q') : (a : R) → ↥(even Q')) ((Q : (a : M) → R) m) : ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
⊢ HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
have simp_rw : HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
      ↥(even Q'))
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q')) =
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h,
          QuadraticMap.neg_apply, smul_neg, neg_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
simp_rw :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
⊢ HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
have simp_rw₁ : HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
    (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
      ↥(even Q'))
    (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q')) =
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h,
          QuadraticMap.neg_apply, smul_neg, neg_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
simp_rw :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₁ :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
⊢ HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
have simp_rw₂ : HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q' : (a : M) → R) m₂ : R)
    (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q')) =
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h,
          QuadraticMap.neg_apply, smul_neg, neg_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
simp_rw :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₁ :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₂ :
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q' : (a : M) → R) m₂ : R)
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
⊢ HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
have simp_rw₃ : HSMul.hSMul (α := R) (β := ↥(even Q')) ((-Q : (a : M) → R) m₂ : R)
    (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q')) =
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h,
          QuadraticMap.neg_apply, smul_neg, neg_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
⊢ (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R ↥(even Q)
have h₁ : ∀ (m₁ m₂ : M),
  Eq (α := ↥(even Q))
    ((((((even.ι Q).compr₂ ((evenToNeg Q' Q h').comp (evenToNeg Q Q' h))).bilin : (a : M) → M →ₗ[R] ↥(even Q)) m₁ :
            M →ₗ[R] ↥(even Q)) :
          (a : M) → ↥(even Q))
        m₂ :
      ↥(even Q))
    ((((((even.ι Q).compr₂ (AlgHom.id R ↥(even Q))).bilin : (a : M) → M →ₗ[R] ↥(even Q)) m₁ : M →ₗ[R] ↥(even Q)) :
          (a : M) → ↥(even Q))
        m₂ :
      ↥(even Q))
Tactic: ext m₁ m₂ : 4
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
have nil : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    (List.prod []) =
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
Tactic: rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
nil :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod []) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
have nil₁ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N) 1 =
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
Tactic: rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
nil :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod []) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
nil₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
have nil₂ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N) 1 =
  n
Tactic: rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
nil :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod []) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
nil₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
nil₂ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    n
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n []
have nil₃ : n = n
Tactic: rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
hd : M
tl : List M
ih :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (hd :: tl))) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
have cons : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    (List.prod ((ι Q : (a : M) → CliffordAlgebra Q) hd :: List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) :
      CliffordAlgebra Q) =
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
Tactic: rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
hd : M
tl : List M
ih :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl
cons :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod ((ι Q : (a : M) → CliffordAlgebra Q) hd :: List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) :
        CliffordAlgebra Q) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (hd :: tl))) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
have cons₁ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) hd : CliffordAlgebra Q)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) : CliffordAlgebra Q)) =
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
Tactic: rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]