chore(logic/basic): +2 simp lemmas (#5500)

* simplify `a ∨ b ↔ a` to `b → a`;
* simplify `a ∨ b ↔ b` to `a → b`.

src/data/ordmap/ordset.lean

@@ -155,7 +155,7 @@ theorem balanced_sz.symm {l r : ℕ} : balanced_sz l r → balanced_sz r l :=
 or.imp (by rw add_comm; exact id) and.symm
 
 theorem balanced_sz_zero {l : ℕ} : balanced_sz l 0 ↔ l ≤ 1 :=
-by simp [balanced_sz]; apply or_iff_left_of_imp; rintro rfl; exact zero_le_one
+by simp [balanced_sz] { contextual := tt }
 
 theorem balanced_sz_up {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂)
   (h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l)

src/logic/basic.lean

@@ -383,6 +383,12 @@ protected theorem decidable.not_imp_not [decidable a] : (¬ a → ¬ b) ↔ (b 
 
 theorem not_imp_not : (¬ a → ¬ b) ↔ (b → a) := decidable.not_imp_not
 
+@[simp] theorem or_iff_left_iff_imp : (a ∨ b ↔ a) ↔ (b → a) :=
+⟨λ h hb, h.1 (or.inr hb), or_iff_left_of_imp⟩
+
+@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) :=
+by rw [or_comm, or_iff_left_iff_imp]
+
 /-! ### Declarations about distributivity -/
 
 /-- `∧` distributes over `∨` (on the left). -/