feat(Logic/Basic): forall_and_index (#27737)

Author: ChrisHughes24

Mathlib/Logic/Basic.lean

@@ -641,6 +641,15 @@ protected theorem Decidable.forall_or_right {q} {p : α → Prop} [Decidable q]
 theorem forall_or_right {q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q :=
   open scoped Classical in Decidable.forall_or_right
 
+@[simp]
+theorem forall_and_index {p q : Prop} {r : p ∧ q → Prop} :
+    (∀ h : p ∧ q, r h) ↔ ∀ (hp : p) (hq : q), r ⟨hp, hq⟩ :=
+  ⟨fun h hp hq ↦ h ⟨hp, hq⟩, fun h h1 ↦ h h1.1 h1.2⟩
+
+theorem forall_and_index' {p q : Prop} {r : p → q → Prop} :
+    (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ h : p ∧ q, r h.1 h.2 :=
+  (forall_and_index (r := fun h => r h.1 h.2)).symm
+
 theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
   | ⟨h, _⟩ => h
 

MathlibTest/LibraryRewrite.lean

@@ -17,6 +17,10 @@ Pattern a → b → c
 · p ∧ p → q
   and_imp
 
+Pattern ∀ (hp : p) (hq : q), r hp hq
+· p ∧ p → q
+  forall_and_index'
+
 Pattern ∀ (x : α), p x → b
 · (∃ x, p) → q
   exists_imp