awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
r : R
f : MultilinearMap R N M₂
⊢ (r • f).currySum (N := N) = r • f.currySum (N := N)

Tactic:
rfl

Premises used: MultilinearMap.currySum, 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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst_9 : DecidableEq (ι ⊕ ι')
m : (i : ι ⊕ ι') → N i
val : ι
x y : N (Sum.inl val)
⊢ (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
          update (β := N) m (Sum.inl val) (x + y) (Sum.inl i) :
        (a : (i : ι') → N (Sum.inr i)) → M₂)
      fun (i' : ι') ↦ update (β := N) m (Sum.inl val) (x + y) (Sum.inr i')) =
    HAdd.hAdd (α := M₂) (β := M₂)
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inl val) x (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inl val) x (Sum.inr i') :
        M₂)
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inl val) y (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inl val) y (Sum.inr i') :
        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)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst_9 : DecidableEq (ι ⊕ ι')
m : (i : ι ⊕ ι') → N i
val : ι'
x y : N (Sum.inr val)
⊢ (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
          update (β := N) m (Sum.inr val) (x + y) (Sum.inl i) :
        (a : (i : ι') → N (Sum.inr i)) → M₂)
      fun (i' : ι') ↦ update (β := N) m (Sum.inr val) (x + y) (Sum.inr i')) =
    HAdd.hAdd (α := M₂) (β := M₂)
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inr val) x (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inr val) x (Sum.inr i') :
        M₂)
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inr val) y (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inr val) y (Sum.inr i') :
        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)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst_9 : DecidableEq (ι ⊕ ι')
m : (i : ι ⊕ ι') → N i
val : ι
c : R
x : N (Sum.inl val)
⊢ (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
          update (β := N) m (Sum.inl val) (c • x) (Sum.inl i) :
        (a : (i : ι') → N (Sum.inr i)) → M₂)
      fun (i' : ι') ↦ update (β := N) m (Sum.inl val) (c • x) (Sum.inr i')) =
    HSMul.hSMul (β := M₂) c
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inl val) x (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inl val) x (Sum.inr i') :
        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)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst_9 : DecidableEq (ι ⊕ ι')
m : (i : ι ⊕ ι') → N i
val : ι'
c : R
x : N (Sum.inr val)
⊢ (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
          update (β := N) m (Sum.inr val) (c • x) (Sum.inl i) :
        (a : (i : ι') → N (Sum.inr i)) → M₂)
      fun (i' : ι') ↦ update (β := N) m (Sum.inr val) (c • x) (Sum.inr i')) =
    HSMul.hSMul (β := M₂) c
      (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
              update (β := N) m (Sum.inr val) x (Sum.inl i) :
            (a : (i : ι') → N (Sum.inr i)) → M₂)
          fun (i' : ι') ↦ update (β := N) m (Sum.inr val) x (Sum.inr i') :
        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)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
u : (i : ι ⊕ ι') → N i
⊢ Eq.{v₂ + 1} (α := M₂) ((g.uncurrySum (N := N) : (a : (i : ι ⊕ ι') → N i) → M₂) u : M₂)
    (((g : (a : (i : ι) → N (Sum.inl i)) → MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂) fun (i : ι) ↦
            u (Sum.inl i) :
          (a : (i : ι') → N (Sum.inr i)) → M₂)
        fun (i' : ι') ↦ u (Sum.inr i') :
      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_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
g₁ g₂ :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
⊢ (g₁ + g₂).uncurrySum (N := N) = g₁.uncurrySum (N := N) + g₂.uncurrySum (N := N)

Tactic:
rfl

Premises used: MultilinearMap.uncurrySum, 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_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
r : R
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
⊢ (r • g).uncurrySum (N := N) = r • g.uncurrySum (N := N)

Tactic:
rfl

Premises used: MultilinearMap.uncurrySum, 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_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
f : MultilinearMap R N M₂
H :
  ∀ (x : (i : ι ⊕ ι') → N i),
    Eq.{v₂ + 1} (α := M₂) ((f.currySum (N := N).uncurrySum (N := N) : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)
      ((f : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)
⊢ f.currySum (N := N).uncurrySum (N := N) = f

Tactic:
ext
-- 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₂
x : (i : ι ⊕ ι') → N i
H :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t :
      M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f.currySum (N := N).uncurrySum (N := N) : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)

Tactic:
simp only [uncurrySum_apply, currySum_apply]

Premises used: MultilinearMap.uncurrySum_apply, MultilinearMap.currySum_apply
-- 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₂
x : (i : ι ⊕ ι') → N i
H :
  (fun (t : ι ⊕ ι') ↦
      Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t) =
    x
⊢ Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) fun (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t :
      M₂)
    ((f : (a : (i : ι ⊕ ι') → N i) → M₂) x : M₂)

Tactic:
congr
-- 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₂
x : (i : ι ⊕ ι') → N i
H :
  ∀ (val : ι),
    Eq (α := N (Sum.inl val))
      (Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i'))
        (Sum.inl val))
      (x (Sum.inl val))
H₁ :
  ∀ (val : ι'),
    Eq (α := N (Sum.inr val))
      (Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i'))
        (Sum.inr val))
      (x (Sum.inr val))
⊢ (fun (t : ι ⊕ ι') ↦
      Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t) =
    x

Tactic:
ext (_ | _)
-- 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₂
x : (i : ι ⊕ ι') → N i
val : ι
⊢ Eq (α := N (Sum.inl val))
    (Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i'))
      (Sum.inl val))
    (x (Sum.inl val))

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₂
x : (i : ι ⊕ ι') → N i
val : ι'
⊢ Eq (α := N (Sum.inr val))
    (Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i'))
      (Sum.inr val))
    (x (Sum.inr val))

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)
g :
  MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)
⊢ g.uncurrySum (N := N).currySum (N := N) = g

Tactic:
rfl

Premises used: MultilinearMap.currySum, 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₂
N : ι ⊕ ι' → Type u_1
inst_7 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_8 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
⊢ ∀ (x y : MultilinearMap R N M₂), (x + y).currySum (N := N) = x.currySum (N := N) + y.currySum (N := N)

Tactic:
aesop
-- 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)
⊢ ∀ (m : R) (x : MultilinearMap R N M₂),
    (m • x).currySum (N := N) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (x.currySum (N := N))

Tactic:
aesop
-- 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)
x : MultilinearMap R N M₂
⊢ x.currySum (N := N).uncurrySum (N := N) = x

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)
⊢ Eq (α :=
    (a : MultilinearMap R N M₂) →
      MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
        (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂))
    (⇑(currySumEquiv (N := N)) :
      (a : MultilinearMap R N M₂) →
        MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂))
    (currySum (N := N))

Tactic:
rfl

Premises used: MultilinearMap.currySum, 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_1
inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst_4 : (i : ι ⊕ ι') → Module.{uR, u_1} R (N i)
⊢ Eq (α :=
    (a :
        MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
          (MultilinearMap.{uR, uι', u_1, v₂} R (fun (i : ι') ↦ N (Sum.inr i)) M₂)) →
      MultilinearMap R N M₂)
    (⇑(LinearEquiv.symm (currySumEquiv (N := N))) :
      (a : MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i)) (MultilinearMap R (fun (i : ι') ↦ N (Sum.inr i)) M₂)) →
        MultilinearMap R N M₂)
    (uncurrySum (N := N))

Tactic:
rfl

Premises used: MultilinearMap.uncurrySum, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂
mk : Fin k → M'
ml : Fin l → M'
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((((curryFinFinset R M₂ M' hk hl :
                      (a : MultilinearMap R (fun (x : Fin n) ↦ M') M₂) →
                        MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂))
                    f :
                  MultilinearMap R (fun (x : Fin k) ↦ M')
                    (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)) :
                (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂)
              mk :
            MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂) :
          (a : (i : Fin l) → M') → M₂)
        ml :
      M₂)
    ((f : (a : (i : Fin n) → M') → M₂) fun (i : Fin n) ↦
        Sum.elim mk ml (((finSumEquivOfFinset hk hl).symm : (a : Fin n) → Fin k ⊕ Fin l) i) :
      M₂)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
m : Fin n → M'
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((LinearEquiv.symm (curryFinFinset R M₂ M' hk hl) :
                (a : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂)) →
                  MultilinearMap R (fun (x : Fin n) ↦ M') M₂)
              f :
            MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂) :
          (a : (i : Fin n) → M') → M₂)
        m :
      M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (i : Fin k) ↦
            m ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)) :
          (a : (i : Fin l) → M') → M₂)
        fun (i : Fin l) ↦ m ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)) :
      M₂)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
rw :
  Eq.{v₂ + 1} (α := M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (i : Fin k) ↦
            s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
              ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)) :
          (a : (i : Fin l) → M') → M₂)
        fun (i : Fin l) ↦
        s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
          ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)) :
      M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → M') → M₂)
        fun (x : Fin l) ↦ y :
      M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((LinearEquiv.symm (curryFinFinset R M₂ M' hk hl) :
                (a : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂)) →
                  MultilinearMap R (fun (x : Fin n) ↦ M') M₂)
              f :
            MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂) :
          (a : (i : Fin n) → M') → M₂)
        (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → M') → M₂)
        fun (x : Fin l) ↦ y :
      M₂)

Tactic:
rw [curryFinFinset_symm_apply]

Premises used: MultilinearMap.curryFinFinset_symm_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
h :
  Eq.{v' + 1} (α := (i : Fin k) → M')
    (fun (i : Fin k) ↦
      s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)))
    fun (x_1 : Fin k) ↦ x
h₁ :
  Eq.{v' + 1} (α := (i : Fin l) → M')
    (fun (i : Fin l) ↦
      s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)))
    fun (x : Fin l) ↦ y
⊢ Eq.{v₂ + 1} (α := M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (i : Fin k) ↦
            s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
              ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)) :
          (a : (i : Fin l) → M') → M₂)
        fun (i : Fin l) ↦
        s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
          ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)) :
      M₂)
    (((f : (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂) fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → M') → M₂)
        fun (x : Fin l) ↦ y :
      M₂)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
h :
  ∀ (x_1 : Fin k),
    s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_2 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl x_1)) =
      x
⊢ Eq.{v' + 1} (α := (i : Fin k) → M')
    (fun (i : Fin k) ↦
      s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)))
    fun (x_1 : Fin k) ↦ x

Tactic:
ext