awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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
have this₁ : r i₀ ∈ B i₀
Tactic: have : r i₀ ∈ B i₀ := by simp [B, hri₀, mem_piFinset.1 hr i₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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)
⊢ 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₂)
have pi_BC : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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₂)
have 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₂)
Tactic: rw [A_eq_BC]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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₂)
have 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)
Tactic: simp only [MultilinearMap.map_update_add, Beq, Ceq, Brec, Crec, pi_BC]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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)
have 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))
Tactic: rw [← Finset.sum_union D]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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₂)
have 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₂)
Tactic: induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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₂)
⊢ 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₂)
have 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 a s, g a)) : M₂)
    (∑ a ∈ insert a s, (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]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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₂)
have 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₂)
Tactic: classical
    induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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₂)
⊢ 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₂)
have 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 a s, g a)) : M₂)
    (∑ a ∈ insert a s, (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]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (x : ι₂) ↦ M₂) v i (a + b) ((σ : (a : ι₁) → ι₂) i_1)) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i a ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i b ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)
have simp_rw : ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
    update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a + b) i_1) =
  HAdd.hAdd (α := M₃) (β := M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
        update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
      M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
        update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
      M₃)
Tactic: simp_rw [Function.update_apply_equiv_apply v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a + b) i_1) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)
have rw : HAdd.hAdd (α := M₃) (β := M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃)
        (update (β := fun (x : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a : (a : ι₁) → M₂) :
      M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃)
        (update (β := fun (x : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b : (a : ι₁) → M₂) :
      M₃) =
  HAdd.hAdd (α := M₃) (β := M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
        update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
      M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
        update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
      M₃)
Tactic: rw [m.map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (x : ι₂) ↦ M₂) v i (a • b) ((σ : (a : ι₁) → ι₂) i_1)) =
    HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i b ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)
have simp_rw : ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
    update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a • b) i_1) =
  HSMul.hSMul (β := M₃) a
    ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
        update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
      M₃)
Tactic: simp_rw [Function.update_apply_equiv_apply v]