awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
x_1 : Fin k
h : Membership.mem (α := Fin n) s ((s.orderEmbOfFin hk : (a : Fin k) → Fin n) x_1 : Fin n)
⊢ s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_2 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
      ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl x_1)) =
    x

Tactic:
rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]

Premises used: Finset.piecewise_eq_of_mem, finSumEquivOfFinset_inl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
x_1 : Fin k
⊢ Membership.mem (α := Fin n) s ((s.orderEmbOfFin hk : (a : Fin k) → Fin n) x_1 : Fin n)

Tactic:
apply Finset.orderEmbOfFin_mem

Premises used: Finset.orderEmbOfFin_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
h :
  ∀ (x_1 : Fin l),
    s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_2 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr x_1)) =
      y
⊢ Eq.{v' + 1} (α := (i : Fin l) → M')
    (fun (i : Fin l) ↦
      s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_1 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
        ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)))
    fun (x : Fin l) ↦ y

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
x_1 : Fin l
h : ((sᶜ.orderEmbOfFin hl : (a : Fin l) → Fin n) x_1 : Fin n) ∉ s
⊢ s.piecewise (π := fun (i : Fin n) ↦ M') (fun (x_2 : Fin n) ↦ x) (fun (x : Fin n) ↦ y)
      ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr x_1)) =
    y

Tactic:
rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]

Premises used: finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
x_1 : Fin l
⊢ ((sᶜ.orderEmbOfFin hl : (a : Fin l) → Fin n) x_1 : Fin n) ∉ s

Tactic:
Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

Premises used: Finset.mem_compl, Iff.mp, Finset.orderEmbOfFin_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x y : M'
x_1 : Fin l
⊢ ((sᶜ.orderEmbOfFin hl : (a : Fin l) → Fin n) x_1 : Fin n) ∉ s

Tactic:
exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

Premises used: Finset.mem_compl, Iff.mp, Finset.orderEmbOfFin_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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 R (fun (x : Fin k) ↦ M') (MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin l) ↦ M') M₂)
x : M'
⊢ 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₂)
              f :
            MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂) :
          (a : (i : Fin n) → M') → M₂)
        fun (x_1 : Fin n) ↦ x :
      M₂)
    (((f : (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_1 : Fin l) ↦ x :
      M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Curry
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₂)
rw₁ 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₂)
⊢ 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₂)

Tactic:
rw [← curryFinFinset_symm_apply_piecewise_const hk hl, LinearEquiv.symm_apply_apply]

Premises used: MultilinearMap.curryFinFinset_symm_apply_piecewise_const, LinearEquiv.symm_apply_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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))
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)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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 :
  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) x : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) x : N)

Tactic:
change f (fun i ↦ x i) = g (fun i ↦ x i)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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 ι
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)
⊢ 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:
rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]

Premises used: funext, Eq.symm, DFinsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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 ι
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)))
⊢ 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:
simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]

Premises used: DFinsupp.sum, MultilinearMap.map_sum_finset
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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 ι
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)
⊢ 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:
congr! 1 with p
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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
⊢ ∀ (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

Premises used: MultilinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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
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
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)
⊢ 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:
h _ _

Premises used: DFinsupp.single
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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
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
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)
⊢ 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:
exact h _ _
-- 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)
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
simp :
  (∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
      (∀ (a_1 : ι), a a_1 ⋯ ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a 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
⊢ 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

Tactic:
simp only [Multiset.mem_map, Multiset.mem_pi, Finset.mem_val, Finset.mem_univ,
          forall_true_left]

Premises used: Finset.mem_univ, forall_true_left, Multiset.mem_pi, Multiset.mem_map, Finset.mem_val
-- 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)
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
simp_rw :
  ¬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 →
    ∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
      (∀ (a_1 : ι), a a_1 ⋯ ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a i ⋯) = p
⊢ (∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
      (∀ (a_1 : ι), a a_1 ⋯ ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a 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

Tactic:
simp_rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right