Skip to content

Commit f768b2c

Browse files
committed
fix: Data.Finset.Basic Change statement of two simp lemmas so they can be used with rw (#1615)
1 parent 6fe10b8 commit f768b2c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Mathlib/Data/Finset/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1298,12 +1298,12 @@ instance : Lattice (Finset α) :=
12981298
inf_le_right := fun _ _ _ h => (mem_ndinter.1 h).2 }
12991299

13001300
@[simp]
1301-
theorem sup_eq_union : ((· ⊔ ·) : Finset α → Finset α → Finset α) = (· ∪ ·) :=
1301+
theorem sup_eq_union : (HasSup.sup : Finset α → Finset α → Finset α) = Union.union :=
13021302
rfl
13031303
#align finset.sup_eq_union Finset.sup_eq_union
13041304

13051305
@[simp]
1306-
theorem inf_eq_inter : ((· ⊓ ·) : Finset α → Finset α → Finset α) = (· ∩ ·) :=
1306+
theorem inf_eq_inter : (HasInf.inf : Finset α → Finset α → Finset α) = Inter.inter :=
13071307
rfl
13081308
#align finset.inf_eq_inter Finset.inf_eq_inter
13091309

0 commit comments

Comments
 (0)