-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
/-- This calculates the differences between the values of a multilinear map at
two arguments that differ on a finset `s` of `ι`. It requires a
linear order on `ι` in order to express the result. -/
lemma map_piecewise_sub_map_piecewise [LinearOrder ι] (a b v : (i : ι) → M₁ i) (s : Finset ι) :
    f (s.piecewise a v) - f (s.piecewise b v) = ∑ i ∈ s, f
      fun 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

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise 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

Tactic:
by_cases hjs : j ∈ s

Result:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : 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 a v j else if i = j then s.piecewise 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

case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : 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 a v j else if i = j then s.piecewise 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

Proof state:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

Tactic:
rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]

Result:
no goals

Proof state:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

Tactic:
rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]

Result:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Proof state:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ (if i = i then s.piecewise a v i - b i else b i) = if i = i then a i - b i else b i

case neg.inr
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ (∑ i ∈ s, f fun j => if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    ∑ i ∈ s, f fun 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

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise 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

Proof state:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : 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 a v j else if i = j then s.piecewise 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

Tactic:
rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_not_mem _ _ hjs]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ f (s.piecewise a v) - f (s.piecewise b v) =
    ∑ i ∈ s, f fun 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

Tactic:
rw [← s.piecewise_idem_right b a, map_sub_map_piecewise]

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ (∑ i ∈ s, f fun j => if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    ∑ i ∈ s, f fun 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