awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
h :
  Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
h : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1
h₁ : Eq.{v₂ + 1} (α := M₂) (0 : M₂) ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
h₂ h₃ : Eq.{v₂ + 1} (α := M₂) 0 0
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)

Tactic:
rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]

Premises used: smul_zero, MultilinearMap.mkPiRing_apply, MultilinearMap.zero_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z : M₂
rw :
  Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) (MultilinearMap.mkPiRing R ι 0) ↔
    z = 0
rw₁ rw₂ : z = 0 ↔ z = 0
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

Premises used: MultilinearMap.mkPiRing_zero, MultilinearMap.mkPiRing_eq_iff
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦ (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)) (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : ι) → M₁ i) ↦ (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)) (update (β := M₁) m i x))
      ((fun (m : (i : ι) → M₁ i) ↦ (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)) (update (β := M₁) m i y))

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦ (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)) (update (β := M₁) m i (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : ι) → M₁ i) ↦ (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)) (update (β := M₁) m i x))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (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₂
m : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((-f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g_1 f g : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
simp :
  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₂) (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
        (-(g : (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₂)
        (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
        (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
⊢ (fun (m : (i : ι) → M₁ i) ↦
        HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
      (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : ι) → M₁ i) ↦
          HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
            ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i x))
      ((fun (m : (i : ι) → M₁ i) ↦
          HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
            ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i y))

Tactic:
simp only [MultilinearMap.map_update_add, sub_eq_add_neg, neg_add]

Premises used: MultilinearMap.map_update_add, sub_eq_add_neg, neg_add
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g_1 f g : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ 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₂) (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
        (-(g : (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₂)
        (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
        (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g_1 f g : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦
        HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
      (update (β := M₁) m i (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((fun (m : (i : ι) → M₁ i) ↦
          HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
            ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i x))

Tactic:
simp only [MultilinearMap.map_update_smul, smul_sub]

Premises used: MultilinearMap.map_update_smul, smul_sub
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f g : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ (f - g : (a : (i : ι) → M₁ i) → M₂) m =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: 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 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x + x)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
rw₂ rw₃ : Eq.{v₂ + 1} (α := M₂) 0 0
⊢ 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 x) : M₂) =
    0

Tactic:
rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

Premises used: MultilinearMap.map_update_add, neg_add_cancel, MultilinearMap.map_coord_zero, Function.update_self, OfNat.ofNat
-- 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 : 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₂)
rw₃ 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₂)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]

Premises used: MultilinearMap.map_update_add, sub_eq_add_neg, MultilinearMap.map_update_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 : 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₂))
rw₂ 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₂)
⊢ (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₂)

Tactic:
rw [map_update_sub, update_eq_self, sub_sub_cancel]

Premises used: Function.update_eq_self, MultilinearMap.map_update_sub, sub_sub_cancel
-- 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
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
empty₂ empty₃ : Eq.{v₂ + 1} (α := M₂) 0 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

Tactic:
rw [Finset.piecewise_empty, sum_empty, sub_self]

Premises used: sub_self, Finset.sum_empty, Finset.piecewise_empty
-- 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
⊢ 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:
?_
-- 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
s : Finset ι
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.insert k s).piecewise (π := M₁) b a) : M₂) =
      ∑ i ∈ Insert.insert k s,
        (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if j ∈ Insert.insert k 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₂) (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

Tactic:
induction s using induction_on_min with
  | empty => rw [Finset.piecewise_empty, sum_empty, sub_self]
  | insert k s hk ih => ?_

Premises used: sub_self, Insert.insert, Finset.sum_empty, Finset.piecewise_empty
-- 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 :
  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.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.insert k s → j < x then a j else if x = j then a j - b j else b j :
        M₂)
⊢ HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) a : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) ((Insert.insert k s).piecewise (π := M₁) b a) : M₂) =
    ∑ i ∈ Insert.insert k s,
      (f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if j ∈ Insert.insert k s → j < i then a j else if i = j then a j - b j else b j

Tactic:
rw [Finset.piecewise_insert, map_update, ← sub_add, ih,
      add_comm, sum_insert (lt_irrefl _ <| hk k ·)]

Premises used: sub_add, Finset.piecewise_insert, lt_irrefl, MultilinearMap.map_update, add_comm, Finset.sum_insert
-- 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 :
  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₂)
⊢ 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.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.insert k 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]

Premises used: Finset.mem_insert
-- 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 :
  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₂)
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)
⊢ 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:
congr 1
-- 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 :
  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
⊢ 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