Skip to content

Commit b49055f

Browse files
committed
address feedback
1 parent 65583c4 commit b49055f

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

src/Std/Sat/AIG/Lemmas.lean

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -276,9 +276,7 @@ theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
276276
. intro a heq
277277
simp only [denote_idx_atom heq]
278278
apply h
279-
rw [mem_def]
280-
rw [← heq]
281-
rw [Array.mem_def]
279+
rw [mem_def, ← heq, Array.mem_def]
282280
apply Array.getElem_mem_data
283281
. intro lhs rhs linv rinv heq
284282
simp only [denote_idx_gate heq]

0 commit comments

Comments
 (0)