awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : Fin n.succ
x : R
y : 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)) =
      HSMul.hSMul (β := M₂) 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))
p₁ :
  ∀ (j : Fin n) (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)) =
      HSMul.hSMul (β := M₂) 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))
⊢ (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 i (x • y)) =
    HSMul.hSMul (β := M₂) 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 i y))

Tactic:
cases i using Fin.succAboveCases p
-- 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 : R
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)) =
    HSMul.hSMul (β := M₂) 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
x : R
j : Fin n
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)) =
    HSMul.hSMul (β := M₂) 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
-- 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 : MultilinearMap R M M₂
x y : M p
H :
  ∀ (x_1 : (i : Fin n) → M (p.succAbove i)),
    Eq.{v₂ + 1} (α := M₂)
      ((mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
              (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (x + y) m))
              ⋯ ⋯ :
            (a : (i : Fin n) → M (p.succAbove i)) → M₂)
          x_1 :
        M₂)
      ((HAdd.hAdd (α := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
              (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
                (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                  (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
                ⋯ ⋯)
              (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
                (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                  (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) y m))
                ⋯ ⋯) :
            (a : (i : Fin n) → M (p.succAbove i)) → M₂)
          x_1 :
        M₂)
⊢ mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
      (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
        (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (x + y) m))
      ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
      (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
        (fun (m : (i : Fin n) → M (p.succAbove i)) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
        ⋯ ⋯)
      (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
        (fun (m : (i : Fin n) → M (p.succAbove i)) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) y m))
        ⋯ ⋯)

Tactic:
ext
-- 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 : MultilinearMap R M M₂
x y : M p
x_1 : (i : Fin n) → M (p.succAbove i)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
            (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
              (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (x + y) m))
            ⋯ ⋯ :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)
    ((HAdd.hAdd (α := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
            (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
              (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
              ⋯ ⋯)
            (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
              (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) y m))
              ⋯ ⋯) :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)

Tactic:
simp [map_insertNth_add]

Premises used: MultilinearMap.map_insertNth_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₂
p : Fin (n + 1)
f : MultilinearMap R M M₂
c : R
x : M p
H :
  ∀ (x_1 : (i : Fin n) → M (p.succAbove i)),
    Eq.{v₂ + 1} (α := M₂)
      ((mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
              (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (c • x) m))
              ⋯ ⋯ :
            (a : (i : Fin n) → M (p.succAbove i)) → M₂)
          x_1 :
        M₂)
      ((HSMul.hSMul (α := R) (β := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
              ((RingHom.id R : (a : R) → R) c : R)
              (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
                (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                  (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
                ⋯ ⋯) :
            (a : (i : Fin n) → M (p.succAbove i)) → M₂)
          x_1 :
        M₂)
⊢ mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
      (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
        (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (c • x) m))
      ⋯ ⋯ =
    HSMul.hSMul (α := R) (β := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
      ((RingHom.id R : (a : R) → R) c : R)
      (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
        (fun (m : (i : Fin n) → M (p.succAbove i)) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
        ⋯ ⋯)

Tactic:
ext
-- 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 : MultilinearMap R M M₂
c : R
x : M p
x_1 : (i : Fin n) → M (p.succAbove i)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
            (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
              (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (c • x) m))
            ⋯ ⋯ :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)
    ((HSMul.hSMul (α := R) (β := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂)
            ((RingHom.id R : (a : R) → R) c : R)
            (mk' (M₁ := fun (i : Fin n) ↦ M (p.succAbove i))
              (fun (m : (i : Fin n) → M (p.succAbove i)) ↦
                (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m))
              ⋯ ⋯) :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)

Tactic:
simp [map_insertNth_smul]

Premises used: MultilinearMap.map_insertNth_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₂
i : Fin (n + 1)
f : M i →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (j : Fin n) ↦ M (i.succAbove j)) M₂
h :
  ∀ (x : M i) (x_1 : (i_1 : Fin n) → M (i.succAbove i_1)),
    Eq.{v₂ + 1} (α := M₂)
      ((((curryMid (M := M) i (uncurryMid (M := M) i f) :
                  (a : M i) → MultilinearMap R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂)
                x :
              MultilinearMap.{uR, 0, v, v₂} R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) :
            (a : (i_1 : Fin n) → M (i.succAbove i_1)) → M₂)
          x_1 :
        M₂)
      ((((f : (a : M i) → MultilinearMap R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) x :
              MultilinearMap.{uR, 0, v, v₂} R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) :
            (a : (i_1 : Fin n) → M (i.succAbove i_1)) → M₂)
          x_1 :
        M₂)
⊢ curryMid (M := M) i (uncurryMid (M := M) i f) = f

Tactic:
ext
-- 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₂
i : Fin (n + 1)
f : M i →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (j : Fin n) ↦ M (i.succAbove j)) M₂
x : M i
x_1 : (i_1 : Fin n) → M (i.succAbove i_1)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((curryMid (M := M) i (uncurryMid (M := M) i f) :
                (a : M i) → MultilinearMap R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂)
              x :
            MultilinearMap.{uR, 0, v, v₂} R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) :
          (a : (i_1 : Fin n) → M (i.succAbove i_1)) → M₂)
        x_1 :
      M₂)
    ((((f : (a : M i) → MultilinearMap R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) x :
            MultilinearMap.{uR, 0, v, v₂} R (fun (i_1 : Fin n) ↦ M (i.succAbove i_1)) M₂) :
          (a : (i_1 : Fin n) → M (i.succAbove i_1)) → M₂)
        x_1 :
      M₂)

Tactic:
simp
-- 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₂
i : Fin (n + 1)
f : MultilinearMap R M M₂
H :
  ∀ (x : (i : Fin n.succ) → M i),
    Eq.{v₂ + 1} (α := M₂)
      ((LinearMap.uncurryMid (M := M) i (curryMid (M := M) i f) : (a : (i : Fin n.succ) → M i) → M₂) x : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) x : M₂)
