diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 4d4884b00..3662fcbef 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -20,6 +20,8 @@ jobs:
       - uses: actions/checkout@v4
       - name: Test documentation checker
         run: python3 -m unittest discover -s scripts -p 'test_*.py'
+      - name: "Source hygiene"
+        run: python3 -B scripts/check_hygiene.py --check-simp
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail --iofail @complexitylib @mathlib/mk_all @/checkInitImports @mathlib/lint-style"
diff --git a/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean b/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
index 35587403f..7e29266cb 100644
--- a/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
+++ b/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
@@ -124,7 +124,10 @@ def step (k distance : ℕ) : Circuit signature (k + k) (k + k) :=
     (Circuit.pi fun i => (propagateFormula k distance i).toCircuit)
 
 @[simp] theorem size_step (k distance : ℕ) : (step k distance).size = 3 * k := by
-  simp [step, generateFormula, propagateFormula, Formula.size_toCircuit]
+  simp only [step, generateFormula, Fin.natAdd_eq_addNat, propagateFormula, Circuit.size_append,
+    Circuit.size_pi, Formula.size_toCircuit, Formula.size_or, Formula.size_input, Formula.size_and,
+    add_zero, zero_add, Nat.reduceAdd, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
+    smul_eq_mul, mul_one]
   omega
 
 theorem depth_step_le (k distance : ℕ) : (step k distance).depth ≤ 2 := by