awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ (((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₂ : Eq.{u_3 + 1} (α := N)
  ((((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)) :
    N)
  ((((f : (a : M) → N →ₗ[R] N) hd : N →ₗ[R] N) : (a : N) → N)
      (List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl) :
    N)
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
l : List 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 (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n l
have nil : (((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 []
Tactic: induction l with
  | nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
  | cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]
Cleared hypotheses: l
-- 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
l : List 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.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 []
⊢ (((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) l)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n l
have cons : ∀ (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)
Tactic: induction l with
  | nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
  | cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]
Cleared hypotheses: l
-- 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
m : M
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
have rw : Eq.{u_3 + 1} (α := N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
        CliffordAlgebra Q) :
    N)
  ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
Tactic: rw [← foldr_reverse, reverse_ι, foldr_ι]
-- 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
m : M
rw :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
          CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
have rw₁ : Eq.{u_3 + 1} (α := N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :
    N)
  ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
Tactic: rw [← foldr_reverse, reverse_ι, foldr_ι]
-- 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
m : M
rw :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
          CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
have rw₂ : Eq (α := N) ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
  ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n : N)
Tactic: rw [← foldr_reverse, reverse_ι, foldr_ι]
-- 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
r : R
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    r • n
have rw : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q) =
  r • n
Tactic: rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]
-- 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
r : R
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q) =
    r • n
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    r • n
have rw₁ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
  r • n
Tactic: rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]
-- 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
r : R
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q) =
    r • n
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    r • n
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    r • n
have rw₂ : r • n = r • n
Tactic: rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]
-- 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
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    n
have rw : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 1) =
  n
Tactic: rw [← foldr_reverse, reverse.map_one, 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
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 1) =
    n
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    n
have rw₁ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N) 1 =
  n
Tactic: rw [← foldr_reverse, reverse.map_one, 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
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 1) =
    n
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    n
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      1 =
    n
have rw₂ : n = n
Tactic: rw [← foldr_reverse, reverse.map_one, 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
a b : CliffordAlgebra Q
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (a * b) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
have rw : Eq.{u_3 + 1} (α := N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
    N)
  ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
            ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                (a : CliffordAlgebra Q) → N)
              a) :
          CliffordAlgebra Q →ₗ[R] N) :
        (a : CliffordAlgebra Q) → N)
      b :
    N)
Tactic: rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]
-- 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
a b : CliffordAlgebra Q
rw :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (a * b) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
have rw₁ : Eq.{u_3 + 1} (α := N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
    N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
            ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                (a : CliffordAlgebra Q) → N)
              a) :
          CliffordAlgebra Q →ₗ[R] N) :
        (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
    N)
Tactic: rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]