awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis.{u_5, u_2, u_3} (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R N
inst_5 : Fintype ι
inst_6 : ∀ (i : ι), Finite.{u_5 + 1} (κ i)
i : ((i : ι) → κ i) × ι'
H :
  ∀ (x : (i : ι) → M i),
    Eq.{u_7 + 1} (α := N)
      ((((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) i :
              MultilinearMap R M N) :
            (a : (i : ι) → M i) → N)
          x :
        N)
      (((LinearMap.compMultilinearMap (M₁ := M) (M₂ := R) (LinearMap.smulRight LinearMap.id ((b' : (a : ι') → N) i.2))
                (compLinearMap (M₁ := M) (M₁' := fun (x : ι) ↦ R) (MultilinearMap.mkPiRing R ι 1) fun (i' : ι) ↦
                  (b i').coord (i.1 i')) :
              MultilinearMap R M N) :
            (a : (i : ι) → M i) → N)
          x :
        N)
⊢ Eq (α := MultilinearMap R M N)
    ((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) i :
      MultilinearMap R M N)
    (LinearMap.compMultilinearMap (M₁ := M) (M₂ := R) (LinearMap.smulRight LinearMap.id ((b' : (a : ι') → N) i.2))
        (compLinearMap (M₁ := M) (M₁' := fun (x : ι) ↦ R) (MultilinearMap.mkPiRing R ι 1) fun (i' : ι) ↦
          (b i').coord (i.1 i')) :
      MultilinearMap R M N)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis.{u_5, u_2, u_3} (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R N
inst_5 : Fintype ι
inst_6 : ∀ (i : ι), Finite.{u_5 + 1} (κ i)
i : ((i : ι) → κ i) × ι'
x : (i : ι) → M i
⊢ Eq.{u_7 + 1} (α := N)
    ((((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) i :
            MultilinearMap R M N) :
          (a : (i : ι) → M i) → N)
        x :
      N)
    (((LinearMap.compMultilinearMap (M₁ := M) (M₂ := R) (LinearMap.smulRight LinearMap.id ((b' : (a : ι') → N) i.2))
              (compLinearMap (M₁ := M) (M₁' := fun (x : ι) ↦ R) (MultilinearMap.mkPiRing R ι 1) fun (i' : ι) ↦
                (b i').coord (i.1 i')) :
            MultilinearMap R M N) :
          (a : (i : ι) → M i) → N)
        x :
      N)

Tactic:
simp +instances only [multilinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm,
    LinearEquiv.symm_symm, LinearEquiv.trans_apply, LinearEquiv.multilinearMapCongrRight_symm_apply,
    Basis.coe_repr_symm, LinearEquiv.multilinearMapCongrLeft_symm_apply, compLinearMap_apply,
    LinearEquiv.coe_coe, LinearMap.compMultilinearMap_apply, freeFinsuppEquiv_single, one_smul,
    Finsupp.linearCombination_single, Basis.coord_apply, mkPiRing_apply, smul_eq_mul, mul_one,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Subsingleton.elim (Fintype.ofFinite ι)]

Premises used: LinearEquiv.multilinearMapCongrLeft_symm_apply, Fintype.ofFinite, LinearMap.id_coe, LinearEquiv.multilinearMapCongrRight_symm_apply, LinearEquiv.trans_apply, LinearEquiv.symm_symm, Finsupp.linearCombination_single, one_smul, MultilinearMap.freeFinsuppEquiv_single, Module.Basis.coe_ofRepr, Module.Basis.coe_repr_symm, MultilinearMap.compLinearMap_apply, LinearMap.coe_smulRight, LinearEquiv.trans_symm, smul_eq_mul, MultilinearMap.mkPiRing_apply, mul_one, Subsingleton.elim, LinearMap.compMultilinearMap_apply, Module.Basis.coord_apply, LinearEquiv.coe_coe, id_eq, Basis.multilinearMap
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis.{u_5, u_2, u_3} (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R N
inst_5 : Fintype ι
inst_6 : ∀ (i : ι), Finite.{u_5 + 1} (κ i)
ii : ((i : ι) → κ i) × ι'
v : (i : ι) → M i
⊢ (((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) ii :
          MultilinearMap R M N) :
        (a : (i : ι) → M i) → N)
      v =
    HSMul.hSMul.{u_2, u_7, u_7} (α := R) (β := N)
      (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (v i) : Finsupp.{u_5, u_2} (κ i) R) : (a : κ i) → R) (ii.1 i))
      ((b' : (a : ι') → N) ii.2 : N)

Tactic:
simp [Basis.multilinearMap_apply]

Premises used: Basis.multilinearMap_apply
-- 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
x y : M 0
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m 0 (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n
x y : M i.succ
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i.succ (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
c : R
x : M i
zero :
  ∀ (x : M 0),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 (c • x)) =
      HSMul.hSMul (β := M₂) c
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                  (a : (i : Fin n) → M i.succ) → M₂)
                (tail (α := M) m) :
              M₂))
          (update (β := M) m 0 x))
succ :
  ∀ (i : Fin n) (x : M i.succ),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ (c • x)) =
      HSMul.hSMul (β := M₂) c
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                  (a : (i : Fin n) → M i.succ) → M₂)
                (tail (α := M) m) :
              M₂))
          (update (β := M) m i.succ x))
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i x))

Tactic:
cases i using Fin.cases
-- 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
x : M 0
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m 0 (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
i : Fin n
x : M i.succ
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i.succ (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
⊢ Eq.{v₂ + 1} (α := M₂) ((f.uncurryLeft (M := M) : (a : (i : Fin n.succ) → M i) → M₂) m : M₂)
    ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
            MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
          (a : (i : Fin n) → M i.succ) → M₂)
        (tail (α := M) m) :
      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₂
x y : M 0
H :
  ∀ (m : (i : Fin n) → M i.succ),
    Eq.{v₂ + 1} (α := M₂)
      ((mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
              (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (x + y) m))
              ⋯ ⋯ :
            (a : (i : Fin n) → M i.succ) → M₂)
          m :
        M₂)
      ((HAdd.hAdd (α := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂)
              (mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
                (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m)) ⋯
                ⋯)
              (mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
                (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m)) ⋯
                ⋯) :
            (a : (i : Fin n) → M i.succ) → M₂)
          m :
        M₂)
⊢ mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
      (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (x + y) m)) ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂)
      (mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
        (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m)) ⋯ ⋯)
      (mk' (M₁ := fun (i : Fin n) ↦ M i.succ)
        (fun (m : (i : Fin n) → M i.succ) ↦ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m)) ⋯ ⋯)

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

Tactic:
cons_add f m x y

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

Tactic:
exact cons_add f m x y

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

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

Tactic:
cons_smul f m c x

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

Tactic:
exact cons_smul f m c x

Premises used: MultilinearMap.cons_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₂
x : M 0
m : (i : Fin n) → M i.succ
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((f.curryLeft (M := M) : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) x :
            MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
          (a : (i : Fin n) → M i.succ) → M₂)
        m :
      M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : 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 : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
⊢ f.uncurryLeft (M := M).curryLeft (M := M) = f

Tactic:
rfl