awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N_1 : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N_1 p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N_1 p)
N : Type u_1
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
p : (i : ι) → κ i
a : (i : ι) → M i (p i)
⊢ Eq.{u_1 + 1} (α := N)
    (((((LinearMap.pi (φ := fun (p : (i : ι) → κ i) ↦ MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N)
                    fun (p : (i : ι) → κ i) ↦
                    compLinearMapₗ (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
                      fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (p i)) ∘ₗ
                  LinearMap.compMultilinearMapₗ R (M₁ := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
                      ((DFinsupp.lsum ℕ (M := fun (a : (i : ι) → κ i) ↦ N) :
                          (a : (i : (i : ι) → κ i) → N →ₗ[R] N) → (Π₀ (i : (i : ι) → κ i), N) →ₗ[R] N)
                        fun (x : (i : ι) → κ i) ↦ LinearMap.id) ∘ₗ
                    dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N)
              f p :
            MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N) :
          (a : (i : ι) → M i (p i)) → N)
        a :
      N)
    ((((LinearMap.id :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N)
              f p :
            MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N) :
          (a : (i : ι) → M i (p i)) → N)
        a :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq.{u_1 + 1} (α := N)
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → N)
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i) :
      N)
    ((f p : (a : (i : ι) → M i (p i)) → N) x : N)

Tactic:
simp [fromDFinsuppEquiv]

Premises used: MultilinearMap.fromDFinsuppEquiv
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ Eq.{u_1 + 1} (α := N)
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → N)
        x :
      N)
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i) :
      N)

Tactic:
(DFinsupp.sumAddHom_apply _ _).trans ?_

Premises used: DFinsupp.sumAddHom_apply, Eq.trans, Trunc.lift
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
refine :
  Eq.{u_1 + 1} (α := N)
    (DFinsupp.sum (β := fun (a : (i : ι) → κ i) ↦ N)
      ((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
          (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
        x)
      fun (x : (i : ι) → κ i) ↦
      (⇑(LinearMap.toAddMonoidHom.{uR, uR, u_1, u_1} (R := R) (S := R) (modM₁ := (fun (x : (i : ι) → κ i) ↦ inst_6) x)
            (modM₂ := inst_6) (σ := RingHom.id R) ((fun (x : (i : ι) → κ i) ↦ (LinearMap.id : N →ₗ[R] N)) x)) :
        (a : N) → N))
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i))
⊢ Eq.{u_1 + 1} (α := N)
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → N)
        x :
      N)
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i) :
      N)

Tactic:
refine (DFinsupp.sumAddHom_apply _ _).trans ?_

Premises used: DFinsupp.sumAddHom_apply, Eq.trans
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ Eq.{u_1 + 1} (α := N)
    (DFinsupp.sum (β := fun (a : (i : ι) → κ i) ↦ N)
      ((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
          (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
        x)
      fun (x : (i : ι) → κ i) ↦
      (⇑(LinearMap.toAddMonoidHom.{uR, uR, u_1, u_1} (R := R) (S := R) (modM₁ := (fun (x : (i : ι) → κ i) ↦ inst_6) x)
            (modM₂ := inst_6) (σ := RingHom.id R) ((fun (x : (i : ι) → κ i) ↦ (LinearMap.id : N →ₗ[R] N)) x)) :
        (a : N) → N))
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i))

Tactic:
Finset.sum_subset (MultilinearMap.support_dfinsuppFamily_subset _ _) ?_

