From f4033cecada13056047fbf1f42f6af0ad8488d45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 25 Jun 2024 11:27:29 +0200
Subject: [PATCH] perf: add another dsimp into If.lean

---
 LeanSAT/AIG/If.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/LeanSAT/AIG/If.lean b/LeanSAT/AIG/If.lean
index a25d3eb3..cbfc5ff8 100644
--- a/LeanSAT/AIG/If.lean
+++ b/LeanSAT/AIG/If.lean
@@ -63,6 +63,7 @@ theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
     if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧ := by
   rw [if_as_bool]
   unfold mkIfCached
+  dsimp
   simp only [TernaryInput.cast, Ref_cast', id_eq, Int.reduceNeg, denote_mkOrCached,
     denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
   congr 2