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₂
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
⊢ (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))
have 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))
Tactic: cases i using Fin.succAboveCases p
Cleared hypotheses: i, 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₂
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))
⊢ (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))
have 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))
Tactic: cases i using Fin.succAboveCases p
Cleared hypotheses: i, 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₂
p : Fin (n + 1)
f : MultilinearMap R M M₂
x y : M p
⊢ 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))
        ⋯ ⋯)
have 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))
            sorry sorry :
          (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))
              sorry sorry)
            (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))
              sorry sorry) :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)
Tactic: ext
-- 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 : MultilinearMap R M M₂
c : R
x : M p
⊢ 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))
        ⋯ ⋯)
have 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))
            sorry sorry :
          (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))
              sorry sorry) :
          (a : (i : Fin n) → M (p.succAbove i)) → M₂)
        x_1 :
      M₂)
Tactic: ext
-- 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₂
i : Fin (n + 1)
f : M i →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (j : Fin n) ↦ M (i.succAbove j)) M₂
⊢ curryMid (M := M) i (uncurryMid (M := M) i f) = f
have 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₂)
Tactic: ext
-- 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₂
i : Fin (n + 1)
f : MultilinearMap R M M₂
⊢ LinearMap.uncurryMid (M := M) i (curryMid (M := M) i f) = f
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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₂
⊢ f.currySum (N := N).uncurrySum (N := N) = f
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ 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₂)
have 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₂)
Tactic: simp only [uncurrySum_apply, currySum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ 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₂)
have H : (fun (t : ι ⊕ ι') ↦
    Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t) =
  x
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ (fun (t : ι ⊕ ι') ↦
      Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t) =
    x
have 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))
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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))
⊢ (fun (t : ι ⊕ ι') ↦
      Sum.rec (motive := fun (x : ι ⊕ ι') ↦ N x) (fun (i : ι) ↦ x (Sum.inl i)) (fun (i' : ι') ↦ x (Sum.inr i')) t) =
    x
have 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))
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
⊢ 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₂)
have 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₂)
Tactic: rw [curryFinFinset_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
⊢ 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₂)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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
⊢ 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₂)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
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
have h : Membership.mem (α := Fin n) s ((s.orderEmbOfFin hk : (a : Fin k) → Fin n) x_1 : Fin n)
Tactic: rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
⊢ 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
have h : ∀ (x_1 : Fin l),
  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.inr x_1)) =
    y
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
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'
x_1 : Fin l
⊢ 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.inr x_1)) =
    y
have h : ((sᶜ.orderEmbOfFin hl : (a : Fin l) → Fin n) x_1 : Fin n) ∉ s
Tactic: rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]