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 : ι) → 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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
insert :
  ∀ (i : ι),
    update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i =
      if i = k ∨ i ∈ s → i < k then a i else if k = i then a i - b i else b i
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) = fun (j : ι) ↦
    if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
pos :
  ∀ (h₁ : i = k ∨ i ∈ s → i < k),
    update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i
pos₁ :
  ∀ (h₁ : ¬(i = k ∨ i ∈ s → i < k)) (h₂ : k = i),
    update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i - b i
neg :
  ∀ (h₁ : ¬(i = k ∨ i ∈ s → i < k)) (h₂ : ¬k = i),
    update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = b i
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i =
    if i = k ∨ i ∈ s → i < k then a i else if k = i then a i - b i else b i

Tactic:
split_ifs with 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 : ι) → 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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
pos : i ∉ s
pos₁ : i ≠ k
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i

Tactic:
rw [update_of_ne, Finset.piecewise_eq_of_notMem]

Premises used: Finset.piecewise_eq_of_notMem, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
⊢ i ∉ s

Tactic:
fun h ↦ (hk i h).not_gt (h₁ <| .inr h)

Premises used: LT.lt.not_gt, Not, Or.inr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
⊢ i ∉ s

Tactic:
exact fun h ↦ (hk i h).not_gt (h₁ <| .inr h)

Premises used: LT.lt.not_gt, Or.inr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
⊢ i ≠ k

Tactic:
fun h ↦ (h₁ <| .inl h).ne h

Premises used: Or.inl, Not, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
⊢ i ≠ k

Tactic:
exact fun h ↦ (h₁ <| .inl h).ne h

Premises used: Or.inl, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
pos :
  ∀ (h₁ : ¬(k = k ∨ k ∈ s → k < k)),
    update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) k = a k - b k
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i - b i

Tactic:
cases h₂
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
h₁ : ¬(k = k ∨ k ∈ s → k < k)
pos : s.piecewise (π := M₁) b a k - b k = a k - b k
pos₁ pos₂ : a k - b k = a k - b k
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) k = a k - b k

Tactic:
rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]

Premises used: lt_irrefl, Function.update_self, Finset.piecewise_eq_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 : ι) → 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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
⊢ (i = k ∨ i ∈ s) ∧ k ≤ i

Tactic:
push Not at h₁

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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
neg : s.piecewise (π := M₁) b a i = b i
neg₁ neg₂ : b i = b i
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) 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₂)]

Premises used: Or.resolve_left, Ne.symm, And.left, Finset.piecewise_eq_of_mem, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
insert :
  ∀ x ∈ s,
    Eq.{v₂ + 1} (α := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < x then a j else if x = j then a j - b j else b j :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j :
        M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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 : (a : (i : ι) → M₁ i) → M₂) 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

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 : ι) → 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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ ∀ x ∈ s,
    Eq.{v₂ + 1} (α := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦ if j ∈ s → j < x then a j else if x = j then a j - b j else b j :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j :
        M₂)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 ι
rw :
  Eq.{v₂ + 1} (α := M₂)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (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)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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)
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) a v) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) b v) : M₂) =
    ∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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]

Premises used: Finset.piecewise_idem_right, MultilinearMap.map_sub_map_piecewise
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 ι
⊢ Eq.{v₂ + 1} (α := M₂)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (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)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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:
Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_

Premises used: funext, MultilinearMap.congr_arg, 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 : ι) → 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 ι
refine :
  ∀ (i : ι) (hi : i ∈ s) (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
⊢ Eq.{v₂ + 1} (α := M₂)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (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)
    (∑ i ∈ s,
      (f : (a : (i : ι) → M₁ i) → M₂) 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 ↦ ?_

Premises used: funext, MultilinearMap.congr_arg, 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 : ι) → 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 : ι
pos :
  ∀ (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
neg :
  ∀ (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
⊢ (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

Tactic:
by_cases hjs : 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 : ι) → 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
pos :
  (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 < i then a j else if j = i then a j - b j else b 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

Tactic:
rw [if_pos hjs]

Premises used: if_pos
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
pos :
  ∀ (hji : j < i),
    (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 < i then a j else if j = i then a j - b j else b j
neg :
  ∀ (hji : ¬j < i),
    (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 < i then a j else if j = i then a j - b j else b 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 < i then a j else if j = i then a j - b j else b j

Tactic:
by_cases hji : 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 : ι) → 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
pos : s.piecewise (π := M₁) a v j = if j < i then a j else if j = i then a j - b j else b j
pos₁ : s.piecewise (π := M₁) a v j = a j
pos₂ pos₃ : a j = a 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 < 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]

Premises used: if_pos, Finset.piecewise_eq_of_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
neg : (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
⊢ (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 < 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]

Premises used: Iff.mpr, Classical.not_imp, And.intro, if_neg
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
neg :
  ∀ (hjs : i ∈ s) (hji : ¬i < i),
    (if i = i then s.piecewise (π := M₁) a v i - b i else b i) = if i = i then a i - b i else b i
neg₁ : ∀ (hij : i ≠ 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
⊢ (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

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 hjs : i ∈ s
hji : ¬i < i
neg : s.piecewise (π := M₁) a v i - b i = if i = i then a i - b i else b i
neg₁ : s.piecewise (π := M₁) a v i - b i = a i - b i
neg₂ neg₃ : a i - b i = a i - b i
⊢ (if i = i then s.piecewise (π := M₁) a v i - b i else b i) = if i = i then a i - b i else b i

Tactic:
rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]

Premises used: if_pos, Finset.piecewise_eq_of_mem, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
neg₁ neg₂ : b j = 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

Tactic:
rw [if_neg hij, if_neg hij.symm]

Premises used: Ne.symm, if_neg
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
neg₂ neg₃ : 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

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

Premises used: False.elim, if_pos, Finset.piecewise_eq_of_notMem, if_neg