chore(logic/basic): and_iff_left/right_iff_imp, or.right_comm (#3854

)

Also add `@[simp]` to `forall_bool` and `exists_bool`

src/data/bool.lean

@@ -68,10 +68,10 @@ lemma not_ff : ¬ ff := by simp
 theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
 by cases b; simp
 
-theorem forall_bool {p : bool → Prop} : (∀ b, p b) ↔ p ff ∧ p tt :=
+@[simp] theorem forall_bool {p : bool → Prop} : (∀ b, p b) ↔ p ff ∧ p tt :=
 ⟨λ h, by simp [h], λ ⟨h₁, h₂⟩ b, by cases b; assumption⟩
 
-theorem exists_bool {p : bool → Prop} : (∃ b, p b) ↔ p ff ∨ p tt :=
+@[simp] theorem exists_bool {p : bool → Prop} : (∃ b, p b) ↔ p ff ∨ p tt :=
 ⟨λ ⟨b, h⟩, by cases b; [exact or.inl h, exact or.inr h],
  λ h, by cases h; exact ⟨_, h⟩⟩
 

src/data/finmap.lean

@@ -249,11 +249,11 @@ m.entries.foldl (λ d s, f d s.1 s.2) (λ d s t, H _ _ _ _ _) d
 
 /-- `any f s` returns `tt` iff there exists a value `v` in `s` such that `f v = tt`. -/
 def any (f : Π x, β x → bool) (s : finmap β) : bool :=
-s.foldl (λ x y z, x ∨ f y z) (by simp [or_assoc]; intros; congr' 2; rw or_comm) ff
+s.foldl (λ x y z, x ∨ f y z) (by { intros,  simp [or.right_comm] }) ff
 
 /-- `all f s` returns `tt` iff `f v = tt` for all values `v` in `s`. -/
 def all (f : Π x, β x → bool) (s : finmap β) : bool :=
-s.foldl (λ x y z, x ∧ f y z) (by simp [and_assoc]; intros; congr' 2; rw and_comm) ff
+s.foldl (λ x y z, x ∧ f y z) (by { intros, simp [and.right_comm] }) ff
 
 /-! ### erase -/
 

src/data/set/disjointed.lean

@@ -28,8 +28,7 @@ theorem set.pairwise_on.on_injective {s : set α} {r : α → α → Prop} (hs :
 
 theorem pairwise_on_bool {r} (hr : symmetric r) {a b : α} :
   pairwise (r on (λ c, cond c a b)) ↔ r a b :=
-by simp [pairwise, bool.forall_bool, function.on_fun];
-   exact and_iff_right_of_imp (@hr _ _)
+by simpa [pairwise, function.on_fun] using @hr a b
 
 theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
   pairwise (disjoint on (λ c, cond c a b)) ↔ disjoint a b :=

src/logic/basic.lean

@@ -314,6 +314,12 @@ iff.intro and.left (λ ha, ⟨ha, h ha⟩)
 theorem and_iff_right_of_imp {a b : Prop} (h : b → a) : (a ∧ b) ↔ b :=
 iff.intro and.right (λ hb, ⟨h hb, hb⟩)
 
+@[simp] theorem and_iff_left_iff_imp {a b : Prop} : ((a ∧ b) ↔ a) ↔ (a → b) :=
+⟨λ h ha, (h.2 ha).2, and_iff_left_of_imp⟩
+
+@[simp] theorem and_iff_right_iff_imp {a b : Prop} : ((a ∧ b) ↔ b) ↔ (b → a) :=
+⟨λ h ha, (h.2 ha).1, and_iff_right_of_imp⟩
+
 lemma and.congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
 ⟨λ h ha, by simp [ha] at h; exact h, and_congr_right⟩
 
@@ -325,6 +331,8 @@ lemma and.congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
 
 /-! ### Declarations about `or` -/
 
+theorem or.right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, or_comm b]
+
 theorem or_of_or_of_imp_of_imp (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) : c ∨ d :=
 or.imp h₂ h₃ h₁
 

src/set_theory/zfc.lean

@@ -568,7 +568,7 @@ def funs (x y : Set.{u}) : Set.{u} :=
 {f ∈ powerset (prod x y) | is_func x y f}
 
 @[simp] theorem mem_funs {x y f : Set.{u}} : f ∈ funs x y ↔ is_func x y f :=
-by simp [funs]; exact and_iff_right_of_imp and.left
+by simp [funs, is_func]
 
 -- TODO(Mario): Prove this computably
 noncomputable instance map_definable_aux (f : Set → Set) [H : definable 1 f] : definable 1 (λy, pair y (f y)) :=

test/qpf.lean

@@ -142,9 +142,10 @@ begin
   simp only [qpf.is_uniform, foo, qpf.foo, set.image_univ, not_forall, not_imp],
   existsi [bool,ff,ff,λ a : unit, tt,λ a : unit, ff], split,
   { apply quot.sound, simp [foo.R,qpf.abs,qpf._match_1], },
-  { simp! only [set.range,set.ext_iff], simp,
-    intro h, specialize (h tt), simp at h,
-    apply h () }
+  { simp! only [set.range, set.ext_iff],
+    simp only [not_exists, false_iff, bool.forall_bool, eq_self_iff_true, exists_false, not_true,
+      and_self, set.mem_set_of_eq, iff_false],
+    exact λ h, h () }
 end
 
 /-- intuitive consequence of original definition of `supp`. -/