awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ (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))
have 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))
Tactic: cases i using Fin.cases
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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))
⊢ (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))
have 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))
Tactic: cases i using Fin.cases
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ 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)) ⋯ ⋯)
have 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)) sorry
            sorry :
          (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)) sorry sorry)
            (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)) sorry
              sorry) :
          (a : (i : Fin n) → M i.succ) → M₂)
        m :
      M₂)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ 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)) ⋯ ⋯)
have 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)) sorry
            sorry :
          (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)) sorry
              sorry) :
          (a : (i : Fin n) → M i.succ) → M₂)
        m :
      M₂)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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₂
⊢ f.curryLeft (M := M).uncurryLeft (M := M) = f
have 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₂)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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.succ
x y : M i
⊢ (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 (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 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 y))
have last : ∀ (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: cases i using Fin.lastCases
Cleared hypotheses: i, x, y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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.succ
c : R
x : M i
⊢ (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 (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 x))
have last : ∀ (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: cases i using Fin.lastCases
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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))
⊢ (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))
have 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))
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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₂)
⊢ f.uncurryRight (M := M).curryRight (M := M) = f
have 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₂)
Tactic: ext m x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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)
⊢ 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₂)
have 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₂)
Tactic: simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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)
⊢ 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₂)
have 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₂)
Tactic: rw [init_snoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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₂
⊢ f.curryRight (M := M).uncurryRight (M := M) = f
have 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₂)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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 y : M i
⊢ (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)) =
    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 i 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))
have x₁ : ∀ (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: cases i using Fin.succAboveCases p
Cleared hypotheses: i, x, y