Premises used: DFinsupp.sum, Finset.sum_subset, MultilinearMap.support_dfinsuppFamily_subset
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ∀ (x_1 : (i : ι) → κ i),
    Membership.mem (γ := Finset ((i : ι) → κ i)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i))
        x_1 →
      x_1 ∉
          DFinsupp.support (β := fun (a : (i : ι) → κ i) ↦ N)
            ((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                      (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
                    f :
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
                (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
              x) →
        Eq.{u_1 + 1} (α := N)
          ((fun (x : (i : ι) → κ i) ↦
              ((⇑(LinearMap.toAddMonoidHom.{uR, uR, u_1, u_1} (R := R) (S := R) (modM₁ :=
                      (fun (x : (i : ι) → κ i) ↦ inst_6) x) (modM₂ := inst_6) (σ := RingHom.id R)
                      ((fun (x : (i : ι) → κ i) ↦ (LinearMap.id : N →ₗ[R] N)) x)) :
                  (a : N) → N) :
                (a : N) → N))
            x_1
            ((((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                            (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                              MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
                          f :
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
                      (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
                    x :
                  Π₀ (i : (i : ι) → κ i), N) :
                (a : (i : ι) → κ i) → N)
              x_1))
          0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
p : (i : ι) → κ i
⊢ Eq (α := MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N)
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N)
        f p :
      MultilinearMap.{uR, uι, uM, u_1} 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 : ι) ↦
        DFinsupp.lsingle (M := M i) (p i) :
      MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N)

Tactic:
rfl

Premises used: MultilinearMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
    ((freeDFinsuppEquiv (κ := κ) :
          (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) → MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
        f :
      MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
    (((fromDFinsuppEquiv κ R (M := fun (i : ι) (j : κ i) ↦ R) (N := Π₀ (x : ι'), R) :
            ((p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ R) (Π₀ (x : ι'), R)) ≃ₗ[R]
              MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), R) (Π₀ (x : ι'), R)) :
          (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ R) (Π₀ (x : ι'), R)) →
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), R) (Π₀ (x : ι'), R))
        ((LinearEquiv.piCongrRight (φ := fun (i : (i : ι) → κ i) ↦ Π₀ (j : ι'), R) (ψ := fun (x : (i : ι) → κ i) ↦
              MultilinearMap R (fun (x : ι) ↦ R) (Π₀ (j : ι'), R)) fun (x : (i : ι) → κ i) ↦
              MultilinearMap.piRingEquiv :
            (a : (i : (i : ι) → κ i) → Π₀ (j : ι'), R) →
              (i : (i : ι) → κ i) → MultilinearMap R (fun (x : ι) ↦ R) (Π₀ (j : ι'), R))
          ((DFinsupp.linearEquivFunOnFintype (M := fun (i : (i : ι) → κ i) ↦ Π₀ (j : ι'), R) :
                (a : Π₀ (i : (i : ι) → κ i) (j : ι'), R) → (i : (i : ι) → κ i) → Π₀ (j : ι'), R)
              (((DFinsupp.sigmaCurryLEquiv (R := R) (α := fun (i : (i : ι) → κ i) ↦ ι') (M :=
                        fun (i : (i : ι) → κ i) (j : ι') ↦ R) :
                      (Π₀ (i : (_ : (i : ι) → κ i) × ι'), R) ≃ₗ[R] Π₀ (i : (i : ι) → κ i) (j : ι'), R) :
                    (a : Π₀ (i : (_ : (i : ι) → κ i) × ι'), R) → Π₀ (i : (i : ι) → κ i) (j : ι'), R)
                  ((DFinsupp.domLCongr (M := fun (i : ((i : ι) → κ i) × ι') ↦ R)
                        (Equiv.symm (Equiv.sigmaEquivProd ((i : ι) → κ i) ι')) :
                      (a : Π₀ (i : ((i : ι) → κ i) × ι'), R) → Π₀ (i : (_ : (i : ι) → κ i) × ι'), R)
                    f) :
                Π₀ (i : (i : ι) → κ i) (j : ι'), R) :
            (i : (i : ι) → κ i) → Π₀ (j : ι'), R)) :
      MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), R) (Π₀ (x : ι'), R))

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
inst_5 : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
rw :
  HSMul.hSMul (β := Π₀ (x : ι'), R) r
    ((((freeDFinsuppEquiv (κ := κ) :
                (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
              (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
| (((freeDFinsuppEquiv (κ := κ) :
            (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) → MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
          (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p r) :
        MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
      (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
    x

Tactic:
rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]

Premises used: MultilinearMap.smul_apply, DFinsupp.single_smul, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
inst_5 : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
conv_lhs :
  HSMul.hSMul (β := Π₀ (x : ι'), R) r
      ((((freeDFinsuppEquiv (κ := κ) :
                  (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                    MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
              MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
            (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
          x :
        Π₀ (x : ι'), R) =
    HSMul.hSMul (β := Π₀ (x : ι'), R) r
      (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)))
⊢ (((freeDFinsuppEquiv (κ := κ) :
              (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
            (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p r) :
          MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
        (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
      x =
    HSMul.hSMul (β := Π₀ (x : ι'), R) r
      (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)))

Tactic:
conv_lhs => rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]

Premises used: MultilinearMap.smul_apply, DFinsupp.single_smul, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
inst_5 : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
e_a :
  Eq (α := Π₀ (x : ι'), R)
    ((((freeDFinsuppEquiv (κ := κ) :
                (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
              (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
    (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)) : Π₀ (i : ι'), R)
⊢ HSMul.hSMul (β := Π₀ (x : ι'), R) r
      ((((freeDFinsuppEquiv (κ := κ) :
                  (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                    MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
              MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
            (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
          x :
        Π₀ (x : ι'), R) =
    HSMul.hSMul (β := Π₀ (x : ι'), R) r
      (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
inst_5 : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
e_a :
  ∀ (i : ι'),
    (((((freeDFinsuppEquiv (κ := κ) :
                      (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                    (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
                (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
              x :
            Π₀ (x : ι'), R) :
          (a : ι') → R)
        i =
      (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)) : (a : ι') → R) i
⊢ Eq (α := Π₀ (x : ι'), R)
    ((((freeDFinsuppEquiv (κ := κ) :
                (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
              (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
    (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)) : Π₀ (i : ι'), R)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → Fintype (κ i)
inst_4 : (i : ι) → DecidableEq (κ i)
inst_5 : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
i : ι'
e_a :
  ∀ (p : (i : ι) → κ i) (j : ι'),
    (((((freeDFinsuppEquiv (κ := κ) :
                      (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                    (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) (p, j) 1) :
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
                (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
              x :
            Π₀ (x : ι'), R) :
          (a : ι') → R)
        i =
      (DFinsupp.single (β := fun (x : ι') ↦ R) (p, j).2 (∏ i : ι, (x i : (a : κ i) → R) ((p, j).1 i)) : (a : ι') → R) i
⊢ (((((freeDFinsuppEquiv (κ := κ) :
                    (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                      MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                  (DFinsupp.single (β := fun (a : ((i : ι) → κ i) × ι') ↦ R) p 1) :
                MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
              (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
            x :
          Π₀ (x : ι'), R) :
        (a : ι') → R)
      i =
    (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)) : (a : ι') → R) i

Tactic:
obtain ⟨p, j⟩ := p