From ea75c924a1ab4bb25f4d2e144a141f899da7ba32 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 24 Sep 2024 16:36:00 -0700 Subject: [PATCH] feat: add `heq_comm` (#5456) Requested [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/heq_comm/near/472516757). --- src/Init/Core.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 28eda9455c..c10db7aab2 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -837,6 +837,9 @@ instance : Trans Iff Iff Iff where theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm +theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm +theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm + @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm