From 2e06bd9f0f56ec7f72fad9f6bc0acd8ccdc0bf13 Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Fri, 18 Aug 2023 14:30:24 +0000
Subject: [PATCH] feat(Data/Sum): forall_sum_pi (#6658)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
---
 Mathlib/Data/Sum/Basic.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/Data/Sum/Basic.lean b/Mathlib/Data/Sum/Basic.lean
index 2eed0a45702ae..c56e13a11da4c 100644
--- a/Mathlib/Data/Sum/Basic.lean
+++ b/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