From 5d84aebeb9c7bf683c16bf46f28fa526fed7bb0b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 26 Aug 2024 13:04:53 +1000
Subject: [PATCH] feat: lemmas about `Function.comp` that help confluence
 (#5162)

---
 src/Init/Core.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a3b2fec75e..fb2a781754 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -36,6 +36,17 @@ and `flip (·<·)` is the greater-than relation.
 
 theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x) := rfl
 
+@[simp] theorem Function.const_comp {f : α → β} {c : γ} :
+    (Function.const β c ∘ f) = Function.const α c := by
+  rfl
+@[simp] theorem Function.comp_const {f : β → γ} {b : β} :
+    (f ∘ Function.const α b) = Function.const α (f b) := by
+  rfl
+@[simp] theorem Function.true_comp {f : α → β} : ((fun _ => true) ∘ f) = fun _ => true := by
+  rfl
+@[simp] theorem Function.false_comp {f : α → β} : ((fun _ => false) ∘ f) = fun _ => false := by
+  rfl
+
 attribute [simp] namedPattern
 
 /--