awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m₁ m₂ : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (m₁ + m₂) f i =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₁ f)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₂ f)
      i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.add_apply, map_add, Pi.add_apply, AlternatingMap.curryLeft_smul, AlternatingMap.curryLeft_add, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_1 :
  ∀ (i : ℕ),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (c • m) f i =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
        i
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (c • m) f =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)

Tactic:
ext i : 1
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (c • m) f i =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
      i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.add_apply, map_add, Pi.add_apply, AlternatingMap.curryLeft_smul, AlternatingMap.curryLeft_add, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m : M
f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_1 :
  ∀ (i : ℕ),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m (f₁ + f₂) i =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₁)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₂)
        i
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (f₁ + f₂) =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₁)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₂)

Tactic:
ext i : 1
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m : M
f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (f₁ + f₂) i =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₁)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₂)
      i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.add_apply, map_add, Pi.add_apply, AlternatingMap.curryLeft_smul, AlternatingMap.curryLeft_add, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_1 :
  ∀ (i : ℕ),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m (c • f) i =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
        i
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (c • f) =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)

Tactic:
ext i : 1
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
i : ℕ
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (c • f) i =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
      i

Tactic:
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.add_apply, map_add, Pi.add_apply, AlternatingMap.curryLeft_smul, AlternatingMap.curryLeft_add, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m : M
x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_2 :
  ∀ (x_1 : ℕ) (x_2 : Fin x_1 → M),
    Eq.{u_3 + 1} (α := N)
      ((((((LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯ :
                        (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                      m :
                    ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                  (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                ((((LinearMap.mk₂ R
                              (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                                (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                              ⋯ ⋯ ⋯ ⋯ :
                            (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                          m :
                        ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    x :
                  (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                x_1 :
              M [⋀^Fin x_1]→ₗ[R] N) :
            (a : Fin x_1 → M) → N)
          x_2 :
        N)
      ((HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x x_1 : (a : Fin x_1 → M) → N) x_2 : N)
⊢ (((LinearMap.mk₂ R
                (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                  (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                ⋯ ⋯ ⋯ ⋯ :
              (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            m :
          ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
        (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((((LinearMap.mk₂ R
                    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                      (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                    ⋯ ⋯ ⋯ ⋯ :
                  (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                m :
              ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
            (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
          x :
        (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) =
    HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m : M
x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
x_1 : ℕ
x_2 : Fin x_1 → M
⊢ Eq.{u_3 + 1} (α := N)
    ((((((LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯ :
                      (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    m :
                  ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              ((((LinearMap.mk₂ R
                            (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                              (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                            ⋯ ⋯ ⋯ ⋯ :
                          (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                        m :
                      ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  x :
                (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x_1 :
            M [⋀^Fin x_1]→ₗ[R] N) :
          (a : Fin x_1 → M) → N)
        x_2 :
      N)
    ((HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x x_1 : (a : Fin x_1 → M) → N) x_2 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
dsimp :
  Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    f :
                  ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) :
      N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)

Tactic:
dsimp [liftAlternating]

Premises used: ExteriorAlgebra.liftAlternating
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
rw :
  Eq.{u_3 + 1} (α := N) ((f (HAdd.hAdd (α := ℕ) 0 1) : (a : Fin (Nat.succ 0) → M) → N) (Matrix.vecCons m 0) : N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    f :
                  ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)

Tactic:
rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]

Premises used: LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply, CliffordAlgebra.foldl_ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ Eq.{u_3 + 1} (α := N) ((f (HAdd.hAdd (α := ℕ) 0 1) : (a : Fin (Nat.succ 0) → M) → N) (Matrix.vecCons m 0) : N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)

Tactic:
congr!
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
dsimp :
  Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    f :
                  ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) x)
              0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  fun (i : ℕ) ↦ (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) x) :
      N)
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) fun (i : ℕ) ↦
            (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
          (a : ExteriorAlgebra R M) → N)
        x :
      N)

Tactic:
dsimp [liftAlternating]

Premises used: ExteriorAlgebra.liftAlternating
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → CliffordAlgebra 0 →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    ((((LinearMap.mk₂ R
                                (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                                  (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                                ⋯ ⋯ ⋯ ⋯ :
                              (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                            m :
                          ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                        (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                      f) :
                  CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0 →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : CliffordAlgebra 0) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  fun (i : ℕ) ↦ (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
dsimp :
  Eq.{u_3 + 1} (α := N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  f :
                ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
              (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            1 0 :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) 0 : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        1 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) 0 : N)

Tactic:
dsimp [liftAlternating]

Premises used: ExteriorAlgebra.liftAlternating
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
rw rw₁ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) 0 : N) ((f 0 : (a : Fin 0 → M) → N) 0 : N)
⊢ Eq.{u_3 + 1} (α := N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  f :
                ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
              (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            1 0 :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) 0 : N)

Tactic:
rw [foldl_one]

Premises used: CliffordAlgebra.foldl_one