⊢ LinearMap.uncurryMid (M := M) i (curryMid (M := M) i f) = f

Tactic:
ext
-- 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₂
i : Fin (n + 1)
f : MultilinearMap R M M₂
x : (i : Fin n.succ) → M i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((LinearMap.uncurryMid (M := M) i (curryMid (M := M) i f) : (a : (i : Fin n.succ) → M i) → M₂) x : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) x : 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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [inst_9 : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (x y : N (Sum.inr i)),
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u (update (β := fun (i : ι') ↦ N (Sum.inr i)) m i (x + y)) t) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
            Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u (update (β := fun (i : ι') ↦ N (Sum.inr i)) m i x) t :
          M₂)
        ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
            Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u (update (β := fun (i : ι') ↦ N (Sum.inr i)) m i y) t :
          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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [inst_9 : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (c : R) (x : N (Sum.inr i)),
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u (update (β := fun (i : ι') ↦ N (Sum.inr i)) m i (c • x)) t) =
      HSMul.hSMul (β := M₂) c
        ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
            Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u (update (β := fun (i : ι') ↦ N (Sum.inr i)) m i x) t :
          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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
inst_9 : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
x y : N (Sum.inl i)
x_1 : (i : ι') → N (Sum.inr i)
this : DecidableEq ι' := Classical.decEq ι'
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (i : ι') ↦ N (Sum.inr i))
            (fun (v : (i : ι') → N (Sum.inr i)) ↦
              (f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
                Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (update (β := fun (i : ι) ↦ N (Sum.inl i)) u i (x + y)) v t)
            ⋯ ⋯ :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        x_1 :
      M₂)
    ((HAdd.hAdd (α := MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
            (mk (M₁ := fun (i : ι') ↦ N (Sum.inr i))
              (fun (v : (i : ι') → N (Sum.inr i)) ↦
                (f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
                  Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (update (β := fun (i : ι) ↦ N (Sum.inl i)) u i x) v t)
              ⋯ ⋯)
            (mk (M₁ := fun (i : ι') ↦ N (Sum.inr i))
              (fun (v : (i : ι') → N (Sum.inr i)) ↦
                (f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
                  Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (update (β := fun (i : ι) ↦ N (Sum.inl i)) u i y) v t)
              ⋯ ⋯) :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        x_1 :
      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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
inst_9 : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
c : R
x : N (Sum.inl i)
x_1 : (i : ι') → N (Sum.inr i)
this : DecidableEq ι' := Classical.decEq ι'
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (i : ι') ↦ N (Sum.inr i))
            (fun (v : (i : ι') → N (Sum.inr i)) ↦
              (f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
                Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (update (β := fun (i : ι) ↦ N (Sum.inl i)) u i (c • x)) v t)
            ⋯ ⋯ :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        x_1 :
      M₂)
    ((HSMul.hSMul (β := MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂) c
            (mk (M₁ := fun (i : ι') ↦ N (Sum.inr i))
              (fun (v : (i : ι') → N (Sum.inr i)) ↦
                (f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
                  Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (update (β := fun (i : ι) ↦ N (Sum.inl i)) u i x) v t)
              ⋯ ⋯) :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        x_1 :
      M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
N : ι ⊕ ι' → Type u_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
v : (i : ι') → N (Sum.inr i)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f.currySum (N := N) : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) u :
            MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂) :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        v :
      M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦ Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) u v t : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : MultilinearMap R (fun (x : ι ⊕ ι') ↦ N) M₂
u : ι → N
v : ι' → N
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f.currySum (N := fun (x : ι ⊕ ι') ↦ N) : (a : (i : ι) → N) → MultilinearMap R (fun (i : ι') ↦ N) M₂) u :
            MultilinearMap.{uR, uι', u_2, v₂} R (fun (i : ι') ↦ N) M₂) :
          (a : (i : ι') → N) → M₂)
        v :
      M₂)
    ((f : (a : (i : ι ⊕ ι') → N) → M₂) (Sum.elim u v) : M₂)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
N : ι ⊕ ι' → Type u_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f₁ f₂ : MultilinearMap R N M₂
⊢ (f₁ + f₂).currySum (N := N) = f₁.currySum (N := N) + f₂.currySum (N := N)

Tactic:
rfl

Premises used: MultilinearMap.currySum, rfl