awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Ne.{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

Tactic:
⟨fun i _ => p i, fun i => (s i).prop _ |>.resolve_right ?_, rfl⟩

Premises used: _private.0.MultilinearMap.dfinsuppFamily._simp_3, Subtype.prop, And.intro, Exists.intro, Eq.substr, Or.resolve_right, rfl, True.intro
-- 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
h : Ne.{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
refine :
  ∀ (i : ι),
    ¬Eq (α := M i ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i ⋯))
        ((x i).toFun (β := fun (j : κ i) ↦ M i j)
          ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) 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

Tactic:
refine ⟨fun i _ => p i, fun i => (s i).prop _ |>.resolve_right ?_, rfl⟩
-- 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
h : Ne.{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
i : ι
⊢ ¬Eq (α := M i ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i ⋯))
      ((x i).toFun (β := fun (j : κ i) ↦ M i j)
        ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i ⋯))
      0

Tactic:
mt ((f p).map_coord_zero (m := fun i => x i _) i) h

Premises used: mt, MultilinearMap.map_coord_zero
-- 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
h : Ne.{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
i : ι
⊢ ¬Eq (α := M i ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i ⋯))
      ((x i).toFun (β := fun (j : κ i) ↦ M i j)
        ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i ⋯))
      0

Tactic:
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) h

Premises used: mt, MultilinearMap.map_coord_zero
-- 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)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x + y : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((y : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
simp_rw₁ :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        (HAdd.hAdd (α := M i (p i)) ((x : (a : κ i) → M i a) (p i)) ((y : (a : κ i) → M i a) (p i))) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((y : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (x + y) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i y i_1 : (a : κ i_1) → M i_1 a) (p i_1))

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.add_apply, (f p).map_update_add]

Premises used: Function.apply_update, MultilinearMap.map_update_add, DFinsupp.add_apply
-- 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)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((c • x : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
simp_rw₁ :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        (HSMul.hSMul (β := M i (p i)) c ((x : (a : κ i) → M i a) (p i))) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]

Premises used: Function.apply_update, MultilinearMap.map_update_smul, DFinsupp.smul_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst_9 : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
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
p : (i : ι) → κ i
hp :
  Membership.mem (γ := Finset ((i : ι) → κ i))
    (DFinsupp.support (β := N)
      ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
        x))
    p
simp :
  ∀
    (hp :
      ¬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 : ι), ¬Eq (α := M a (p a)) ((x a : (a_1 : κ a) → M a a_1) (p a)) 0
⊢ Membership.mem (γ := Finset ((i : ι) → κ i)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p

Tactic:
simp only [DFinsupp.mem_support_toFun, dfinsuppFamily_apply_toFun, ne_eq,
    Fintype.mem_piFinset] at hp ⊢

Premises used: Fintype.mem_piFinset, DFinsupp.mem_support_toFun, MultilinearMap.dfinsuppFamily_apply_toFun, ne_eq
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst_9 : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
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
p : (i : ι) → κ i
hp : ¬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
i : ι
⊢ ¬Eq (α := M i (p i)) ((x i : (a : κ i) → M i a) (p i)) 0

Tactic:
mt ((f p).map_coord_zero (m := fun i => x i _) i) hp

Premises used: mt, MultilinearMap.map_coord_zero
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst_9 : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
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
p : (i : ι) → κ i
hp : ¬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
i : ι
⊢ ¬Eq (α := M i (p i)) ((x i : (a : κ i) → M i a) (p i)) 0

Tactic:
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) hp

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

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

Tactic:
obtain rfl | hpq := eq_or_ne q p

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

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

Tactic:
rw [DFinsupp.single_eq_of_ne hpq]

Premises used: DFinsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ∃ (a : ι), q a ≠ p a

Tactic:
rw [Function.ne_iff] at hpq

Premises used: Function.ne_iff
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : ∃ (a : ι), q a ≠ p a
h :
  ∀ (i : ι) (hpqi : q i ≠ p i),
    ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
          (a : (i : ι) → κ i) → N a)
        q =
      0
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0

Tactic:
obtain ⟨i, hpqi⟩ := hpq
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
h :
  Eq (α := M i (q i))
    (((fun (i : ι) ↦ (DFinsupp.single (β := M i) (p i) (m i) : Π₀ (i_1 : κ i), M i i_1)) i : (a : κ i) → M i a) (q i)) 0
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0

Tactic:
apply (f q).map_coord_zero i

Premises used: MultilinearMap.map_coord_zero
-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
h h₁ : Eq (α := M i (q i)) ((DFinsupp.single (β := M i) (p i) (m i) : (a : κ i) → M i a) (q i)) 0
⊢ Eq (α := M i (q i))
    (((fun (i : ι) ↦ (DFinsupp.single (β := M i) (p i) (m i) : Π₀ (i_1 : κ i), M i i_1)) i : (a : κ i) → M i a) (q i)) 0

Tactic:
simp_rw [DFinsupp.single_eq_of_ne hpqi]

Premises used: DFinsupp.single_eq_of_ne