perf: add another dsimp into If.lean

leanprover · Jun 25, 2024 · f4033ce · f4033ce
1 parent be4fb62
commit f4033ce
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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