Skip to content

Commit 58f09da

Browse files
committed
refactor(Order/Interval/Set/LinearOrder): golf Ioi_diff_Ioc using grind
1 parent c616426 commit 58f09da

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Order/Interval/Set/LinearOrder.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -561,7 +561,7 @@ theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by
561561

562562
@[simp]
563563
theorem Ioi_diff_Ioc : Ioi a \ Ioc a b = Ioi (max a b) := by
564-
simp [diff_eq, compl_Ioc, inter_union_distrib_left, Ioi_inter_Iic, Ioi_inter_Ioi]
564+
grind
565565

566566
theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a := by
567567
grind

0 commit comments

Comments
 (0)