-- 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 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 : (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 : ι
h₂ : ¬k = i
h₁ : (i = k ∨ i ∈ s) ∧ k ≤ i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = b i

Tactic:
rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]

Result:
no goals

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
⊢ ∀ 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

Tactic:
intro i hi

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
i : ι
hi : 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 < 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:
simp_rw [imp_iff_not_or, not_or]

Result:
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

Proof state:
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)

Tactic:
apply propext

Result:
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

Proof state:
case refine_2.e_a.h.e_6.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
⊢ (fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) = fun j =>
    if j = k ∨ j ∈ s → j < i then a j else if i = j then a j - b j else b j

Tactic:
ext j

Result:
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

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 : (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 : ι
h₁ : ¬(i = k ∨ i ∈ s → i < k)
h₂ : ¬k = i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = b i

Tactic:
push_neg at h₁

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 : (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 : ι
h₂ : ¬k = i
h₁ : (i = k ∨ i ∈ s) ∧ k ≤ i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = b i