awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i
have pos : i ∉ s
Tactic: rw [update_of_ne, Finset.piecewise_eq_of_notMem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i
have pos₁ : i ≠ k
Tactic: rw [update_of_ne, Finset.piecewise_eq_of_notMem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = a i - b i
have 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
Tactic: cases h₂
Cleared hypotheses: i, h₁, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) k = a k - b k
have pos : s.piecewise (π := M₁) b a k - b k = a k - b k
Tactic: rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) k = a k - b k
have pos₁ : a k - b k = a k - b k
Tactic: rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = b i
have h₃ : (i = k ∨ i ∈ s) ∧ k ≤ i
Tactic: push Not at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = b i
have neg : s.piecewise (π := M₁) b a i = b i
Tactic: rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k) i = b i
have neg₁ : b i = b i
Tactic: rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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)
have 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₂)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 ι
⊢ 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
have 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)
Tactic: rw [← s.piecewise_idem_right b a, map_sub_map_piecewise]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
have 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
Tactic: refine Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι
⊢ (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
have 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
Tactic: by_cases hjs : j ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: by_cases hjs : j ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [if_pos hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: by_cases hji : j < i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: by_cases hji : j < i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have pos₁ : s.piecewise (π := M₁) a v j = a j
Tactic: rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have pos₂ : a j = a j
Tactic: rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, hjs, hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have 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
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have neg : s.piecewise (π := M₁) a v i - 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have neg₁ : s.piecewise (π := M₁) a v i - b i = a i - b i
Tactic: rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have neg₂ : a i - b i = a i - b i
Tactic: rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ (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
have neg : b j = if j = i then a j - b j else b j
Tactic: rw [if_neg hij, if_neg hij.symm]