chore: cleanup imports in Archive/IfNormalization (#21318)

leanprover-community · Feb 1, 2025 · 213a36c · 213a36c
1 parent 81a72b9
commit 213a36c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 5 deletions.
diff --git a/Archive/Examples/IfNormalization/Result.lean b/Archive/Examples/IfNormalization/Result.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Archive.Examples.IfNormalization.Statement
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 import Mathlib.Tactic.Recall
 

diff --git a/Archive/Examples/IfNormalization/WithoutAesop.lean b/Archive/Examples/IfNormalization/WithoutAesop.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Kim Morrison
 -/
 import Archive.Examples.IfNormalization.Statement
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 
 /-!
@@ -20,7 +18,7 @@ we put primes on the declarations in the file.)
 namespace IfExpr
 
 attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
-  List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
+  List.disjoint
 
 theorem eval_ite_ite' {a b c d e : IfExpr} {f : ℕ → Bool} :
     (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by