awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
x y : CliffordAlgebra Q
hx :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q)))
hy :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) y) : CliffordAlgebra (Q' Q)))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) (x + y)) : CliffordAlgebra (Q' Q)))

Tactic:
simp only [map_add, Subalgebra.coe_add, hx, hy]

Premises used: map_add, Subalgebra.coe_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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'))
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'))

Tactic:
simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg]

Premises used: QuadraticMap.neg_apply, LinearMap.neg_apply, CliffordAlgebra.EvenHom.contract, neg_neg, map_neg
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
⊢ Eq (α := ↥(even Q'))
    ((evenToNeg Q Q' h : (a : ↥(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'))

Tactic:
even.lift_ι _ _ m₁ m₂

Premises used: Set.Mem, CliffordAlgebra.even.lift_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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'
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))
⊢ (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R ↥(even Q)

Tactic:
ext m₁ m₂ : 4
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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'
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:
simp [evenToNeg_ι]

Premises used: CliffordAlgebra.evenToNeg_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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)
    ((((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:
LinearMap.congr_fun (lift_ι_apply _ _ _) n

Premises used: CliffordAlgebra.lift_ι_apply, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
⊢ (((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:
LinearMap.congr_fun (AlgHom.commutes _ r) n

Premises used: LinearMap.congr_fun, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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)
      1 =
    n

Tactic:
LinearMap.congr_fun (map_one (lift Q _)) n

Premises used: LinearMap.congr_fun, map_one, CliffordAlgebra.lift, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (a * b) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                b) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        a :
      N)

Tactic:
LinearMap.congr_fun (map_mul (lift Q _) _ _) n

Premises used: map_mul, LinearMap.congr_fun, CliffordAlgebra.lift, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
nil₃ nil₄ : 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 []

Tactic:
rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]

Premises used: List.foldr_nil, CliffordAlgebra.foldr_one, List.prod_nil, List.map_nil
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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 []
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)
⊢ (((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

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]

Premises used: CliffordAlgebra.foldr_mul, List.foldr_cons, List.map_cons, List.foldr_nil, CliffordAlgebra.foldr_ι, CliffordAlgebra.foldr_one, List.prod_nil, List.prod_cons, List.map_nil
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
x : 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)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        x :
      N)

Tactic:
DFunLike.congr_arg (foldr Q f hf n) <| reverse_reverse _

Premises used: CliffordAlgebra.reverse_reverse, DFunLike.coe, CliffordAlgebra.foldr, DFunLike.congr_arg
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
x : CliffordAlgebra Q
⊢ 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) x : CliffordAlgebra Q) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        x :
      N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [← foldr_reverse, reverse_ι, foldr_ι]

Premises used: CliffordAlgebra.foldr_ι, CliffordAlgebra.foldr_reverse, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
rw₂ rw₃ : r • n = 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

Tactic:
rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]

Premises used: CliffordAlgebra.reverse.commutes, CliffordAlgebra.foldr_reverse, CliffordAlgebra.foldr_algebraMap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
rw₂ rw₃ : n = n
⊢ (((foldl 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]

Premises used: CliffordAlgebra.foldr_one, CliffordAlgebra.foldr_reverse, CliffordAlgebra.reverse.map_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
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)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₂ :
  (((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.reverse)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₃ :
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n l.reverse =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₄ rw₅ :
  List.foldl (fun (x : N) (y : M) ↦ (((f : (a : M) → N →ₗ[R] N) y : N →ₗ[R] N) : (a : N) → N) x) n l =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
⊢ (((foldl 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.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l

Tactic:
rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]

Premises used: List.foldr_reverse, CliffordAlgebra.foldr_prod_map_ι, CliffordAlgebra.reverse_prod_map_ι, CliffordAlgebra.foldr_reverse, List.map_reverse
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x : CliffordAlgebra Q
have : ∀ (this : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) ⊤ x), P x
⊢ P x

Tactic:
have : x ∈ ⊤ := Submodule.mem_top (R := R)
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x : CliffordAlgebra Q
this : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) ⊤ x
⊢ Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) x

Tactic:
rw [← iSup_ι_range_eq_top] at this

Premises used: CliffordAlgebra.iSup_ι_range_eq_top