[Merged by Bors] - chore: unsimp Set.coe_setOf

Archive/Imo/Imo1987Q1.lean

@@ -44,9 +44,10 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]
-  have (x : _) : ({x}ᶜ : Set α) = Finset.filter (· ≠ x) Finset.univ := by
+  have h (x : α) : ({x}ᶜ : Set α) = Finset.univ.erase x := by
     ext; simp
-  simp [this]
+  simp_rw [h, Fintype.card_subtype, SetLike.mem_coe, Finset.filter_univ_mem]
+  simp
 
 /-- Given `α : Type*` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
 fixed points. -/

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -625,12 +625,10 @@ identify to subsets of `Fin (n + 1)` of cardinality `d + 1`. -/
     (Δ[n] : SSet.{u}).nonDegenerate d ≃ { S : Finset (Fin (n + 1)) | S.card = d + 1 } :=
   Equiv.ofBijective _ (bijective_image_objEquiv_toOrderHom_univ n d)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma nonDegenerateEquiv'_iff {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) (j : Fin (n + 1)) :
     j ∈ (nonDegenerateEquiv' x).val ↔ ∃ (i : Fin (d + 1)), x.val i = j := by
-  simp only [Set.mem_setOf_eq, Set.coe_setOf]
-  dsimp [nonDegenerateEquiv']
-  aesop
+  unfold nonDegenerateEquiv'
+  simp
 
 set_option backward.defeqAttrib.useBackward true in
 /-- If `x` is a nondegenerate `d`-simplex of `Δ[n]`, this is the order isomorphism

Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

@@ -40,7 +40,8 @@ set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem range_arcsin : range arcsin = Icc (-(π / 2)) (π / 2) := by
   rw [arcsin, range_comp Subtype.val]
-  simp [Icc]
+  ext
+  simp
 
 theorem arcsin_le_pi_div_two (x : ℝ) : arcsin x ≤ π / 2 :=
   (arcsin_mem_Icc x).2

Mathlib/CategoryTheory/GradedObject/Monoidal.lean

@@ -610,8 +610,8 @@ instance (n : ℕ) : Finite ({ i : (ℕ × ℕ × ℕ) | i.1 + i.2.1 + i.2.2 = n
   refine Finite.of_injective (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ =>
     (⟨⟨i₁, by lia⟩, ⟨i₂, by lia⟩, ⟨i₃, by lia⟩⟩ :
       Fin (n + 1) × Fin (n + 1) × Fin (n + 1))) ?_
-  rintro ⟨⟨_, _, _⟩, _⟩ ⟨⟨_, _, _⟩, _⟩ h
-  simpa using h
+  intro _ _ h
+  exact Subtype.ext (congrArg (fun x => (x.1.1, x.2.1.1, x.2.2.1)) h)
 
 /-!
 The monoidal category structure on `GradedObject ℕ C` can be inferred

Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

@@ -107,7 +107,7 @@ theorem EqualizerCondition.bijective_mapToEqualizer_pullback' {P : Cᵒᵖ ⥤ T
     simpa [mapToEqualizer] using! ha₁
   · intro y h
     apply ha₂ y
-    simpa [mapToEqualizer, Subtype.ext_iff] using! h
+    simpa [mapToEqualizer] using Subtype.ext_iff.1 h
 
 theorem EqualizerCondition.bijective_mapToEqualizer_pullback {P : Cᵒᵖ ⥤ Type*}
     (hP : EqualizerCondition P) {X B : C} (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π] :
@@ -126,10 +126,11 @@ theorem EqualizerCondition.mk' (P : Cᵒᵖ ⥤ Type*)
   intro b hb
   obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb⟩
   refine ⟨a, ?_, ?_⟩
-  · simpa [Subtype.ext_iff, mapToEqualizer] using! ha₁
+  · simpa [mapToEqualizer] using Subtype.ext_iff.1 ha₁
   · intro y h
     apply ha₂ y
-    simpa [mapToEqualizer, Subtype.ext_iff] using! h
+    ext
+    simpa [mapToEqualizer] using h
 
 set_option backward.isDefEq.respectTransparency false in
 theorem EqualizerCondition.mk (P : Cᵒᵖ ⥤ Type*)

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -557,7 +557,7 @@ theorem isSheafFor_iff_yonedaSheafCondition {P : Cᵒᵖ ⥤ Type v₁} :
   dsimp [functor]
   simp only [Subtype.forall, shrinkYonedaObjObjEquiv.forall_congr_left, Equiv.apply_symm_apply]
   congr!
-  simp [Equiv.subtypeEquiv]
+  simp
 
 /--
 If `P` is a sheaf for the sieve `S` on `X`, a natural transformation from `S` (viewed as a functor)

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -1440,7 +1440,7 @@ def shrinkFunctorUliftFunctorIso [LocallySmall.{w} C] [LocallySmall.{max w' w} C
     fun {U V} f ↦ by
       dsimp
       ext
-      dsimp [Equiv.subtypeEquiv]
+      dsimp [Equiv.subtypeEquiv_apply]
       rw [shrinkYonedaObjObjEquiv_obj_map, shrinkYonedaObjObjEquiv_symm_comp]
       simp
 
@@ -1459,7 +1459,7 @@ variable (S) in
 noncomputable def shrinkFunctorIsoFunctor : (shrinkFunctor.{v₁} S).toFunctor ≅ S.functor :=
   NatIso.ofComponents (fun Y ↦ Equiv.toIso <| Equiv.subtypeEquiv shrinkYonedaObjObjEquiv (by simp))
     fun {U V} f ↦ by
-      dsimp [Equiv.subtypeEquiv]
+      dsimp [Equiv.subtypeEquiv_apply]
       ext
       simp [shrinkYonedaObjObjEquiv_obj_map]
 

Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean

@@ -114,9 +114,9 @@ lemma ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :
      G'.oddComponents.ncard ≤ G.oddComponents.ncard := by
   have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
       {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by
-    refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
-    simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
-      using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
+    refine Set.nonempty_of_ncard_ne_zero fun h' ↦ Nat.not_odd_zero ?_
+    rw [← h']
+    exact (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
   let f : G'.oddComponents → G.oddComponents :=
     fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩
   refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_

Mathlib/Data/Set/Basic.lean

@@ -142,7 +142,6 @@ instance (s : Set α) : CoeTC s α := ⟨fun x => x.1⟩
 theorem Set.coe_eq_subtype (s : Set α) : ↥s = { x // x ∈ s } :=
   rfl
 
-@[simp]
 theorem Set.coe_setOf (p : α → Prop) : ↥{ x | p x } = { x // p x } :=
   rfl
 

Mathlib/Data/Set/Finite/Lattice.lean

@@ -269,7 +269,7 @@ variable {s t : Set α}
 theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) :
     (⋃ i, s i).Infinite :=
   fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype
-    (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦ hs (by simpa using h_eq)
+    (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun _ _ h_eq ↦ hs (Subtype.ext_iff.1 h_eq)
 
 theorem Infinite.biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite)
     (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite := by

Mathlib/FieldTheory/SeparablyGenerated.lean

@@ -64,19 +64,21 @@ theorem aeval_toPolynomialAdjoinImageCompl_eq_zero
   simp_rw [toPolynomialAdjoinImageCompl, ← AlgEquiv.coe_toAlgHom, ← AlgHom.comp_apply]
   congr; ext; aesop (add simp optionEquivLeft_X_some) (add simp optionEquivLeft_X_none)
 
-set_option backward.isDefEq.respectTransparency false in
 theorem irreducible_toPolynomialAdjoinImageCompl {F : MvPolynomial ι k} (hF : Irreducible F) (i : ι)
     (H : AlgebraicIndependent k fun x : {j | j ≠ i} ↦ a x) :
     Irreducible (toPolynomialAdjoinImageCompl F a i) := by
-  have : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp
-  delta toPolynomialAdjoinImageCompl
-  convert!
-    hF.map (renameEquiv k (Equiv.optionSubtypeNe i).symm) |>.map (optionEquivLeft k _) |>.map
-      (Polynomial.mapAlgEquiv
-        (H.aevalEquiv.trans (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $this.symm))))
-  rw [← AlgEquiv.coe_toAlgHom]
-  congr
-  aesop
+  classical
+  unfold toPolynomialAdjoinImageCompl
+  have hc : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp
+  let d : {j // j ≠ i} ≃ {j | j ≠ i} := .subtypeEquivRight (by simp)
+  refine (congrArg Irreducible ?_).mp <|
+    hF.map (renameEquiv k ((Equiv.optionSubtypeNe i).symm)) |>.map
+      (optionEquivLeft k _) |>.map (Polynomial.mapAlgEquiv <|
+        (renameEquiv k d).trans <| H.aevalEquiv.trans
+        (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $hc.symm)))
+  rw [Polynomial.coe_mapAlgEquiv, Polynomial.coe_mapAlgHom]
+  refine congrFun (congrArg Polynomial.map ?_) _
+  ext <;> simp [d]
 
 -- Suppose `F` has minimal total degree among the relations of `a`.
 variable {F : MvPolynomial ι k}

Mathlib/GroupTheory/Perm/Finite.lean

@@ -125,7 +125,6 @@ theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ :
     obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
     grind
 
-set_option backward.isDefEq.respectTransparency false in
 theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n]
     {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
     σ ∈ (sumCongrHom m n).range := by
@@ -143,14 +142,11 @@ theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finit
   rw [Perm.sumCongrHom_apply]
   ext (a | b)
   · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
-      apply_ofInjective_symm Sum.inl_injective]
-    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
-    dsimp [Set.range]
-    rw [subtypePerm_apply]
+      apply_ofInjective_symm Sum.inl_injective, ofInjective_apply]
+    rfl
   · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
       apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
-    dsimp [Set.range]
-    rw [subtypePerm_apply]
+    rfl
 
 nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
     orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=

Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

@@ -160,8 +160,8 @@ def ofBilinear [IsReflexive R M] (B : M →ₗ[R] M →ₗ[R] R) (hNB : LinearMa
       right_inv := by
         intro y
         simp [involutive_reflection (coroot_apply_self B x.2) y] }
-  reflectionPerm_root x y := by
-    simp [Module.reflection_apply]
+  reflectionPerm_root := by
+    simp [coe_setOf, Module.reflection_apply]
   reflectionPerm_coroot x y := by
     simp only [coe_setOf, mem_setOf_eq, Embedding.coeFn_mk, Embedding.subtype_apply,
       Dual.eval_apply, Equiv.coe_fn_mk]

Mathlib/NumberTheory/KummerDedekind.lean

@@ -205,8 +205,6 @@ theorem Ideal.irreducible_map_of_irreducible_minpoly (hI : IsMaximal I) (hI' : I
   rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
   exact normalizedFactors_irreducible hf
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 open Set Classical in
 /-- Let `Q` be a lift of factor of the minimal polynomial of `x`, a generator of `S` over `R`, taken
 `mod I`. Then (the reduction of) `Q` corresponds via
@@ -218,19 +216,19 @@ theorem normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span
     (hI' : I ≠ ⊥) (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
     ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨_, hQ⟩).val =
     span (I.map (algebraMap R S) ∪ {Q.aeval x}) := by
-  dsimp [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk,
-    Ideal.normalizedFactorsEquivSpanNormalizedFactors]
-  rw [IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm]
-  dsimp [IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv,
-    IsDedekindDomain.idealFactorsEquivOfQuotEquiv, OrderIso.ofHomInv]
-  simp only [map_span, image_singleton, coe_coe, quotMapEquivQuotQuotMap_symm_apply hx hx' Q]
-  refine le_antisymm (fun a ha ↦ ?_) (span_le.mpr <| union_subset_iff.mpr <|
-    ⟨le_comap_of_map_le (by simp), by simp⟩)
-  rw [mem_comap, Ideal.mem_span_singleton] at ha
-  obtain ⟨a', ha'⟩ := ha
-  obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a'
-  rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'
-  rw [union_comm, span_union, span_eq, mem_span_singleton_sup]
-  exact ⟨b, a - Q.aeval x * b, ha', by ring⟩
+  unfold normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
+    Ideal.normalizedFactorsEquivSpanNormalizedFactors
+  rw [Equiv.symm_trans_apply, IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm]
+  unfold IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv
+  rw [Equiv.coe_fn_mk, Equiv.symm_symm, Equiv.ofBijective_apply]
+  dsimp only
+  unfold IsDedekindDomain.idealFactorsEquivOfQuotEquiv
+  rw [OrderIso.ofHomInv_apply]
+  erw [IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe]
+  dsimp only
+  rw [map_span, image_singleton, map_span, image_singleton, coe_coe,
+    quotMapEquivQuotQuotMap_symm_apply, span_union, span_eq, sup_comm,
+    ← image_singleton, ← map_span, Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective,
+    Ideal.mk_ker]
 
 end KummerDedekind

Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

@@ -744,7 +744,7 @@ def normalizedFactorsEquivOfQuotEquiv (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
         idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI
           j.prop⟩
   left_inv := fun ⟨j, hj⟩ => by simp
-  right_inv := fun ⟨j, hj⟩ => by simp [-Set.coe_setOf]
+  right_inv := fun ⟨j, hj⟩ => by simp
 
 @[deprecated (since := "2026-04-16")]
 alias _root_.normalizedFactorsEquivOfQuotEquiv := normalizedFactorsEquivOfQuotEquiv