awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : ¬j = i
pos :
  ∀ (h' : j ∈ t), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
neg :
  ∀ (h' : j ∉ t), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j

Tactic:
by_cases h' : j ∈ t
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : ¬j = i
h' : j ∈ t
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j

Tactic:
simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : ¬j = i
h' : j ∉ t
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j

Tactic:
simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''

Tactic:
have C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m'' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [m'', hit]
    · by_cases h' : j ∈ t <;> simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
rw :
  HAdd.hAdd (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'))
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'')) =
    HAdd.hAdd (α := M₂) (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) m m'))
      (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ (insert i t).powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
rw [A, f.map_update_add, B, C, Finset.sum_powerset_insert hit, Hrec, Hrec, add_comm (_ : M₂)]

Premises used: MultilinearMap.map_update_add, add_comm, Finset.sum_powerset_insert
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
e_a :
  Eq.{v₂ + 1} (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m''))
    (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
⊢ HAdd.hAdd (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'))
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'')) =
    HAdd.hAdd (α := M₂) (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) m m'))
      (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
⊢ Eq.{v₂ + 1} (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m''))
    (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))

Tactic:
Finset.sum_congr rfl fun s hs => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
e_a :
  ∀ (s : Finset ι) (hs : s ∈ t.powerset),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i s).piecewise (π := M₁) m m') : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m''))
    (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))

Tactic:
refine Finset.sum_congr rfl fun s hs => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
h : ∀ (j : ι), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
⊢ (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
pos : ∀ (h : j = i), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
neg : ∀ (h : ¬j = i), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j

Tactic:
by_cases h : j = i
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : j = i
pos : (insert i s).piecewise (π := M₁) m m' i = s.piecewise (π := M₁) m m'' i
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : j = i
⊢ (insert i s).piecewise (π := M₁) m m' i = s.piecewise (π := M₁) m m'' i

Tactic:
simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]

Premises used: Finset.notMem_of_mem_powerset_of_notMem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
pos : ∀ (h' : j ∈ s), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
neg : ∀ (h' : j ∉ s), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j

Tactic:
by_cases h' : j ∈ s
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
h' : j ∈ s
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j

Tactic:
simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
h' : j ∉ s
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j

Tactic:
simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
⊢ (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''

Tactic:
have : (insert i s).piecewise m m' = s.piecewise m m'' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]
    · by_cases h' : j ∈ s <;> simp [m'', h, h']
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
this : (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''
e_a e_a₁ :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i s).piecewise (π := M₁) m m') : M₂)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
m m' : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (m + m') : M₂)
    (∑ s : Finset ι, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
simpa using f.map_piecewise_add m m' Finset.univ

Premises used: Finset.univ, MultilinearMap.map_piecewise_add
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
pos :
  ∀ (Ai_empty : ∃ (i : ι), A i = ∅),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
      (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
neg :
  ∀ (Ai_empty : ∀ (i : ι), (A i).Nonempty),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
      (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
by_cases! Ai_empty : ∃ i, A i = ∅