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 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
rw :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
rw₁ :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x - y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
have rw₂ : HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-y)) : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]
-- 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 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
rw :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
rw₁ :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
rw₂ :
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-y)) : M₂) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x - y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
have rw₃ : HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]
-- 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 : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i - v)) : M₂)
have rw : (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
  HSub.hSub (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
    (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂))
Tactic: rw [map_update_sub, update_eq_self, sub_sub_cancel]
-- 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 : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
rw :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂))
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i - v)) : M₂)
have rw₁ : (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
  HSub.hSub (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
    (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂))
Tactic: rw [map_update_sub, update_eq_self, sub_sub_cancel]
-- 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 : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
rw :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂))
rw₁ :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂))
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i - v)) : M₂)
have rw₂ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂)
  ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i v) : M₂)
Tactic: rw [map_update_sub, update_eq_self, sub_sub_cancel]
-- 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
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ b a) : M₂) =
    ∑ i ∈ ∅,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
have empty : HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) =
  ∑ i ∈ ∅,
    (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
Tactic: rw [Finset.piecewise_empty, sum_empty, sub_self]
-- 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
empty :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) =
    ∑ i ∈ ∅,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ b a) : M₂) =
    ∑ i ∈ ∅,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
have empty₁ : HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) = 0
Tactic: rw [Finset.piecewise_empty, sum_empty, sub_self]
-- 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
empty :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) =
    ∑ i ∈ ∅,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
empty₁ :
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂) = 0
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ b a) : M₂) =
    ∑ i ∈ ∅,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if Membership.mem (γ := Finset ι) ∅ j → j < i then a j else if i = j then a j - b j else b j
have empty₂ : Eq.{v₂ + 1} (α := M₂) 0 0
Tactic: rw [Finset.piecewise_empty, sum_empty, sub_self]
-- 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
s : Finset ι
⊢ 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
have insert : ∀ (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),
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) ((insert k s).piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ insert k s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j
Tactic: induction s using induction_on_min with
  | empty => rw [Finset.piecewise_empty, sum_empty, sub_self]
  | insert k s hk ih => ?_
Cleared hypotheses: 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 : (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
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) ((insert k s).piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ insert k s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j
have insert : HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
      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 :
      M₂) =
  HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j ∈ insert k s → j < k then a j else if k = j then a j - b j else b j :
      M₂)
    (∑ x ∈ s,
        (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j ∈ insert k s → j < x then a j else if x = j then a j - b j else b j :
      M₂)
Tactic: rw [Finset.piecewise_insert, map_update, ← sub_add, ih,
      add_comm, sum_insert (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
⊢ HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
        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 :
        M₂) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j ∈ insert k s → j < k then a j else if k = j then a j - b j else b j :
        M₂)
      (∑ x ∈ s,
          (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
            if j ∈ insert k s → j < x then a j else if x = j then a j - b j else b j :
        M₂)
have insert : HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
      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 :
      M₂) =
  HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
      M₂)
    (∑ 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 :
      M₂)
Tactic: simp_rw [s.mem_insert]
-- 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
⊢ HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
        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 :
        M₂) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
        M₂)
      (∑ 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 :
        M₂)
have insert : Eq.{v₂ + 1} (α := M₂)
  ((f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
    M₂)
  ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
    M₂)
Tactic: congr 1
-- 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
insert :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
      M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
      M₂)
⊢ HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
        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 :
        M₂) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
        M₂)
      (∑ 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 :
        M₂)
have insert₁ : 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: congr 1
-- 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₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁) (s.piecewise (π := M₁) b a) k (s.piecewise (π := M₁) b a k - b k)) :
      M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j :
      M₂)
have insert : 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: congr
-- 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
⊢ 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
have 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
Tactic: ext 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 : (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 : ι
⊢ 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 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
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 : ι
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
⊢ 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 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
Tactic: split_ifs with h₁ h₂