-- 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 :
  (((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)))
conv_lhs₁ 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)))
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)
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
e_a₂ :
  ∀ (i : ι') (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
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)
        j =
      (DFinsupp.single (β := fun (x : ι') ↦ R) (p, j).2 (∏ i : ι, (x i : (a : κ i) → R) ((p, j).1 i)) : (a : ι') → R) j
e_a₄ e_a₅ :
  ∀ (i : ι') (p : (i : ι) → κ i) (j : ι') (h : j ≠ i),
    (((((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 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:
classical
  conv_lhs => rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]
  congr
  ext i
  obtain ⟨p, j⟩ := p
  rcases eq_or_ne j i with rfl | h
  · suffices ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i) by
      simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]
    exact fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm
  · simp [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
      fromDFinsuppEquiv_apply, h]

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, Finset.mem_univ, MultilinearMap.smul_apply, DFinsupp.sigmaCurryEquiv, MultilinearMap.freeDFinsuppEquiv_def, DFinsupp.single_smul, Finset.prod_eq_zero, smul_eq_mul, MultilinearMap.piRingEquiv, mul_one, Eq.symm, rfl, map_smul