awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
i : ι'
p : (i : ι) → κ i
j : ι'
e_a :
  (((((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₁ :
  ∀ (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, 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

Tactic:
rcases eq_or_ne j i with rfl | h

Premises used: eq_or_ne, rfl
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
this : ∀ (l : ι), (x l : (a : κ l) → R) (p l) = 0 → Eq.{uR + 1} (α := R) 0 (∏ i : ι, (x i : (a : κ i) → R) (p 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)
      j =
    (DFinsupp.single (β := fun (x : ι') ↦ R) (p, j).2 (∏ i : ι, (x i : (a : κ i) → R) ((p, j).1 i)) : (a : ι') → R) j

Tactic:
simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, DFinsupp.sigmaCurryEquiv, MultilinearMap.freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
e_a : ∀ (l : ι), (x l : (a : κ l) → R) (p l) = 0 → Eq.{uR + 1} (α := R) 0 (∏ i : ι, (x i : (a : κ i) → R) (p 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)
      j =
    (DFinsupp.single (β := fun (x : ι') ↦ R) (p, j).2 (∏ i : ι, (x i : (a : κ i) → R) ((p, j).1 i)) : (a : ι') → R) j

Tactic:
suffices ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i) by
      simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
⊢ ∀ (l : ι), (x l : (a : κ l) → R) (p l) = 0 → Eq.{uR + 1} (α := R) 0 (∏ i : ι, (x i : (a : κ i) → R) (p i))

Tactic:
fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm

Premises used: Finset.mem_univ, Finset.prod_eq_zero, Eq.symm
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
⊢ ∀ (l : ι), (x l : (a : κ l) → R) (p l) = 0 → Eq.{uR + 1} (α := R) 0 (∏ i : ι, (x i : (a : κ i) → R) (p i))

Tactic:
exact fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm

Premises used: Finset.mem_univ, Finset.prod_eq_zero, Eq.symm
-- 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
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

Tactic:
simp [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
      fromDFinsuppEquiv_apply, h]

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, DFinsupp.sigmaCurryEquiv, MultilinearMap.freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv
-- 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
⊢ 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)

Tactic:
simp
-- 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_1 : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
p : ((i : ι) → κ i) × ι'
r : R
f : Π₀ (i : ((i : ι) → κ i) × ι'), R
hfx :
  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) p r + f) :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R)) :
          (a : (i : ι) → Π₀ (x : κ i), R) → Π₀ (x : ι'), R)
        x :
      Π₀ (x : ι'), R)
    (∑ p_1 : ((i : ι) → κ i) × ι',
        HSMul.hSMul (β := Π₀ (x : ι'), R)
          ((DFinsupp.single (β := fun (i : ((i : ι) → κ i) × ι') ↦ R) p r + f : (a : ((i : ι) → κ i) × ι') → R) p_1)
          (DFinsupp.single (β := fun (x : ι') ↦ R) p_1.2 (∏ i : ι, (x i : (a : κ i) → R) (p_1.1 i))) :
      Π₀ (x : ι'), R)

Tactic:
simp [Finset.sum_add_distrib, add_smul, hfx]

Premises used: Finset.sum_add_distrib, add_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Finite ι
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M'
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ ⨁ (j : κ i), M i j) fun (i : ι) ↦
        lof R (κ i) (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ ⨁ (j : κ i), M i j) fun (i : ι) ↦
        lof R (κ i) (M i) (p i))
⊢ f = g

Tactic:
dfinsupp_ext h

Premises used: MultilinearMap.dfinsupp_ext, DirectSum
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
haveI :
  ∀ (this : Fintype ι),
    Eq.{u_3 + 1} (α := M')
      ((((fromDirectSumEquiv (κ := κ) (M := M) :
                  (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                    MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
                f :
              MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
            (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
          fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
        M')
      ((f p : (a : (i : ι) → M i (p i)) → M') x : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDirectSumEquiv (κ := κ) (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')
    ((f p : (a : (i : ι) → M i (p i)) → M') x : M')

Tactic:
haveI : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
rw :
  Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → M')
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i) :
      M')
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDirectSumEquiv (κ := κ) (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')
    ((f p : (a : (i : ι) → M i (p i)) → M') x : M')

Tactic:
rw [fromDirectSumEquiv, ← fromDFinsuppEquiv_single]

Premises used: MultilinearMap.fromDFinsuppEquiv_single, MultilinearMap.fromDirectSumEquiv
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → M')
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i) :
      M')

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Fintype ι
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
rw :
  Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')
    ((((fromDFinsuppEquiv κ R (M := fun (i : ι) (j : κ i) ↦ M i j) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDirectSumEquiv (κ := κ) (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')
    (∑
        p ∈
          Fintype.piFinset (δ := κ) fun (i : ι) ↦
            DFinsupp.support (β := fun (j : κ i) ↦ M i j) ((x : (a : ι) → ⨁ (j : κ a), M a j) i),
        (f p : (a : (i : ι) → M i (p i)) → M') fun (i : ι) ↦
          ((x : (a : ι) → ⨁ (j : κ a), M a j) i : (a : κ i) → M i a) (p i) :
      M')

Tactic:
rw [fromDirectSumEquiv, ← fromDFinsuppEquiv_apply]

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, MultilinearMap.fromDirectSumEquiv
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Fintype ι
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Fintype ι
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
⊢ Eq.{u_3 + 1} (α := M')
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')
    ((((fromDFinsuppEquiv κ R (M := fun (i : ι) (j : κ i) ↦ M i j) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M') →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M')
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → M')
        (⇑x : (a : ι) → ⨁ (j : κ a), M a j) :
      M')

Tactic:
convert! rfl

Premises used: rfl