-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma map_sub_map_piecewise [LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι) :
    f a - f (s.piecewise b a) =
    ∑ i ∈ s, f (fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j)

Proof state:
case refine_2.e_a.h.e_6.h.h.e_c.a
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
hi : i ∈ s
j : ι
⊢ j ∉ s ∨ j < i ↔ ¬j = k ∧ j ∉ s ∨ j < i

Tactic:
apply or_congr_left'

Result:
case refine_2.e_a.h.e_6.h.h.e_c.a.h
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
hi : i ∈ s
j : ι
⊢ ¬j < i → (j ∉ s ↔ ¬j = k ∧ j ∉ s)

Proof state:
case refine_2.e_a
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    ∑ x ∈ s, f fun j => if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j

Tactic:
apply sum_congr rfl

Result:
case refine_2.e_a
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ ∀ x ∈ s,
    (f fun j => if j ∈ s → j < x then a j else if x = j then a j - b j else b j) =
      f fun j => if j = k ∨ j ∈ s → j < x then a j else if x = j 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 : (i : ι) → M₁ i
s : Finset ι
⊢ f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j

Tactic:
refine s.induction_on_min ?_ fun k s hk ih ↦ ?_

Result:
case refine_1
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 : (i : ι) → M₁ i
s : Finset ι
⊢ f a - f (∅.piecewise b a) = ∑ i ∈ ∅, f fun j => if j ∈ ∅ → j < i then a j else if i = j then a j - b j else b j

case refine_2
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - f ((insert k s).piecewise b a) =
    ∑ i ∈ insert k s, f fun j => if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j

Proof state:
case refine_2
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (f (update (s.piecewise b a) k (s.piecewise b a k - b k)) +
      ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    (f fun j => if j ∈ insert k s → j < k then a j else if k = j then a j - b j else b j) +
      ∑ x ∈ s, f fun j => if j ∈ insert k s → j < x then a j else if x = j then a j - b j else b j

Tactic:
simp_rw [s.mem_insert]

Result:
case refine_2
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (f (update (s.piecewise b a) k (s.piecewise b a k - b k)) +
      ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    (f fun j => if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j) +
      ∑ x ∈ s, f fun j => if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j

Proof state:
case refine_2.e_a.h.e_6.h.h
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
hi : i ∈ s
j : ι
⊢ (if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    if j = k ∨ j ∈ s → j < i then a j else if i = j then a j - b j else b j

Tactic:
congr 1

Result:
case refine_2.e_a.h.e_6.h.h.e_c
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 : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
hi : i ∈ s
j : ι
⊢ (j ∈ s → j < i) = (j = k ∨ j ∈ s → j < i)