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
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
x : CliffordAlgebra Q
algebraMap₁ :
  ∀ (r : R),
    P
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))
⊢ P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
have add₁ : ∀ (x y : CliffordAlgebra Q) (hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))
  (hy : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y)),
  P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y))
Tactic: induction x using CliffordAlgebra.right_induction with
  | algebraMap r => simpa only [reverse.commutes] using algebraMap r
  | add _ _ hx hy => simpa only [map_add] using add _ _ hx hy
  | mul_ι _ _ hx => simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
x : CliffordAlgebra Q
algebraMap₁ :
  ∀ (r : R),
    P
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))
add₁ :
  ∀ (x y : CliffordAlgebra Q) (hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))
    (hy : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y)),
    P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y))
⊢ P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
have mul_ι : ∀ (m : M) (x : CliffordAlgebra Q) (hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)),
  P
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)))
Tactic: induction x using CliffordAlgebra.right_induction with
  | algebraMap r => simpa only [reverse.commutes] using algebraMap r
  | add _ _ hx hy => simpa only [map_add] using add _ _ hx hy
  | mul_ι _ _ hx => simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx
Cleared hypotheses: x
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
have have : (v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)) → M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
Tactic: have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
have have : (l : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q) → M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
Tactic: have l := v_mul.compl₂ (LinearMap.fst _ _ N)
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
v : M
x_fx : CliffordAlgebra Q × N
⊢ (((foldr'Aux Q f : (a : M) → Module.End R (CliffordAlgebra Q × N)) v : Module.End R (CliffordAlgebra Q × N)) :
        (a : CliffordAlgebra Q × N) → CliffordAlgebra Q × N)
      ((((foldr'Aux Q f : (a : M) → Module.End R (CliffordAlgebra Q × N)) v : Module.End R (CliffordAlgebra Q × N)) :
          (a : CliffordAlgebra Q × N) → CliffordAlgebra Q × N)
        x_fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
have simp : (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
        (a : CliffordAlgebra Q × N) → N)
      ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
          (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
              (a : CliffordAlgebra Q × N) → N)
            x_fx) :
        CliffordAlgebra Q × N)) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
Tactic: simp only [foldr'Aux_apply_apply]
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
v : M
x_fx : CliffordAlgebra Q × N
⊢ (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1),
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
have rw : (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
      x_fx.1,
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
        (a : CliffordAlgebra Q × N) → N)
      ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
          (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
              (a : CliffordAlgebra Q × N) → N)
            x_fx) :
        CliffordAlgebra Q × N)) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
Tactic: rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
v : M
x_fx : CliffordAlgebra Q × N
rw :
  (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
        x_fx.1,
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
⊢ (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1),
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
have rw₁ : (HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) v) : CliffordAlgebra Q)
      x_fx.1,
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
        (a : CliffordAlgebra Q × N) → N)
      ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
          (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
              (a : CliffordAlgebra Q × N) → N)
            x_fx) :
        CliffordAlgebra Q × N)) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
Tactic: rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
⊢ Eq.{u_3 + 1} (α := N)
    ((foldr' Q f hf n : (a : CliffordAlgebra Q) → N)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
      N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((x, (foldr' Q f hf n : (a : CliffordAlgebra Q) → N) x) : CliffordAlgebra Q × N) :
      N)
have dsimp : Eq.{u_3 + 1} (α := N)
  ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)).2 :
    N)
  ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) : (a : CliffordAlgebra Q × N) → N)
      (x,
        (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                      CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                    (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                  (1, n) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
            x).2) :
    N)
Tactic: dsimp [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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)).2 :
      N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        (x,
          (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                        CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                      (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                    (1, n) :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
              x).2) :
      N)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine : Eq (α := CliffordAlgebra Q × N)
  ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        x).1,
    (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        x).2)
  (x,
    (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        x).2)
Tactic: refine congr_arg (f m) (Prod.mk.eta.symm.trans ?_)
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra Q × N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).1,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)
    (x,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)
have e_fst : (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
            (1, n) :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
      x).1 =
  x
Tactic: congr 1
-- 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 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)).1 :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have e_fst : (HSMul.hSMul (β := CliffordAlgebra Q × N) r (1, n)).1 =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r
Tactic: simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]