awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
H :
  Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)

Tactic:
rw [funext (fun i ↦ Eq.symm (Finset.univ_sum_single (x i)))]

Premises used: Finset.univ_sum_single, funext, Eq.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
H :
  Eq.{uN + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)

Tactic:
simp_rw [MultilinearMap.map_sum_finset]

Premises used: MultilinearMap.map_sum_finset
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
H :
  ∀ (p : (a : ι) → κ a),
    Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p →
      Eq.{uN + 1} (α := N)
        ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
        ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
⊢ Eq.{uN + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))

Tactic:
congr! 1 with p
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
h_1 : Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p
⊢ ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    Eq.{uN + 1} (α := N)
      ((f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)
      ((g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)

Tactic:
simp_rw [MultilinearMap.ext_iff] at h

Premises used: MultilinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
h_1 : Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p
h :
  ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    Eq.{uN + 1} (α := N)
      ((f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)
      ((g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)

Tactic:
h _ _

Premises used: Function.update, Pi.single, dite
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
h_1 : Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p
h :
  ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    Eq.{uN + 1} (α := N)
      ((f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)
      ((g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
              LinearMap.single R (M i) (p i) :
            (a : (i : ι) → M i (p i)) → N)
          x :
        N)
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)

Tactic:
exact h _ _
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
dsimp :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := (t : (i : ι) → κ i) → N t) (β := (t : (i : ι) → κ i) → N t)
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
      p

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((x + y) (p i)) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (y (p i) : M i (p i)) i_1)
simp_rw₁ :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i
        (HAdd.hAdd (α := M i (p i)) (x (p i)) (y (p i))) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (y (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]

Premises used: Function.apply_update, MultilinearMap.map_update_add, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
dsimp :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := (t : (i : ι) → κ i) → N t) c
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      p

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((c • x) (p i)) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
simp_rw₁ :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i
        (HSMul.hSMul (β := M i (p i)) c (x (p i))) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.smul_apply, (f p).map_update_smul]

Premises used: Function.apply_update, MultilinearMap.map_update_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
h :
  ∀ (q : (i : ι) → κ i),
    Eq.{uN + 1} (α := N q)
      ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
      (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
⊢ Eq (α := (t : (i : ι) → κ i) → N t)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i) :
      (t : (i : ι) → κ i) → N t)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (j : (i : ι) → κ i) → N j)

Tactic:
ext q
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
h :
  Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) p)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) p)
h₁ :
  ∀ (hpq : p ≠ q),
    Eq.{uN + 1} (α := N q)
      ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
      (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)

Tactic:
obtain rfl | hpq := eq_or_ne p q

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) p)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) p)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
h :
  Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)

Tactic:
rw [Pi.single_eq_of_ne' hpq]

Premises used: Pi.single_eq_of_ne'
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
⊢ ∃ (a : ι), p a ≠ q a

Tactic:
rw [Function.ne_iff] at hpq

Premises used: Function.ne_iff
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : ∃ (a : ι), p a ≠ q a
h :
  ∀ (i : ι) (hpqi : p i ≠ q i),
    Eq.{uN + 1} (α := N q)
      ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
      0
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0

Tactic:
obtain ⟨i, hpqi⟩ := hpq