diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 7827cea112302..aafa4ca011c68 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -806,12 +806,12 @@ theorem union_right_comm (s₁ s₂ s₃ : Set α) : s₁ ∪ s₂ ∪ s₃ = s @[simp] theorem union_eq_left {s t : Set α} : s ∪ t = s ↔ t ⊆ s := sup_eq_left -#align set.union_eq_left Set.union_eq_left +#align set.union_eq_left_iff_subset Set.union_eq_left @[simp] theorem union_eq_right {s t : Set α} : s ∪ t = t ↔ s ⊆ t := sup_eq_right -#align set.union_eq_right Set.union_eq_right +#align set.union_eq_right_iff_subset Set.union_eq_right theorem union_eq_self_of_subset_left {s t : Set α} (h : s ⊆ t) : s ∪ t = t := union_eq_right.mpr h