feat(Data/Sum): forall_sum_pi (#6658)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author: ChrisHughes24

Mathlib/Data/Sum/Basic.lean

@@ -59,6 +59,18 @@ theorem «exists» {p : Sum α β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a)
     | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
 #align sum.exists Sum.exists
 
+theorem forall_sum_pi {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) :
+    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) :=
+  ⟨fun h fa fb => h _, fun h fab => by
+    have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
+      ext ab; cases ab <;> rfl
+    rw [h1]; exact h _ _⟩
+
+theorem exists_sum_pi {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) :
+    (∃ fab, p fab) ↔ (∃ fa fb, p (Sum.rec fa fb)) := by
+  rw [← not_forall_not, forall_sum_pi]
+  simp
+
 theorem inl_injective : Function.Injective (inl : α → Sum α β) := fun _ _ ↦ inl.inj
 #align sum.inl_injective Sum.inl_injective