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 ∈ B i

Tactic:
simp [B, 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)
⊢ piFinset (δ := α) B ∪ piFinset (δ := α) C ⊆ piFinset (δ := α) A

Tactic:
Finset.union_subset (piFinset_subset _ _ fun i => B_subset_A i)
          (piFinset_subset _ _ fun i => C_subset_A i)

Premises used: Finset.union_subset, Set.Mem, setOf, Fintype.piFinset_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₂}
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)
⊢ piFinset (δ := α) B ∪ piFinset (δ := α) C ⊆ piFinset (δ := α) A

Tactic:
exact
        Finset.union_subset (piFinset_subset _ _ fun i => B_subset_A i)
          (piFinset_subset _ _ fun i => C_subset_A i)

Premises used: Finset.union_subset, Fintype.piFinset_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₂}
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)
⊢ piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C

Tactic:
have pi_BC : piFinset A = piFinset B ∪ piFinset C := by
    apply Finset.Subset.antisymm
    · intro r hr
      by_cases hri₀ : r i₀ = j₂
      · apply Finset.mem_union_right
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ C i₀ := by simp [C, hri₀]
          rwa [hi]
        · simp [C, hi, mem_piFinset.1 hr i]
      · apply Finset.mem_union_left
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ B i₀ := by simp [B, hri₀, mem_piFinset.1 hr i₀]
          rwa [hi]
        · simp [B, hi, mem_piFinset.1 hr i]
    · exact
        Finset.union_subset (piFinset_subset _ _ fun i => B_subset_A i)
          (piFinset_subset _ _ fun i => C_subset_A 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)
pi_BC : piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C
neg :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (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))) :
      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:
rw [A_eq_BC]
-- 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)
pi_BC : piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C
neg :
  HAdd.hAdd (α := M₂) (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i))
      (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i)) =
    ∑ r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (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))) :
      M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
simp only [MultilinearMap.map_update_add, Beq, Ceq, Brec, Crec, pi_BC]

Premises used: MultilinearMap.map_update_add
-- 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)
pi_BC : piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C
neg neg₁ :
  Eq.{v₂ + 1} (α := M₂)
    (∑ x ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (x i))
    (∑ r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i))
⊢ HAdd.hAdd (α := M₂) (∑ r ∈ piFinset (δ := α) B, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i))
      (∑ r ∈ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i)) =
    ∑ r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i)

Tactic:
rw [← Finset.sum_union D]

Premises used: Finset.sum_union
-- 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
A : (i : ι) → Finset (α i)
inst_5 : DecidableEq ι
inst_6 : Fintype ι
⊢ 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:
f.map_sum_finset_aux _ _ rfl

Premises used: MultilinearMap.map_sum_finset_aux, rfl
-- 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 ι
inst_7 : (i : ι) → Fintype (α i)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j : α i, g i j : M₂)
    (∑ r : (i : ι) → α i, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
f.map_sum_finset g fun _ => Finset.univ

Premises used: Finset.univ, Finset.map, Fintype.piFinset, MultilinearMap.map_sum_finset
-- 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_2
inst_5 : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ ∅, g a)) : M₂)
    (∑ a ∈ ∅, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : 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₂
α : Type u_2
inst_5 : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
a : α
s : Finset α
has : a ∉ s
ih :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ s, g a)) : M₂)
    (∑ a ∈ s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ insert a s, g a)) : M₂)
    (∑ a ∈ insert a s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)

Tactic:
simp [Finset.sum_insert has, ih]

Premises used: 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 : ι) → 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_2
inst_5 : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
empty :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ ∅, g a)) : M₂)
    (∑ a ∈ ∅, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ s, g a)) : M₂)
        (∑ a ∈ s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ Insert.insert a s, g a)) : M₂)
      (∑ a ∈ Insert.insert a s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ t, g a)) : M₂)
    (∑ a ∈ t, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)

Tactic:
induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]

Premises used: Insert.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₂
α : Type u_2
inst_5 : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
empty :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ ∅, g a)) : M₂)
    (∑ a ∈ ∅, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ s, g a)) : M₂)
        (∑ a ∈ s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ Insert.insert a s, g a)) : M₂)
      (∑ a ∈ Insert.insert a s, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (∑ a ∈ t, g a)) : M₂)
    (∑ a ∈ t, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (g a)) : M₂)

Tactic:
classical
    induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]

Premises used: Insert.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₂
A : Type u_1
inst_5 : Semiring A
inst_6 : SMul R A
inst_7 : (i : ι) → Module.{u_1, v₁} A (M₁ i)
inst_8 : Module A M₂
inst_9 : ∀ (i : ι), IsScalarTower.{uR, u_1, v₁} R A (M₁ i)
inst_10 : IsScalarTower R A M₂
f : MultilinearMap A M₁ M₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₂) (⇑(restrictScalars R (M₁ := M₁) f) : (a : (i : ι) → M₁ i) → M₂)
    (⇑f : (a : (i : ι) → M₁ i) → M₂)

Tactic:
rfl

Premises used: rfl