chore(Finset/Lattice): add simp to sup_image/inf_image (#9340)

leanprover-community · Jan 6, 2024 · a2b7daf · a2b7daf
1 parent 87ffb36
commit a2b7daf
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
@@ -60,6 +60,7 @@ theorem sup_insert [DecidableEq β] {b : β} : (insert b s : Finset β).sup f =
   fold_insert_idem
 #align finset.sup_insert Finset.sup_insert
 
+@[simp]
 theorem sup_image [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) :
     (s.image f).sup g = s.sup (g ∘ f) :=
   fold_image_idem
@@ -341,6 +342,7 @@ theorem inf_insert [DecidableEq β] {b : β} : (insert b s : Finset β).inf f =
   fold_insert_idem
 #align finset.inf_insert Finset.inf_insert
 
+@[simp]
 theorem inf_image [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) :
     (s.image f).inf g = s.inf (g ∘ f) :=
   fold_image_idem