diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 9b961cbfa8..e927945b19 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -197,13 +197,13 @@ instance : LawfulBEq Bool where
   eq_of_beq {a b} h := by cases a <;> cases b <;> first | rfl | contradiction
   rfl {a} := by cases a <;> decide
 
-instance : LawfulBEq Char where
-  eq_of_beq h := of_decide_eq_true h
-  rfl {a} := of_decide_eq_self_eq_true a
+instance [DecidableEq α] : LawfulBEq α where
+  eq_of_beq := of_decide_eq_true
+  rfl := of_decide_eq_self_eq_true _
 
-instance : LawfulBEq String where
-  eq_of_beq h := of_decide_eq_true h
-  rfl {a} := of_decide_eq_self_eq_true a
+instance : LawfulBEq Char := inferInstance
+
+instance : LawfulBEq String := inferInstance
 
 /- Logical connectives an equality -/
 
@@ -356,6 +356,9 @@ theorem Iff.symm (h : a ↔ b) : b ↔ a :=
 theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
   Iff.intro Iff.symm Iff.symm
 
+theorem And.comm : a ∧ b ↔ b ∧ a := by
+  constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
+
 /- Exists -/
 
 theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
@@ -736,6 +739,9 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
+@[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
+  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
+
 /- Quotients -/
 
 -- Iff can now be used to do substitutions in a calculation
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index b5bd23e528..a1828dd339 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -561,9 +561,9 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
       cases bs with
       | nil => intro h; contradiction
       | cons b bs =>
-        simp [BEq.beq, List.beq]
+        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl]
         intro ⟨h₁, h₂⟩
-        exact ⟨eq_of_beq h₁, ih h₂⟩
+        exact ⟨h₁, ih h₂⟩
   rfl {as} := by
     induction as with
     | nil => rfl
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index 9210b007a2..b00538b402 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -180,7 +180,7 @@ instance : LawfulBEq PolyCnstr where
     have h : eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ := h
     simp at h
     have ⟨⟨h₁, h₂⟩, h₃⟩ := h
-    rw [h₁, eq_of_beq h₂, eq_of_beq h₃]
+    rw [h₁, h₂, h₃]
   rfl {a} := by
     cases a; rename_i eq lhs rhs
     show (eq == eq && lhs == lhs && rhs == rhs) = true
diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean
index 976d61ec01..fd1b3814cf 100644
--- a/src/Init/Data/Prod.lean
+++ b/src/Init/Data/Prod.lean
@@ -7,5 +7,7 @@ prelude
 import Init.SimpLemmas
 
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
-  eq_of_beq {a b} h := by cases a; cases b; simp [BEq.beq] at h; have ⟨h₁, h₂⟩ := h; rw [eq_of_beq h₁, eq_of_beq h₂]
+  eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
+    cases a; cases b
+    refine congr (congrArg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
   rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]
diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out
index 188f4363d6..414115551d 100644
--- a/tests/lean/interactive/completion7.lean.expected.out
+++ b/tests/lean/interactive/completion7.lean.expected.out
@@ -52,7 +52,8 @@
 {"textDocument": {"uri": "file://completion7.lean"},
  "position": {"line": 2, "character": 11}}
 {"items":
- [{"label": "intro", "kind": 4, "detail": "a → b → a ∧ b"},
+ [{"label": "comm", "kind": 3, "detail": "a ∧ b ↔ b ∧ a"},
+  {"label": "intro", "kind": 4, "detail": "a → b → a ∧ b"},
   {"label": "left", "kind": 5, "detail": "a ∧ b → a"},
   {"label": "right", "kind": 5, "detail": "a ∧ b → b"}],
  "isIncomplete": true}