awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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
⊢ (((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'
have 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
Tactic: obtain rfl | hp := eq_or_ne p p'
Cleared hypotheses: p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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
⊢ (((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'
have 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'
Tactic: obtain rfl | hp := eq_or_ne p p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t))
    (dfinsuppFamily (κ := κ) (M := M) (N := N) 0) 0
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ dfinsuppFamily (κ := κ) (M := M) (N := N) (f + g) =
    dfinsuppFamily (κ := κ) (M := M) (N := N) f + dfinsuppFamily (κ := κ) (M := M) (N := N) g
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ dfinsuppFamily (κ := κ) (M := M) (N := N) (s • f) = s • dfinsuppFamily (κ := κ) (M := M) (N := N) f
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ 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
have 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)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ 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
have 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)
Tactic: ext f p a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
have 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))
Tactic: refine (DFinsupp.sumAddHom_apply _ _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
have 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))
Tactic: classical
  refine (DFinsupp.sumAddHom_apply _ _).trans ?_
  refine Finset.sum_subset (MultilinearMap.support_dfinsuppFamily_subset _ _) ?_
  simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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
| (((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
have 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)
Tactic: rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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
⊢ (((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)))
have 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)))
Tactic: conv_lhs => rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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
⊢ 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)))
have 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)
Tactic: congr