awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → (b : β i) → Type u_2
inst_15 : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst_16 : (i : ι) → (b : β i) → Module.{uR, u_2} R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap.{uR, u_1, u_2, v₁} R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) (i : (i : ι) × β i)
    (x y : N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))),
    ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
        (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
          (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
            (update (β := fun (j : (i : ι) × β i) ↦ N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i)))
              m i (x + y))
            i_1)) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i x)
                i_1) :
          M₂)
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i y)
                i_1) :
          M₂)

Tactic:
simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Premises used: Function.apply_update, Sigma.curry_update, Sigma.instDecidableEqSigma, Subsingleton.elim, DFunLike.coe
-- 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 : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → (b : β i) → Type u_2
inst_15 : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst_16 : (i : ι) → (b : β i) → Module.{uR, u_2} R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap.{uR, u_1, u_2, v₁} R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) (i : (i : ι) × β i)
    (x y : N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))),
    ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
        (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
          (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
            (update (β := fun (j : (i : ι) × β i) ↦ N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i)))
              m i (x + y))
            i_1)) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i x)
                i_1) :
          M₂)
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i y)
                i_1) :
          M₂)

Tactic:
classical
    simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Premises used: Sigma.curry_update
-- 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 : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → (b : β i) → Type u_2
inst_15 : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst_16 : (i : ι) → (b : β i) → Module.{uR, u_2} R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap.{uR, u_1, u_2, v₁} R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) (i : (i : ι) × β i)
    (c : R) (x : N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))),
    ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
        (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
          (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
            (update (β := fun (j : (i : ι) × β i) ↦ N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i)))
              m i (c • x))
            i_1)) =
      HSMul.hSMul (β := M₂) c
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i x)
                i_1) :
          M₂)

Tactic:
simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Premises used: Function.apply_update, Sigma.curry_update, Sigma.instDecidableEqSigma, Subsingleton.elim, DFunLike.coe
-- 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 : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → (b : β i) → Type u_2
inst_15 : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst_16 : (i : ι) → (b : β i) → Module.{uR, u_2} R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap.{uR, u_1, u_2, v₁} R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) (i : (i : ι) × β i)
    (c : R) (x : N (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))),
    ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
        (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
          (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
            (update (β := fun (j : (i : ι) × β i) ↦ N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i)))
              m i (c • x))
            i_1)) =
      HSMul.hSMul (β := M₂) c
        ((g : (a : (i : ι) → M₁ i) → M₂) fun (i_1 : ι) ↦
            (f i_1 : (a : (i : β i_1) → N i_1 i) → M₁ i_1)
              (Sigma.curry (β := fun (i : ι) ↦ β i) (γ := N)
                (update (β := fun (j : (i : ι) × β i) ↦
                  N (j.fst (β := fun (i : ι) ↦ β i)) (j.snd (β := fun (i : ι) ↦ β i))) m i x)
                i_1) :
          M₂)

Tactic:
classical
    simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Premises used: Sigma.curry_update
-- 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 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m m' : (i : ι) → M₁ i
t : Finset ι
revert :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
revert m'
-- 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 : AddCommMonoid 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
t : Finset ι
⊢ ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ (m + m') m') : M₂)
      (∑ s ∈ Finset.powerset ∅, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

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 : AddCommMonoid 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
t : Finset ι
refine :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (m' : (i : ι) → M₁ i),
          Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (m + m') m') : M₂)
            (∑ s ∈ s.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)) →
        ∀ (m' : (i : ι) → M₁ i),
          Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) ((insert a s).piecewise (π := M₁) (m + m') m') : M₂)
            (∑ s ∈ (insert a s).powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
⊢ ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
refine Finset.induction_on t (by 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
⊢ (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)

Tactic:
have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
    t.piecewise_insert _ _ _
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
h : ∀ (j : ι), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'

Tactic:
ext j
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
pos :
  ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
neg :
  ∀ (h : ¬j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j

Tactic:
by_cases h : 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
h : j = i
pos : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) i = t.piecewise (π := M₁) (m + m') m' i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j

Tactic:
rw [h]
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
h : j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) i = t.piecewise (π := M₁) (m + m') m' i

Tactic:
simp [hit]
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
h : ¬j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j

Tactic:
simp [h]
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'

Tactic:
have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [hit]
    · simp [h]
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
h : ∀ (j : ι), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''

Tactic:
ext j
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
pos :
  ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
neg :
  ∀ (h : ¬j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j

Tactic:
by_cases h : 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : j = i
pos : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) i = t.piecewise (π := M₁) (m + m'') m'' i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j

Tactic:
rw [h]
-- 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 : AddCommMonoid 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
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) i = t.piecewise (π := M₁) (m + m'') m'' i

Tactic:
simp [m'', hit]