awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
        HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) →
      (f : (a : (i : ι) → M₁ i) → M₂) ((insert a s).piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
        HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ insert a s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
Tactic: refine s.induction_on (by simp) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
⊢ update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m
have h : ∀ (i : ι),
  update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
i : ι
⊢ update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
have pos : ∀ (h : i = j),
  update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
i : ι
pos :
  ∀ (h : i = j),
    update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
      s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
⊢ update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
have neg : ∀ (h : ¬i = j),
  update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
i : ι
h : i = j
⊢ update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) i =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m i
have pos : update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) j =
  s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) ((insert j s).piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ insert j s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
have A : update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) =
  s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m
Tactic: have A :
    Function.update (s.piecewise (fun i => c i • m i) m) j (m j) =
      s.piecewise (fun i => c i • m i) m := by
    ext i
    by_cases h : i = j
    · rw [h]
      simp [j_notMem_s]
    · simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s_1 : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec :
  (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
A :
  update (β := M₁) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) j (m j) =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m
⊢ (f : (a : (i : ι) → M₁ i) → M₂) ((insert j s).piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ insert j s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
have rw : c j • HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) =
  HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ insert j s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
Tactic: rw [s.piecewise_insert, f.map_update_smul, A, Hrec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring 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₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) (c • m) i x) =
    HSMul.hSMul (β := M₂) (c ^ (Fintype.card ι - 1)) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
have this : (f : (a : (i : ι) → M₁ i) → M₂)
    ((erase Finset.univ i).piecewise (π := M₁) (c • update (β := M₁) m i x) (update (β := M₁) m i x)) =
  HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ _i ∈ erase Finset.univ i, c)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
Tactic: have : f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
      (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x) :=
    map_piecewise_smul f _ _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Finite ι
f g : MultilinearMap R (fun (x : ι) ↦ R) M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
⊢ f = g
have H : ∀ (x : (i : ι) → R), Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Finite ι
f g : MultilinearMap R (fun (x : ι) ↦ R) M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
x : (i : ι) → R
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
have H : ∀ (val : Fintype ι), Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
Tactic: obtain ⟨_⟩ := nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Finite ι
f g : MultilinearMap R (fun (x : ι) ↦ R) M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
x : (i : ι) → R
val : Fintype ι
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
have hf : ((f : (a : (i : ι) → R) → M₂) fun (i : ι) ↦ HSMul.hSMul (β := R) (x i) 1) =
  HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, x i) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
Tactic: have hf := f.map_smul_univ x (fun _ ↦ 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Finite ι
f g : MultilinearMap R (fun (x : ι) ↦ R) M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
x : (i : ι) → R
val : Fintype ι
hf :
  ((f : (a : (i : ι) → R) → M₂) fun (i : ι) ↦ HSMul.hSMul (β := R) (x i) 1) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, x i) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
have hg : ((g : (a : (i : ι) → R) → M₂) fun (i : ι) ↦ HSMul.hSMul (β := R) (x i) 1) =
  HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, x i) ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
Tactic: have hg := g.map_smul_univ x (fun _ ↦ 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
f : MultilinearMap R (fun (x : ι) ↦ R) M₂
⊢ MultilinearMap.mkPiRing R ι ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1) = f
have h : Eq.{v₂ + 1} (α := M₂)
  (((MultilinearMap.mkPiRing R ι ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1) :
          MultilinearMap R (fun (x : ι) ↦ R) M₂) :
        (a : (i : ι) → R) → M₂)
      fun (x : ι) ↦ 1 :
    M₂)
  ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z₁ z₂ : M₂
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z₁) (MultilinearMap.mkPiRing R ι z₂) ↔
    z₁ = z₂
have simp_rw : (∀ (x : (i : ι) → R),
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂) ↔
  z₁ = z₂
Tactic: simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : (i : ι) → R),
      HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂) ↔
    z₁ = z₂
have mp : (∀ (x : (i : ι) → R),
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂) →
  z₁ = z₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z₁ z₂ : M₂
mp :
  (∀ (x : (i : ι) → R),
      HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂) →
    z₁ = z₂
⊢ (∀ (x : (i : ι) → R),
      HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂) ↔
    z₁ = z₂
have mpr : z₁ = z₂ →
  ∀ (x : (i : ι) → R),
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₁ = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, x i) z₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι 0) 0
have h : Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
  ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
have h : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1
Tactic: rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
h : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
have h₁ : Eq.{v₂ + 1} (α := M₂) (0 : M₂) ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
Tactic: rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
h : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1
h₁ : Eq.{v₂ + 1} (α := M₂) (0 : M₂) ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((0 : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
have h₂ : Eq.{v₂ + 1} (α := M₂) 0 0
Tactic: rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z : M₂
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) 0 ↔ z = 0
have rw : Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) (MultilinearMap.mkPiRing R ι 0) ↔ z = 0
Tactic: rw [← mkPiRing_zero, mkPiRing_eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : Fintype ι
z : M₂
rw :
  Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) (MultilinearMap.mkPiRing R ι 0) ↔
    z = 0
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z) 0 ↔ z = 0
have rw₁ : z = 0 ↔ z = 0
Tactic: rw [← mkPiRing_zero, mkPiRing_eq_iff]
-- 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f_1 g_1 f g : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦
        HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
      (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : ι) → M₁ i) ↦
          HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
            ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i x))
      ((fun (m : (i : ι) → M₁ i) ↦
          HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
            ((g : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i y))
have simp : HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂) +
    HAdd.hAdd (α := M₂) (β := M₂) (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) +
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
      (-(g : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
Tactic: simp only [MultilinearMap.map_update_add, sub_eq_add_neg, neg_add]
-- 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 : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x)) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) =
    0
have rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x + x)) : M₂) (0 : M₂)
Tactic: rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]
-- 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 : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x + x)) : M₂) (0 : M₂)
⊢ HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x)) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) =
    0
have rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
Tactic: rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]
-- 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 : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x + x)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
⊢ HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (-x)) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂) =
    0
have rw₂ : Eq.{v₂ + 1} (α := M₂) 0 0
Tactic: rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]
-- 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 : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x - y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
have rw : (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
  HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]
-- 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 : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
rw :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x - y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
have rw₁ : (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + -y)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
    (-(f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]