awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
h :
  ∀ (p' : (i : ι) → κ i),
    (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                  (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                    MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        p' =
      (DFinsupp.single (β := N) p
            ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
          (a : (i : ι) → κ i) → N a)
        p'
⊢ Eq (α := Π₀ (t : (i : ι) → κ i), N t)
    ((dfinsuppFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
        x :
      Π₀ (t : (i : ι) → κ i), N t)
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
      Π₀ (i : (i : ι) → κ i), N i)

Tactic:
ext p'
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p' : (i : ι) → κ i
h :
  (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                  MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      p =
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
        (a : (i : ι) → κ i) → N a)
      p
h₁ :
  ∀ (hp : p ≠ p'),
    (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                  (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                    MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        p' =
      (DFinsupp.single (β := N) p
            ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
          (a : (i : ι) → κ i) → N a)
        p'
⊢ (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                  MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      p' =
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
        (a : (i : ι) → κ i) → N a)
      p'

Tactic:
obtain rfl | hp := eq_or_ne p p'

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

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                  MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      p' =
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
        (a : (i : ι) → κ i) → N a)
      p'

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t))
    (dfinsuppFamily (κ := κ) (M := M) (N := N)
      (Pi.single (M := fun (p : (i : ι) → κ i) ↦ MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p
        f))
    (LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) (DFinsupp.lsingle (M := N) p)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) (M₁' := fun (i : ι) ↦ M i (p i)) fun (i : ι) ↦
        DFinsupp.lapply (M := M i) (p i)))

Tactic:
ext <| dfinsuppFamily_single_left_apply _ _

Premises used: MultilinearMap.dfinsuppFamily_single_left_apply, MultilinearMap.ext
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := 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)) =
    LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (DFinsupp.lsingle (M := N) p) (f p)

Tactic:
MultilinearMap.ext <| dfinsuppFamily_single f p

Premises used: MultilinearMap.dfinsuppFamily_single, MultilinearMap.ext
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
H :
  ∀ (x : (i : ι) → Π₀ (j : κ i), M i j) (i : (i : ι) → κ i),
    (((dfinsuppFamily (κ := κ) (M := M) (N := N) 0 : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i =
      (((0 : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t) x : Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t))
    (dfinsuppFamily (κ := κ) (M := M) (N := N) 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
i : (i : ι) → κ i
⊢ (((dfinsuppFamily (κ := κ) (M := M) (N := N) 0 : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i =
    (((0 : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t) x : Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
H :
  ∀ (x : (i : ι) → Π₀ (j : κ i), M i j) (i : (i : ι) → κ i),
    (((dfinsuppFamily (κ := κ) (M := M) (N := N) (f + g) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i =
      (((dfinsuppFamily (κ := κ) (M := M) (N := N) f + dfinsuppFamily (κ := κ) (M := M) (N := N) g :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i
⊢ dfinsuppFamily (κ := κ) (M := M) (N := N) (f + g) =
    dfinsuppFamily (κ := κ) (M := M) (N := N) f + dfinsuppFamily (κ := κ) (M := M) (N := N) g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
i : (i : ι) → κ i
⊢ (((dfinsuppFamily (κ := κ) (M := M) (N := N) (f + g) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i =
    (((dfinsuppFamily (κ := κ) (M := M) (N := N) f + dfinsuppFamily (κ := κ) (M := M) (N := N) g :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : Monoid S
inst_8 : (p : (i : ι) → κ i) → DistribMulAction.{uS, uN} S (N p)
inst_9 : ∀ (p : (i : ι) → κ i), SMulCommClass.{uR, uS, uN} R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
H :
  ∀ (x : (i : ι) → Π₀ (j : κ i), M i j) (i : (i : ι) → κ i),
    (((dfinsuppFamily (κ := κ) (M := M) (N := N) (s • f) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i =
      (((s • dfinsuppFamily (κ := κ) (M := M) (N := N) f :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
              x :
            Π₀ (t : (i : ι) → κ i), N t) :
          (a : (i : ι) → κ i) → N a)
        i
⊢ dfinsuppFamily (κ := κ) (M := M) (N := N) (s • f) = s • dfinsuppFamily (κ := κ) (M := M) (N := N) f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : Monoid S
inst_8 : (p : (i : ι) → κ i) → DistribMulAction.{uS, uN} S (N p)
inst_9 : ∀ (p : (i : ι) → κ i), SMulCommClass.{uR, uS, uN} R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
i : (i : ι) → κ i
⊢ (((dfinsuppFamily (κ := κ) (M := M) (N := N) (s • f) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i =
    (((s • dfinsuppFamily (κ := κ) (M := M) (N := N) f :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      i

Tactic:
simp
-- 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)
h :
  ∀ (f : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) (x : (i : ι) → κ i) (x_1 : (i : ι) → M i (x i)),
    Eq.{u_1 + 1} (α := N)
      ((compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
              (((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)) ∘ₗ
                    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) :
                  (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) →
                    MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
                f)
              fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
            (a : (i : ι) → M i (x i)) → N)
          x_1 :
        N)
      ((compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
              ((LinearMap.id :
                  (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) →
                    MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
                f)
              fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
            (a : (i : ι) → M i (x i)) → N)
          x_1 :
        N)
⊢ Eq (α :=
    MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N →ₗ[R] MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
    ((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)) ∘ₗ
      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.id

Tactic:
ext f x
-- 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 : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
x : (i : ι) → κ i
x_1 : (i : ι) → M i (x i)
⊢ Eq.{u_1 + 1} (α := N)
    ((compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
            (((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)) ∘ₗ
                  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) :
                (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f)
            fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
          (a : (i : ι) → M i (x i)) → N)
        x_1 :
      N)
    ((compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
            ((LinearMap.id :
                (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f)
            fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
          (a : (i : ι) → M i (x i)) → N)
        x_1 :
      N)

Tactic:
simp
-- 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)
h :
  ∀ (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)
⊢ Eq (α :=
    ((p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N) →ₗ[R]
      (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) 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))
    LinearMap.id

Tactic:
ext f p a