-- 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 ι'
inst_6 : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
h0 :
  Eq (α := Π₀ (x : ι'), R)
    (((freeDFinsuppEquiv (κ := κ) :
              (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
            0 :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (β := Π₀ (x : ι'), R) ((0 : (a : ((i : ι) → κ i) × ι') → R) p)
          (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      Π₀ (x : ι'), R)
ha :
  ∀ (i : ((i : ι) → κ i) × ι') (b : R) (f : Π₀ (i : ((i : ι) → κ i) × ι'), R),
    (f : (a : ((i : ι) → κ i) × ι') → R) i = 0 →
      b ≠ 0 →
        Eq (α := Π₀ (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)) :
                  (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
                x :
              Π₀ (x : ι'), R)
            (∑ p : ((i : ι) → κ i) × ι',
                HSMul.hSMul (β := Π₀ (x : ι'), R) ((f : (a : ((i : ι) → κ i) × ι') → R) p)
                  (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
              Π₀ (x : ι'), R) →
          Eq (α := Π₀ (x : ι'), R)
            ((((freeDFinsuppEquiv (κ := κ) :
                        (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                          MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
                      (DFinsupp.single (β := fun (i : ((i : ι) → κ i) × ι') ↦ R) i b + f) :
                    MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
                  (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
                x :
              Π₀ (x : ι'), R)
            (∑ p : ((i : ι) → κ i) × ι',
                HSMul.hSMul (β := Π₀ (x : ι'), R)
                  ((DFinsupp.single (β := fun (i : ((i : ι) → κ i) × ι') ↦ R) i b + f : (a : ((i : ι) → κ i) × ι') → R)
                    p)
                  (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
              Π₀ (x : ι'), R)
⊢ Eq (α := Π₀ (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)) :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (β := Π₀ (x : ι'), R) ((f : (a : ((i : ι) → κ i) × ι') → R) p)
          (DFinsupp.single (β := fun (x : ι') ↦ R) p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      Π₀ (x : ι'), R)

Tactic:
apply DFinsupp.induction f

Premises used: DFinsupp.induction