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 : 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 ι
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₂)
⊢ (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₂)

Tactic:
refine s.induction_on (by simp) ?_
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂)
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
⊢ 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:
ext i
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
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
⊢ 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:
rw [h]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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) j =
    s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m j

Tactic:
simp [j_notMem_s]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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

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]
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
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₂)
⊢ (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₂)

Tactic:
rw [s.piecewise_insert, f.map_update_smul, A, Hrec]

Premises used: Finset.piecewise_insert, MultilinearMap.map_update_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
⊢ 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:
simp [j_notMem_s, mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ c i • m i) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
simpa using map_piecewise_smul f c m Finset.univ

Premises used: MultilinearMap.map_piecewise_smul, Finset.univ
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ c i • m i) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i : ι, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
classical simpa using map_piecewise_smul f c m Finset.univ
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂)
      ((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 _ _ _
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
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₂)
⊢ (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₂)

Tactic:
simpa [← Function.update_smul c m] using this

Premises used: Function.update_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂)
H :
  ∀ (x : (i : ι) → R), Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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
H :
  ∀ (val : Fintype ι), Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)

Tactic:
obtain ⟨_⟩ := nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 ι
⊢ ((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)
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂)
⊢ ((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)
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂)
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₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) x : M₂) ((g : (a : (i : ι) → R) → M₂) x : M₂)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst_7 : CommSemiring A
inst_8 : Algebra R A
inst_9 : Fintype ι
inst_10 : DecidableEq ι
m : (i : ι) → A
i : ι
x y : A
⊢ ∏ i_1 : ι, update (β := fun (x : ι) ↦ A) m i (x + y) i_1 =
    HAdd.hAdd (α := A) (∏ i_1 : ι, update (β := fun (x : ι) ↦ A) m i x i_1)
      (∏ i_1 : ι, update (β := fun (x : ι) ↦ A) m i y i_1)

Tactic:
simp [Finset.prod_update_of_mem, add_mul]

Premises used: add_mul, Finset.prod_update_of_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst_7 : CommSemiring A
inst_8 : Algebra R A
inst_9 : Fintype ι
inst_10 : DecidableEq ι
m : (i : ι) → A
i : ι
c : R
x : A
⊢ ∏ i_1 : ι, update (β := fun (x : ι) ↦ A) m i (c • x) i_1 =
    HSMul.hSMul (β := A) c (∏ i_1 : ι, update (β := fun (x : ι) ↦ A) m i x i_1)

Tactic:
simp [Finset.prod_update_of_mem]

Premises used: Finset.prod_update_of_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Fintype ι
m : ι → A
⊢ Eq.{u_1 + 1} (α := A) ((MultilinearMap.mkPiAlgebra R ι A : (a : (i : ι) → A) → A) m : A) (∏ i : ι, m i : A)

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst_7 : Semiring A
inst_8 : Algebra R A
m : (i : Fin n) → A
i : Fin n
x y : A
⊢ (fun (m : (i : Fin n) → A) ↦ (List.ofFn m).prod) (update (β := fun (x : Fin n) ↦ A) m i (x + y)) =
    HAdd.hAdd (α := A) ((fun (m : (i : Fin n) → A) ↦ (List.ofFn m).prod) (update (β := fun (x : Fin n) ↦ A) m i x))
      ((fun (m : (i : Fin n) → A) ↦ (List.ofFn m).prod) (update (β := fun (x : Fin n) ↦ A) m i y))

Tactic:
simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul,
        mul_add, add_mul]

Premises used: add_mul, List.Nodup.map_update, List.prod_set, List.nodup_finRange, mul_add, List.ofFn_eq_map
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst_7 : Semiring A
inst_8 : Algebra R A
m : (i : Fin n) → A
i : Fin n
c : R
x : A
⊢ (fun (m : (i : Fin n) → A) ↦ (List.ofFn m).prod) (update (β := fun (x : Fin n) ↦ A) m i (c • x)) =
    HSMul.hSMul (β := A) c ((fun (m : (i : Fin n) → A) ↦ (List.ofFn m).prod) (update (β := fun (x : Fin n) ↦ A) m i x))

Tactic:
simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set]

Premises used: List.Nodup.map_update, List.prod_set, List.nodup_finRange, List.ofFn_eq_map
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
m : Fin n → A
⊢ (MultilinearMap.mkPiAlgebraFin R n A : (a : (i : Fin n) → A) → A) m = (List.ofFn m).prod

Tactic:
rfl

Premises used: rfl, List.prod
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
⊢ ((MultilinearMap.mkPiAlgebraFin R n A : (a : (i : Fin n) → A) → A) fun (x : Fin n) ↦ a) = a ^ n

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₁ R
z : M₂
m : (i : ι) → M₁ i
⊢ (f.smulRight (M₁ := M₁) z : (a : (i : ι) → M₁ i) → M₂) m =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) ((f : (a : (i : ι) → M₁ i) → R) m : R) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
m : ι → R
⊢ (MultilinearMap.mkPiRing R ι z : (a : (i : ι) → R) → M₂) m = HSMul.hSMul.{uR, v₂, v₂} (α := R) (∏ i : ι, m i) z

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
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₂)
⊢ MultilinearMap.mkPiRing R ι ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1) = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
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₂
⊢ Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z₁) (MultilinearMap.mkPiRing R ι z₂) ↔
    z₁ = z₂

Tactic:
simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]

Premises used: MultilinearMap.ext_iff, MultilinearMap.mkPiRing_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
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₂
⊢ (∀ (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
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
h :
  ∀ (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:
simpa using h fun _ => 1

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
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₂
h : 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:
simp [h]