awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
neg : b j = if j = i then a j - b j else b j
⊢ (if i = j then s.piecewise (π := M₁) a v j - b j else b j) = if j = i then a j - b j else b j
have neg₁ : b j = b j
Tactic: rw [if_neg hij, if_neg hij.symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
have neg : (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) = v j
Tactic: rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
neg :
  (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) =
    v j
⊢ (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
have neg₁ : s.piecewise (π := M₁) a v j = v j
Tactic: rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
neg :
  (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) =
    v j
neg₁ : s.piecewise (π := M₁) a v j = v j
⊢ (if j ∈ s → j < i then s.piecewise (π := M₁) a v j else if i = j then s.piecewise (π := M₁) a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
have neg₂ : v j = v j
Tactic: rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h : (i : ι) → M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (x + h) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
have rw : HAdd.hAdd (α := M₂)
    (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
    (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
      (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
    ∑ s ∈ Finset.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
Tactic: rw [add_comm, map_add_univ, ← Finset.powerset_univ,
      ← sum_filter_add_sum_filter_not _ (2 ≤ #·)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h : (i : ι) → M₁ i
⊢ HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s ∈ Finset.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
have simp_rw : HAdd.hAdd (α := M₂)
    (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
    (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 2, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
    ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
Tactic: simp_rw [not_le, Nat.lt_succ_iff, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h : (i : ι) → M₁ i
simp_rw :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 2,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
⊢ HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s ∈ Finset.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
have simp_rw₁ : HAdd.hAdd (α := M₂)
    (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
    (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 ≤ 1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
    ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
Tactic: simp_rw [not_le, Nat.lt_succ_iff, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h : (i : ι) → M₁ i
simp_rw :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 2,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₁ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 ≤ 1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
⊢ HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s ∈ Finset.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
have simp_rw₂ : HAdd.hAdd (α := M₂)
    (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
    (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 1 ∨ #x_1 = 1,
      (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
    ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
Tactic: simp_rw [not_le, Nat.lt_succ_iff, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ HSub.hSub (β := M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (x + h) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (x + h') : M₂))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
have simp_rw : HSub.hSub (β := M₂)
    (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
          ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
        ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) -
      (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
          ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
        ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x)))
    ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
  ∑ s : Finset ι with 2 ≤ #s,
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
Tactic: simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
    ← map_sub, add_sub_cancel_left, sum_sub_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h h' : (i : ι) → M₁ i
simp_rw :
  HSub.hSub (β := M₂)
      (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
          ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) -
        (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
          ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x)))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
⊢ HSub.hSub (β := M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (x + h) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (x + h') : M₂))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
have simp_rw₁ : HSub.hSub (β := M₂)
    (HAdd.hAdd (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        (HAdd.hAdd (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂)
          (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)) -
      HAdd.hAdd (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        (HAdd.hAdd (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂)
          (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)))
    ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
  ∑ s : Finset ι with 2 ≤ #s,
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
Tactic: simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
    ← map_sub, add_sub_cancel_left, sum_sub_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
z z' : M₂
⊢ MultilinearMap.mkPiRing R ι (z + z') =
    HAdd.hAdd (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z)
      (MultilinearMap.mkPiRing R ι z')
have h : Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (z + z') : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
  ((HAdd.hAdd (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z)
          (MultilinearMap.mkPiRing R ι z') :
        (a : (i : ι) → R) → M₂)
      fun (x : ι) ↦ 1 :
    M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
c : R
z : M₂
⊢ MultilinearMap.mkPiRing R ι (c • z) =
    HSMul.hSMul (α := R) (β := MultilinearMap R (fun (x : ι) ↦ R) M₂) ((RingHom.id R : (a : R) → R) c : R)
      (MultilinearMap.mkPiRing R ι z)
have h : Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (c • z) : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
  ((HSMul.hSMul (α := R) (β := MultilinearMap R (fun (x : ι) ↦ R) M₂) ((RingHom.id R : (a : R) → R) c : R)
          (MultilinearMap.mkPiRing R ι z) :
        (a : (i : ι) → R) → M₂)
      fun (x : ι) ↦ 1 :
    M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)
have let : ∀ (i : ι),
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)
Tactic: let ⟨i⟩ := ‹Nonempty ι›
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)
have refine_1 : ∀ (j : ι) (hij : j = i), update (β := M₁) x i (c • x i) j ∈ p j
Tactic: refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
refine_1 : ∀ (j : ι) (hij : j = i), update (β := M₁) x i (c • x i) j ∈ p j
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)
have refine_2 : ∀ (j : ι) (hij : ¬j = i), update (β := M₁) x i (c • x i) j ∈ p j
Tactic: refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
refine_1 : ∀ (j : ι) (hij : j = i), update (β := M₁) x i (c • x i) j ∈ p j
refine_2 : ∀ (j : ι) (hij : ¬j = i), update (β := M₁) x i (c • x i) j ∈ p j
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)
have refine_3 : (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (c • x i)) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
Tactic: refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ update (β := M₁) x i (c • x i) j ∈ p j
have refine_1 : c • x i ∈ p i
Tactic: rw [hij, update_self]