awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂
x y : M'
⊢ Eq.{v₂ + 1} (α := M₂)
    (((((curryFinFinset R M₂ M' hk hl :
                    (a : MultilinearMap R (fun (x : Fin n) ↦ M') M₂) →
                      MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂))
                  f :
                MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)) :
              (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂)
            fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → M') → M₂)
        fun (x : Fin l) ↦ y :
      M₂)
    ((f : (a : (i : Fin n) → M') → M₂)
        (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      M₂)
have rw : Eq.{v₂ + 1} (α := M₂)
  ((((LinearEquiv.symm (curryFinFinset R M₂ M' hk hl) :
              (a : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂)) →
                MultilinearMap R (fun (x : Fin n) ↦ M') M₂)
            ((curryFinFinset R M₂ M' hk hl :
                (a : MultilinearMap R (fun (x : Fin n) ↦ M') M₂) →
                  MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂))
              f) :
          MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂) :
        (a : (i : Fin n) → M') → M₂)
      (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
    M₂)
  ((f : (a : (i : Fin n) → M') → M₂)
      (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
    M₂)
Tactic: rw [← curryFinFinset_symm_apply_piecewise_const hk hl, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
Goal:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst : CommSemiring R
inst_1 : AddCommMonoid M'
inst_2 : AddCommMonoid M₂
inst_3 : Module R M'
inst_4 : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂
x y : M'
rw :
  Eq.{v₂ + 1} (α := M₂)
    ((((LinearEquiv.symm (curryFinFinset R M₂ M' hk hl) :
                (a : MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂)) →
                  MultilinearMap R (fun (x : Fin n) ↦ M') M₂)
              ((curryFinFinset R M₂ M' hk hl :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M') M₂) →
                    MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂))
                f) :
            MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂) :
          (a : (i : Fin n) → M') → M₂)
        (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      M₂)
    ((f : (a : (i : Fin n) → M') → M₂)
        (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    (((((curryFinFinset R M₂ M' hk hl :
                    (a : MultilinearMap R (fun (x : Fin n) ↦ M') M₂) →
                      MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap R (fun (x : Fin l) ↦ M') M₂))
                  f :
                MultilinearMap R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)) :
              (a : (i : Fin k) → M') → MultilinearMap R (fun (x : Fin l) ↦ M') M₂)
            fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → M') → M₂)
        fun (x : Fin l) ↦ y :
      M₂)
    ((f : (a : (i : Fin n) → M') → M₂)
        (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      M₂)
have rw₁ : Eq.{v₂ + 1} (α := M₂)
  ((f : (a : (i : Fin n) → M') → M₂)
      (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
    M₂)
  ((f : (a : (i : Fin n) → M') → M₂)
      (s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
    M₂)
Tactic: rw [← curryFinFinset_symm_apply_piecewise_const hk hl, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
⊢ f = g
have H : ∀ (x : (i : ι) → Π₀ (j : κ i), M i j),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) x : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H : ∀ (val : Fintype ι),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
val : Fintype ι
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H : Eq.{uN + 1} (α := N)
  ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
      (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
    N)
  ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
      (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
    N)
Tactic: rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
val : Fintype ι
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
      N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
      N)
have H : Eq.{uN + 1} (α := N)
  (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
    (f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
      DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
  (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
    (g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
      DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
Tactic: simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
val : Fintype ι
⊢ Eq.{uN + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
have H : ∀ (p : (a : ι) → κ a),
  Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p →
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
        N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
        N)
Tactic: congr! 1 with p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (hypothesis)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
val : Fintype ι
p : (a : ι) → κ a
h_1 : Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
      N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
      N)
have h₁ : ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  Eq.{uN + 1} (α := 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) :
          (a : (i : ι) → M i (p i)) → N)
        x :
      N)
    ((g.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 : (i : ι) → M i (p i)) → N)
        x :
      N)
Tactic: simp_rw [MultilinearMap.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H : ∀ (val : Fintype ι),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
Tactic: classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
H :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H₁ : ∀ (val : Fintype ι),
  Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
      N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
      N)
Tactic: classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
H :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
H₁ :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H₂ : ∀ (val : Fintype ι),
  Eq.{uN + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
        DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
Tactic: classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} 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))
      (g.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))
x : (i : ι) → Π₀ (j : κ i), M i j
H :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
H₁ :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
H₂ :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N)
      (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
      (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
have H₃ : ∀ (val : Fintype ι) (p : (a : ι) → κ a),
  Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p →
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
        N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
        N)
Tactic: classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _
-- 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)
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
s : (i : ι) → { s : Multiset (κ i) // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun (β := fun (j : κ i) ↦ M i j) i_1 = 0 }
p : (i : ι) → κ i
⊢ Membership.mem (γ := Multiset ((i : ι) → κ i))
      (Multiset.map
        (fun (f : (a : ι) → Membership.mem (γ := Multiset ι) (Finset.val Finset.univ) a → κ a) (i : ι) ↦ f i ⋯)
        (Multiset.pi (β := κ) (Finset.val Finset.univ) fun (i : ι) ↦ (↑(s i) : Multiset (κ i))))
      p ∨
    Eq.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0
have simp : (∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
    (∀ (a_1 : ι), a a_1 sorry ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a i sorry) = p) ∨
  Eq.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0
Tactic: simp only [Multiset.mem_map, Multiset.mem_pi, Finset.mem_val, Finset.mem_univ,
          forall_true_left]