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
⊢ 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₂)
have this₁ : LT.lt (α := ℕ) (∑ i : ι, #(B i)) (∑ i : ι, #(A i))
Tactic: have : ∑ i, #(B i) < ∑ i, #(A i) := by
      refine sum_lt_sum (fun i _ => card_le_card (B_subset_A i)) ⟨i₀, mem_univ _, ?_⟩
      have : {j₂} ⊆ A i₀ := by simp [hj₂]
      simp only [B, Finset.card_sdiff_of_subset this, Function.update_self, Finset.card_singleton]
      exact Nat.pred_lt (ne_of_gt (lt_trans Nat.zero_lt_one hi₀))
-- 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_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
this : LT.lt (α := ℕ) (∑ i : ι, #(B i)) (∑ i : ι, #(A i))
⊢ 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₂)
have this₁ : ∑ i : ι, #(B i) < n
Tactic: rw [h] at this
Cleared hypotheses: this
-- 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
⊢ 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 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₂)
Tactic: have Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i) := by
    have : ∑ i, #(B i) < ∑ i, #(A i) := by
      refine sum_lt_sum (fun i _ => card_le_card (B_subset_A i)) ⟨i₀, mem_univ _, ?_⟩
      have : {j₂} ⊆ A i₀ := by simp [hj₂]
      simp only [B, Finset.card_sdiff_of_subset this, Function.update_self, Finset.card_singleton]
      exact Nat.pred_lt (ne_of_gt (lt_trans Nat.zero_lt_one hi₀))
    rw [h] at this
    exact IH _ this B rfl
-- 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₂)
⊢ 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₂)
have this₁ : LT.lt (α := ℕ) (∑ i : ι, #(C i)) (∑ i : ι, #(A i))
Tactic: have : (∑ i, #(C i)) < ∑ i, #(A i) :=
      Finset.sum_lt_sum (fun i _ => Finset.card_le_card (C_subset_A i))
        ⟨i₀, Finset.mem_univ _, by simp [C, hi₀]⟩
-- 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_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₂)
this : LT.lt (α := ℕ) (∑ i : ι, #(C i)) (∑ i : ι, #(A i))
⊢ 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₂)
have this₁ : ∑ i : ι, #(C i) < n
Tactic: rw [h] at this
Cleared hypotheses: this
-- 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₂)
⊢ 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 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₂)
Tactic: have Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i) := by
    have : (∑ i, #(C i)) < ∑ i, #(A i) :=
      Finset.sum_lt_sum (fun i _ => Finset.card_le_card (C_subset_A i))
        ⟨i₀, Finset.mem_univ _, by simp [C, hi₀]⟩
    rw [h] at this
    exact IH _ this C rfl
-- 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₂)
⊢ 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 D : Disjoint (piFinset (δ := α) B) (piFinset (δ := α) C)
Tactic: have D : Disjoint (piFinset B) (piFinset C) :=
    haveI : Disjoint (B i₀) (C i₀) := by simp [B, C]
    piFinset_disjoint_of_disjoint B C this
-- 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)
⊢ piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C
have H₁ : piFinset (δ := α) A ⊆ piFinset (δ := α) B ∪ piFinset (δ := α) C
Tactic: apply Finset.Subset.antisymm
-- 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)
H₁ : piFinset (δ := α) A ⊆ piFinset (δ := α) B ∪ piFinset (δ := α) C
⊢ piFinset (δ := α) A = piFinset (δ := α) B ∪ piFinset (δ := α) C
have H₂ : piFinset (δ := α) B ∪ piFinset (δ := α) C ⊆ piFinset (δ := α) A
Tactic: apply Finset.Subset.antisymm
-- 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)
r : (a : ι) → α a
hr : r ∈ piFinset (δ := α) A
⊢ r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C
have pos : ∀ (hri₀ : r i₀ = j₂), r ∈ piFinset (δ := α) B ∪ piFinset (δ := α) C
Tactic: by_cases hri₀ : r i₀ = j₂