diff --git a/src/data/ordmap/ordset.lean b/src/data/ordmap/ordset.lean
index 11a26a5381ace..c7c9536d551ef 100644
--- a/src/data/ordmap/ordset.lean
+++ 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)
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 7d8a1255931ab..9da84ec02e82c 100644
--- a/src/logic/basic.lean
+++ b/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). -/