awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this_1 : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
Ai_card : ∀ (i : ι), #(A i) = 1
this :
  ∀ r ∈ piFinset (δ := α) A,
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
simp only [Finset.sum_congr rfl this, Ai_card, card_piFinset, prod_const_one, one_nsmul,
      Finset.sum_const]

Premises used: Fintype.card_piFinset, Finset.prod_const_one, one_nsmul, Finset.sum_congr, rfl, Finset.sum_const
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∃ (i : ι), 1 < #(A i)
⊢ ∃ (i : ι), 1 < #(A i)

Tactic:
Ai_singleton
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∃ (i : ι), 1 < #(A i)
neg :
  ∀ (i₀ : ι) (hi₀ : 1 < #(A i₀)),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
      (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
obtain ⟨i₀, hi₀⟩ : ∃ i, 1 < #(A i) := Ai_singleton
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
⊢ ∃ (j₁ : α i₀) (j₂ : α i₀), j₁ ∈ A i₀ ∧ j₂ ∈ A i₀ ∧ j₁ ≠ j₂

Tactic:
Finset.one_lt_card_iff.1 hi₀

Premises used: Finset.one_lt_card_iff, Iff.mp
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
neg :
  ∀ (j₁ j₂ : α i₀),
    j₁ ∈ A i₀ →
      ∀ (hj₂ : j₂ ∈ A i₀),
        j₁ ≠ j₂ →
          Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
            (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
obtain ⟨j₁, j₂, _, hj₂, _⟩ : ∃ j₁ j₂, j₁ ∈ A i₀ ∧ j₂ ∈ A i₀ ∧ j₁ ≠ j₂ :=
    Finset.one_lt_card_iff.1 hi₀

Premises used: Finset.one_lt_card_iff, Iff.mp
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
i : ι
pos : ∀ (hi : i = i₀), B i ⊆ A i
neg : ∀ (hi : ¬i = i₀), B i ⊆ A i
⊢ B i ⊆ A i

Tactic:
by_cases hi : i = 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
i : ι
hi : i = i₀
pos : B i₀ ⊆ A i₀
⊢ B i ⊆ A i

Tactic:
rw [hi]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
i : ι
hi : i = i₀
⊢ B i₀ ⊆ A i₀

Tactic:
simp only [B, sdiff_subset, update_self]

Premises used: Function.update_self, Finset.sdiff_subset
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
i : ι
hi : ¬i = i₀
⊢ B i ⊆ A i

Tactic:
simp only [B, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]

Premises used: Finset.Subset.refl, Ne, not_false_iff, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
⊢ ∀ (i : ι), B i ⊆ A i

Tactic:
have B_subset_A : ∀ i, B i ⊆ A i := by
    intro i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [B, sdiff_subset, update_self]
    · simp only [B, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
pos : ∀ (hi : i = i₀), C i ⊆ A i
neg : ∀ (hi : ¬i = i₀), C i ⊆ A i
⊢ C i ⊆ A i

Tactic:
by_cases hi : i = 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
hi : i = i₀
pos : C i₀ ⊆ A i₀
⊢ C i ⊆ A i

Tactic:
rw [hi]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
hi : i = i₀
⊢ C i₀ ⊆ A i₀

Tactic:
simp only [C, hj₂, Finset.singleton_subset_iff, update_self]

Premises used: Finset.singleton_subset_iff, Function.update_self
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
hi : ¬i = i₀
⊢ C i ⊆ A i

Tactic:
simp only [C, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]

Premises used: Finset.Subset.refl, Ne, not_false_iff, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
⊢ ∀ (i : ι), C i ⊆ A i

Tactic:
have C_subset_A : ∀ i, C i ⊆ A i := by
    intro i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [C, hj₂, Finset.singleton_subset_iff, update_self]
    · simp only [C, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
h₁ :
  ∀ (i : ι),
    ∑ j ∈ A i, g i j =
      update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
        (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)) i
⊢ (fun (i : ι) ↦ ∑ j ∈ A i, g i j) =
    update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
      (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j))

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
pos :
  ∀ (hi : i = i₀),
    ∑ j ∈ A i, g i j =
      update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
        (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)) i
neg :
  ∀ (hi : ¬i = i₀),
    ∑ j ∈ A i, g i j =
      update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
        (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)) i
⊢ ∑ j ∈ A i, g i j =
    update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
      (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)) i

Tactic:
by_cases hi : i = 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
pos : ∑ j ∈ A i₀, g i₀ j = HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)
⊢ ∑ j ∈ A i, g i j =
    update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀
      (HAdd.hAdd (α := M₁ i₀) (∑ j ∈ B i₀, g i₀ j) (∑ j ∈ C i₀, g i₀ j)) i

Tactic:
rw [hi, update_self]

Premises used: Function.update_self