[Merged by Bors] - fix(Data/Set/Image): simp confluence issues with image_subset_iff

Mathlib/Data/Fintype/Basic.lean

@@ -140,6 +140,10 @@ theorem ssubset_univ_iff {s : Finset α} : s ⊂ univ ↔ s ≠ univ :=
   @lt_top_iff_ne_top _ _ _ s
 #align finset.ssubset_univ_iff Finset.ssubset_univ_iff
 
+@[simp]
+theorem univ_subset_iff {s : Finset α} : univ ⊆ s ↔ s = univ :=
+  @top_le_iff _ _ _ s
+
 theorem codisjoint_left : Codisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t := by
   classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]
 #align finset.codisjoint_left Finset.codisjoint_left

Mathlib/Data/Set/Basic.lean

@@ -654,6 +654,7 @@ theorem empty_ne_univ [Nonempty α] : (∅ : Set α) ≠ univ := fun e =>
 theorem subset_univ (s : Set α) : s ⊆ univ := fun _ _ => trivial
 #align set.subset_univ Set.subset_univ
 
+@[simp]
 theorem univ_subset_iff {s : Set α} : univ ⊆ s ↔ s = univ :=
   @top_le_iff _ _ _ s
 #align set.univ_subset_iff Set.univ_subset_iff

Mathlib/Data/Set/Image.lean

@@ -510,6 +510,11 @@ theorem image_preimage_eq {f : α → β} (s : Set β) (h : Surjective f) : f ''
     ⟨y, (e.symm ▸ hx : f y ∈ s), e⟩
 #align set.image_preimage_eq Set.image_preimage_eq
 
+@[simp]
+theorem Nonempty.subset_preimage_const {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) :
+    s ⊆ (fun _ => a) ⁻¹' t ↔ a ∈ t := by
+  rw [← image_subset_iff, hs.image_const, singleton_subset_iff]
+
 @[simp]
 theorem preimage_eq_preimage {f : β → α} (hf : Surjective f) : f ⁻¹' s = f ⁻¹' t ↔ s = t :=
   Iff.intro
@@ -687,12 +692,20 @@ theorem range_iff_surjective : range f = univ ↔ Surjective f :=
 alias ⟨_, _root_.Function.Surjective.range_eq⟩ := range_iff_surjective
 #align function.surjective.range_eq Function.Surjective.range_eq
 
+@[simp]
+theorem subset_range_of_surjective {f : α → β} (h : Surjective f) (s : Set β) :
+    s ⊆ range f := Surjective.range_eq h ▸ subset_univ s
+
 @[simp]
 theorem image_univ {f : α → β} : f '' univ = range f := by
   ext
   simp [image, range]
 #align set.image_univ Set.image_univ
 
+@[simp]
+theorem preimage_eq_univ_iff {f : α → β} {s} : f ⁻¹' s = univ ↔ range f ⊆ s := by
+  rw [← univ_subset_iff, ← image_subset_iff, image_univ]
+
 theorem image_subset_range (f : α → β) (s) : f '' s ⊆ range f := by
   rw [← image_univ]; exact image_subset _ (subset_univ _)
 #align set.image_subset_range Set.image_subset_range
@@ -806,6 +819,7 @@ theorem forall_subset_range_iff {f : α → β} {p : Set β → Prop} :
     (∀ s, s ⊆ range f → p s) ↔ ∀ s, p (f '' s) := by
   rw [← forall_range_iff, range_image]; rfl
 
+@[simp]
 theorem preimage_subset_preimage_iff {s t : Set α} {f : β → α} (hs : s ⊆ range f) :
     f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t := by
   constructor

Mathlib/Logic/Equiv/Set.lean

@@ -118,7 +118,6 @@ theorem preimage_symm_preimage {α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (
   e.leftInverse_symm.preimage_preimage s
 #align equiv.preimage_symm_preimage Equiv.preimage_symm_preimage
 
-@[simp]
 theorem preimage_subset {α β} (e : α ≃ β) (s t : Set β) : e ⁻¹' s ⊆ e ⁻¹' t ↔ s ⊆ t :=
   e.surjective.preimage_subset_preimage_iff
 #align equiv.preimage_subset Equiv.preimage_subset

test/simp_confluence.lean

@@ -0,0 +1,41 @@
+import Mathlib
+
+namespace Set
+
+open Function
+
+variable {α β : Type*}
+
+/-- Without `subset_range_of_surjective`, `image_subset_iff` and `image_preimage_eq` create a simp
+  confluence issue. -/
+example {f : α → β} (s t : Set β) (h : Surjective f) :
+    f '' (f ⁻¹' s) ⊆ t ↔ f '' (f ⁻¹' s) ⊆ t := by
+  conv =>
+    congr
+    · simp [h, -image_preimage_eq, -subset_range_of_surjective]
+    · simp [h, -image_subset_iff, -subset_range_of_surjective]
+  fail_if_success simp [h, -subset_range_of_surjective]
+  simp [h]
+
+/-- Without `Nonempty.subset_preimage_const`, `image_subset_iff` and `Nonempty.image_const` create a
+  simp confluence issue. -/
+example {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) :
+    (fun _ => a) '' s ⊆ t ↔ (fun _ => a) '' s ⊆ t := by
+  conv =>
+    congr
+    · simp [hs, -Nonempty.image_const, -Nonempty.subset_preimage_const]
+    · simp [hs, -image_subset_iff, -Nonempty.subset_preimage_const]
+  fail_if_success simp [hs, -Nonempty.subset_preimage_const]
+  simp [hs]
+
+/-- Without `preimage_eq_univ_iff`, `image_subset_iff` and `image_univ` create a
+  simp confluence issue. -/
+example {f : α → β} (s) : f '' univ ⊆ s ↔ f '' univ ⊆ s := by
+  conv =>
+    congr
+    · simp [-image_univ, -preimage_eq_univ_iff]
+    · simp [-image_subset_iff, -preimage_eq_univ_iff]
+  fail_if_success simp [-preimage_eq_univ_iff]
+  simp
+
+end Set