chore(Multilinear): golf (#17198)

Also add 2 missing `simp` lemmas

Mathlib/Data/Finset/Pi.lean

@@ -92,6 +92,10 @@ lemma pi_nonempty : (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty := by
 @[aesop safe apply (rule_sets := [finsetNonempty])]
 alias ⟨_, pi_nonempty_of_forall_nonempty⟩ := pi_nonempty
 
+@[simp]
+lemma pi_eq_empty : s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅ := by
+  simp [← not_nonempty_iff_eq_empty]
+
 @[simp]
 theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α}
     (ha : a ∉ s) : pi (insert a s) t = (t a).biUnion fun b => (pi s t).image (Pi.cons s a b) := by

Mathlib/Data/Fintype/Pi.lean

@@ -49,12 +49,13 @@ theorem piFinset_subset (t₁ t₂ : ∀ a, Finset (δ a)) (h : ∀ a, t₁ a 
     piFinset t₁ ⊆ piFinset t₂ := fun _ hg => mem_piFinset.2 fun a => h a <| mem_piFinset.1 hg a
 
 @[simp]
-theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅ :=
-  eq_empty_of_forall_not_mem fun _ => by simp
+theorem piFinset_eq_empty : piFinset s = ∅ ↔ ∃ i, s i = ∅ := by simp [piFinset]
 
 @[simp]
-lemma piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty := by
-  simp [Finset.Nonempty, Classical.skolem]
+theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅ := by simp
+
+@[simp]
+lemma piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty := by simp [piFinset]
 
 @[aesop safe apply (rule_sets := [finsetNonempty])]
 alias ⟨_, Aesop.piFinset_nonempty_of_forall_nonempty⟩ := piFinset_nonempty

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -453,14 +453,9 @@ theorem map_sum_finset_aux [DecidableEq ι] [Fintype ι] {n : ℕ} (h : (∑ i,
   induction' n using Nat.strong_induction_on with n IH generalizing A
   -- If one of the sets is empty, then all the sums are zero
   by_cases Ai_empty : ∃ i, A i = ∅
-  · rcases Ai_empty with ⟨i, hi⟩
-    have : ∑ j ∈ A i, g i j = 0 := by rw [hi, Finset.sum_empty]
-    rw [f.map_coord_zero i this]
-    have : piFinset A = ∅ := by
-      refine Finset.eq_empty_of_forall_not_mem fun r hr => ?_
-      have : r i ∈ A i := mem_piFinset.mp hr i
-      simp [hi] at this
-    rw [this, Finset.sum_empty]
+  · obtain ⟨i, hi⟩ : ∃ i, ∑ j ∈ A i, g i j = 0 := Ai_empty.imp fun i hi ↦ by simp [hi]
+    have hpi : piFinset A = ∅ := by simpa
+    rw [f.map_coord_zero i hi, hpi, Finset.sum_empty]
   push_neg at Ai_empty
   -- Otherwise, if all sets are at most singletons, then they are exactly singletons and the result
   -- is again straightforward