awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
H :
  ∀ (m : (i : Fin n.succ) → M i),
    Eq.{v₂ + 1} (α := M₂) ((f.curryLeft (M := M).uncurryLeft (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
⊢ f.curryLeft (M := M).uncurryLeft (M := M) = f

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ Eq.{v₂ + 1} (α := M₂) ((f.curryLeft (M := M).uncurryLeft (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n.succ) → M i
x y : M (last n)
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
              (a : M (last n)) → M₂)
            (m (last n)) :
          M₂))
      (update (β := M) m (last n) (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m (last n) x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m (last n) y))

Tactic:
simp [Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n.succ) → M i
i : Fin n
x y : M i.castSucc
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
              (a : M (last n)) → M₂)
            (m (last n)) :
          M₂))
      (update (β := M) m i.castSucc (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m i.castSucc x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m i.castSucc y))

Tactic:
simp [Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂)
m : (i : Fin n.succ) → M i
i : Fin n.succ
c : R
x : M i
last :
  ∀ (x : M (Fin.last n)),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
                (a : M (Fin.last n)) → M₂)
              (m (Fin.last n)) :
            M₂))
        (update (β := M) m (Fin.last n) (c • x)) =
      HSMul.hSMul (β := M₂) c
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                    LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
                  (a : M (Fin.last n)) → M₂)
                (m (Fin.last n)) :
              M₂))
          (update (β := M) m (Fin.last n) x))
cast :
  ∀ (i : Fin n) (x : M i.castSucc),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
                (a : M (Fin.last n)) → M₂)
              (m (Fin.last n)) :
            M₂))
        (update (β := M) m i.castSucc (c • x)) =
      HSMul.hSMul (β := M₂) c
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                    LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
                  (a : M (Fin.last n)) → M₂)
                (m (Fin.last n)) :
              M₂))
          (update (β := M) m i.castSucc x))
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
              (a : M (Fin.last n)) → M₂)
            (m (Fin.last n)) :
          M₂))
      (update (β := M) m i (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (Fin.last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (Fin.last n)) M₂) :
                (a : M (Fin.last n)) → M₂)
              (m (Fin.last n)) :
            M₂))
        (update (β := M) m i x))

Tactic:
cases i using Fin.lastCases
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n.succ) → M i
c : R
x : M (last n)
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
              (a : M (last n)) → M₂)
            (m (last n)) :
          M₂))
      (update (β := M) m (last n) (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m (last n) x))

Tactic:
simp [Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n.succ) → M i
c : R
i : Fin n
x : M i.castSucc
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
              (a : M (last n)) → M₂)
            (m (last n)) :
          M₂))
      (update (β := M) m i.castSucc (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
                  LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
                (a : M (last n)) → M₂)
              (m (last n)) :
            M₂))
        (update (β := M) m i.castSucc x))

Tactic:
simp [Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n.succ) → M i
⊢ Eq.{v₂ + 1} (α := M₂) ((f.uncurryRight (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) m) :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        (m (last n)) :
      M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)

Tactic:
simp_rw [f.snoc_add]

Premises used: MultilinearMap.snoc_add
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (c • x)) =
    HSMul.hSMul (α := R) (β := M₂) ((RingHom.id R : (a : R) → R) c : R)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)

Tactic:
simp only [f.snoc_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, MultilinearMap.snoc_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f.curryRight (M := M) : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
H :
  ∀ (m : (i : Fin n) → M i.castSucc) (x : M (last n)),
    Eq.{v₂ + 1} (α := M₂)
      ((((f.uncurryRight (M := M).curryRight (M := M) : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
              LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
            (a : M (last n)) → M₂)
          x :
        M₂)
      ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
              LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
            (a : M (last n)) → M₂)
          x :
        M₂)
⊢ f.uncurryRight (M := M).curryRight (M := M) = f

Tactic:
ext m x
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
H :
  Eq.{v₂ + 1} (α := M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) (snoc (α := M) m x)) :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f.uncurryRight (M := M).curryRight (M := M) : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)

Tactic:
simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]

Premises used: MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply, Fin.snoc_last
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R (fun (i : Fin n) ↦ M i.castSucc) (LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
H H₁ :
  Eq.{v₂ + 1} (α := M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) (init (α := M) (snoc (α := M) m x)) :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)
    ((((f : (a : (i : Fin n) → M i.castSucc) → M (last n) →ₗ[R] M₂) m :
            LinearMap.{uR, uR, v, v₂} (RingHom.id R) (M (last n)) M₂) :
          (a : M (last n)) → M₂)
        x :
      M₂)

Tactic:
rw [init_snoc]

Premises used: Fin.init_snoc
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
H :
  ∀ (m : (i : Fin n.succ) → M i),
    Eq.{v₂ + 1} (α := M₂) ((f.curryRight (M := M).uncurryRight (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
⊢ f.curryRight (M := M).uncurryRight (M := M) = f

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ Eq.{v₂ + 1} (α := M₂) ((f.curryRight (M := M).uncurryRight (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
x y : M p
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
              (a : (i : Fin n) → M (p.succAbove i)) → M₂)
            (p.removeNth (α := M) m) :
          M₂))
      (update (β := M) m p (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m p x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m p y))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
j : Fin n
x y : M (p.succAbove j)
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
              (a : (i : Fin n) → M (p.succAbove i)) → M₂)
            (p.removeNth (α := M) m) :
          M₂))
      (update (β := M) m (p.succAbove j) (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m (p.succAbove j) x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m (p.succAbove j) y))

Tactic:
simp