From 6e0d2d3bbe21e2632eee2768665c618b054b9d46 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 1 Jul 2021 11:10:36 +0000
Subject: [PATCH] feat(logic/basic): add two simp lemmas (#8148)

---
 src/logic/basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index e8b0495626554..043d20e39c8da 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -384,6 +384,12 @@ iff.intro and.right (λ hb, ⟨h hb, hb⟩)
 @[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⟩
 
+@[simp] lemma iff_self_and {p q : Prop} : (p ↔ p ∧ q) ↔ (p → q) :=
+by rw [@iff.comm p, and_iff_left_iff_imp]
+
+@[simp] lemma iff_and_self {p q : Prop} : (p ↔ q ∧ p) ↔ (p → q) :=
+by rw [and_comm, iff_self_and]
+
 @[simp] lemma and.congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
 ⟨λ h ha, by simp [ha] at h; exact h, and_congr_right⟩