-- Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
theorem support_dfinsuppFamily_subset
    [∀ i, DecidableEq (κ i)]
    [∀ i j, (x : M i j) → Decidable (x ≠ 0)] [∀ i, (x : N i) → Decidable (x ≠ 0)]
    (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p))
    (x : ∀ i, Π₀ j : κ i, M i j) :
    (dfinsuppFamily f x).support ⊆ Fintype.piFinset fun i => (x i).support

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : ¬((f p) fun i => (x i) (p i)) = 0
i : ι
⊢ ¬(x i) (p i) = 0

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

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ((dfinsuppFamily f) x).support ⊆ Fintype.piFinset fun i => (x i).support

Tactic:
intro p hp

Result:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : p ∈ ((dfinsuppFamily f) x).support
⊢ p ∈ Fintype.piFinset fun i => (x i).support

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : p ∈ ((dfinsuppFamily f) x).support
⊢ p ∈ Fintype.piFinset fun i => (x i).support

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

Result:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : ¬((f p) fun i => (x i) (p i)) = 0
⊢ ∀ (a : ι), ¬(x a) (p a) = 0

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : ¬((f p) fun i => (x i) (p i)) = 0
⊢ ∀ (a : ι), ¬(x a) (p a) = 0

Tactic:
intro i

Result:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : ¬((f p) fun i => (x i) (p i)) = 0
i : ι
⊢ ¬(x i) (p i) = 0