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 : (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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ C i₀

Tactic:
have : r i₀ ∈ C i₀ := by simp [C, hri₀]
-- 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
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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : r i₀ = j₂
i : ι
hi : i = i₀
this : r i₀ ∈ C i₀
pos pos₁ pos₂ pos₃ : r i₀ ∈ C i₀
⊢ r i ∈ C i

Tactic:
rwa [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
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : r i₀ = j₂
i : ι
hi : ¬i = i₀
⊢ r i ∈ C i

Tactic:
simp [C, hi, mem_piFinset.1 hr i]

Premises used: Fintype.mem_piFinset, 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₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
neg : r ∈ piFinset (δ := α) B
⊢ r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C

Tactic:
apply Finset.mem_union_left

Premises used: Finset.mem_union_left
-- 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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
⊢ r ∈ piFinset (δ := α) B

Tactic:
mem_piFinset.2 fun i => ?_

Premises used: Iff.mpr, Fintype.mem_piFinset, Set.Mem, setOf
-- 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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
neg : ∀ (i : ι), r i ∈ B i
⊢ r ∈ piFinset (δ := α) B

Tactic:
refine mem_piFinset.2 fun i => ?_

Premises used: Iff.mpr, Fintype.mem_piFinset
-- 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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
i : ι
pos : ∀ (hi : i = i₀), r i ∈ B i
neg : ∀ (hi : ¬i = i₀), r i ∈ B i
⊢ r i ∈ B 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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ B i₀

Tactic:
simp [B, hri₀, mem_piFinset.1 hr i₀]

Premises used: Fintype.mem_piFinset, 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₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ B i₀

Tactic:
have : r i₀ ∈ B i₀ := by simp [B, hri₀, mem_piFinset.1 hr 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_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
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
A_eq_BC :
  (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))
Beq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ B i, g i j
Ceq :
  Eq (α := (a : ι) → M₁ a) (update (β := M₁) (fun (i : ι) ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j)) fun (i : ι) ↦
    ∑ j ∈ C i, g i j
Brec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ B i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Crec :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ C i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
this : r i₀ ∈ B i₀
pos pos₁ pos₂ pos₃ : r i₀ ∈ B i₀
⊢ r i ∈ B i

Tactic:
rwa [hi]