From 7dea60ba8909cddc931037acf3245aaae36aa486 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Sat, 4 May 2019 17:16:39 -0500
Subject: [PATCH] feat(logic/basic): forall_iff_forall_surj (#977)

a lemma from the perfectoid project
---
 src/logic/basic.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 0d1b5c7384f9b..5ee2b4765247c 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -486,6 +486,13 @@ theorem forall_or_distrib_left {q : Prop} {p : α → Prop} [decidable q] :
 ⟨λ h, if hq : q then or.inl hq else or.inr $ λ x, (h x).resolve_left hq,
   forall_or_of_or_forall⟩
 
+/-- A predicate holds everywhere on the image of a surjective functions iff
+    it holds everywhere. -/
+theorem forall_iff_forall_surj
+  {α β : Type*} {f : α → β} (h : function.surjective f) {P : β → Prop} :
+  (∀ a, P (f a)) ↔ ∀ b, P b :=
+⟨λ ha b, by cases h b with a hab; rw ←hab; exact ha a, λ hb a, hb $ f a⟩
+
 @[simp] theorem exists_prop {p q : Prop} : (∃ h : p, q) ↔ p ∧ q :=
 ⟨λ ⟨h₁, h₂⟩, ⟨h₁, h₂⟩, λ ⟨h₁, h₂⟩, ⟨h₁, h₂⟩⟩