feat(logic/basic): forall2_congr lemmas (#4904)

Some helpful lemmas for working with quantifiers, just other versions of what's already there.

src/logic/basic.lean

@@ -635,12 +635,40 @@ variables {α : Sort*} {β : Sort*} {p q : α → Prop} {b : Prop}
 lemma forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a :=
 λ h' a, h a (h' a)
 
+lemma forall₂_congr {p q : α → β → Prop} (h : ∀ a b, p a b ↔ q a b) :
+  (∀ a b, p a b) ↔ (∀ a b, q a b) :=
+forall_congr (λ a, forall_congr (h a))
+
+lemma forall₃_congr {γ : Sort*} {p q : α → β → γ → Prop}
+  (h : ∀ a b c, p a b c ↔ q a b c) :
+  (∀ a b c, p a b c) ↔ (∀ a b c, q a b c) :=
+forall_congr (λ a, forall₂_congr (h a))
+
+lemma forall₄_congr {γ δ : Sort*} {p q : α → β → γ → δ → Prop}
+  (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+  (∀ a b c d, p a b c d) ↔ (∀ a b c d, q a b c d) :=
+forall_congr (λ a, forall₃_congr (h a))
+
 lemma Exists.imp (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a := exists_imp_exists h p
 
 lemma exists_imp_exists' {p : α → Prop} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a))
   (hp : ∃ a, p a) : ∃ b, q b :=
 exists.elim hp (λ a hp', ⟨_, hpq _ hp'⟩)
 
+lemma exists₂_congr {p q : α → β → Prop} (h : ∀ a b, p a b ↔ q a b) :
+  (∃ a b, p a b) ↔ (∃ a b, q a b) :=
+exists_congr (λ a, exists_congr (h a))
+
+lemma exists₃_congr {γ : Sort*} {p q : α → β → γ → Prop}
+  (h : ∀ a b c, p a b c ↔ q a b c) :
+  (∃ a b c, p a b c) ↔ (∃ a b c, q a b c) :=
+exists_congr (λ a, exists₂_congr (h a))
+
+lemma exists₄_congr {γ δ : Sort*} {p q : α → β → γ → δ → Prop}
+  (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+  (∃ a b c d, p a b c d) ↔ (∃ a b c d, q a b c d) :=
+exists_congr (λ a, exists₃_congr (h a))
+
 theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
 ⟨function.swap, function.swap⟩