chore(*): reduce defeq abuse of Set α = α → Prop (leanprover-community#39019)

Author: urkud

Mathlib/Analysis/Complex/CoveringMap.lean

@@ -89,7 +89,7 @@ theorem isCoveringMapOn_zpow (n : ℤ) (hn : (n : 𝕜) ≠ 0) :
   refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
   · convert isClosed_singleton (x := (0 : 𝕜)).isOpen_compl using 1
     ext; simp [this]
-  · convert (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
+  · convert (isCoveringMap_zpow n hn).comp_homeomorph (.ofEqSubtypes _) using 1
     ext; simpa using (this _).not
 
 attribute [-instance] Units.mulAction'
@@ -103,9 +103,9 @@ theorem isQuotientCoveringMap_npow (n : ℕ) (hn : (n : 𝕜) ≠ 0)
     (by fun_prop) (.restrictPreimage _ surj)
   have : IsQuotientMap fun x : 𝕜ˣ ↦ x ^ n := by
     let e := unitsHomeomorphNeZero (G₀ := 𝕜)
-    convert (e.symm.isQuotientMap.comp this).comp (e.trans (.setCongr _)).isQuotientMap
+    convert (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
     · exact (e.left_inv _).symm
-    · ext; simp [NeZero.ne]; rfl
+    · ext; simp [NeZero.ne]
   refine this.isQuotientCoveringMap_of_subgroup _
     (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_
   simp [mul_pow, mul_inv_eq_one, eq_comm]

Mathlib/Analysis/Normed/Group/FunctionSeries.lean

@@ -74,7 +74,7 @@ theorem tendstoUniformlyOn_tsum_of_cofinite_eventually {ι : Type*} {f : ι →
   apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
   apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
   apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
-  simp only [comp_apply, Subtype.forall, imp_false]
+  simp only [comp_apply, Subtype.forall]
   apply fun i hi => HN i ?_ x hx
   have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
   simp_all

Mathlib/Data/Nat/Order/Lemmas.lean

@@ -30,8 +30,8 @@ instance Subtype.orderBot (s : Set ℕ) [DecidablePred (· ∈ s)] [h : Nonempty
   bot := ⟨Nat.find (nonempty_subtype.1 h), Nat.find_spec (nonempty_subtype.1 h)⟩
   bot_le x := Nat.find_min' _ x.2
 
-instance Subtype.semilatticeSup (s : Set ℕ) : SemilatticeSup s :=
-  { Subtype.instLinearOrder (· ∈ s), LinearOrder.toLattice with }
+instance Subtype.semilatticeSup (p : ℕ → Prop) : SemilatticeSup (Subtype p) :=
+  { Subtype.instLinearOrder p, LinearOrder.toLattice with }
 
 theorem Subtype.coe_bot {s : Set ℕ} [DecidablePred (· ∈ s)] [h : Nonempty s] :
     ((⊥ : s) : ℕ) = Nat.find (nonempty_subtype.1 h) :=

Mathlib/NumberTheory/EulerProduct/ExpLog.lean

@@ -41,8 +41,8 @@ theorem exp_tsum_primes_log_eq_tsum {f : ℕ →*₀ ℂ} (hsum : Summable (‖f
   have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
   have hp (p : Nat.Primes) : 1 - f p ≠ 0 :=
     fun h ↦ (norm_one (α := ℂ) ▸ (sub_eq_zero.mp h) ▸ hs p.prop.one_lt).false
-  have H := hsum.of_norm.clog_one_sub.neg.subtype {p | p.Prime} |>.hasSum.cexp.tprod_eq
-  simp only [Set.coe_setOf, Set.mem_setOf_eq, Function.comp_apply, exp_neg, exp_log (hp _)] at H
+  have H := hsum.of_norm.clog_one_sub.neg.subtype Nat.Prime |>.hasSum.cexp.tprod_eq
+  simp only [Function.comp_apply, exp_neg, exp_log (hp _)] at H
   exact H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum
 
 end EulerProduct

Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

@@ -58,7 +58,7 @@ private def tendsto_norm_le_and_mk_eq_div_atTop_aux₂ :
       (ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) (toMixed K).toLinearMap))
         ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ s} := by
   rw [ZLattice.coe_comap]
-  refine (((toMixed K).toEquiv.image _).trans (Equiv.setCongr ?_)).trans
+  refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
     (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm
   ext
   simp_rw [mem_idealSet, Set.mem_image, Set.mem_inter_iff, Set.mem_preimage, SetLike.mem_coe,

Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

@@ -181,7 +181,7 @@ theorem primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬ p ∣ exponent θ
         inferInstance (by simp [NeZero.ne p]) (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral).symm
         ⟨Q.map (Int.quotientSpanNatEquivZMod p).symm, by
           rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
-          exact ((primesOverSpanEquivMonicFactorsModAux _).symm ⟨Q, hQ⟩).coe_prop⟩ := rfl
+          exact ((primesOverSpanEquivMonicFactorsModAux _).symm ⟨Q, hQ⟩).prop⟩ := rfl
 
 /--
 The ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via

Mathlib/Topology/Algebra/InfiniteSum/Group.lean

@@ -297,18 +297,19 @@ theorem Multipliable.comp_injective {i : γ → β} (hf : Multipliable f) (hi :
     (hf.mulIndicator (Set.range i))
 
 @[to_additive]
-theorem Multipliable.subtype (hf : Multipliable f) (s : Set β) : Multipliable (f ∘ (↑) : s → α) :=
+theorem Multipliable.subtype (hf : Multipliable f) (p : β → Prop) :
+    Multipliable (f ∘ (↑) : Subtype p → α) :=
   hf.comp_injective Subtype.coe_injective
 
 @[to_additive]
 theorem multipliable_subtype_and_compl {s : Set β} :
     ((Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ f x) ↔ Multipliable f :=
-  ⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype s, h.subtype sᶜ⟩⟩
+  ⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype (· ∈ s), h.subtype (· ∈ sᶜ)⟩⟩
 
 @[to_additive]
 protected theorem Multipliable.tprod_subtype_mul_tprod_subtype_compl [T2Space α] {f : β → α}
     (hf : Multipliable f) (s : Set β) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x :=
-  ((hf.subtype s).hasProd.mul_compl (hf.subtype { x | x ∉ s }).hasProd).unique hf.hasProd
+  ((hf.subtype _).hasProd.mul_compl (hf.subtype _).hasProd).unique hf.hasProd
 
 @[to_additive]
 protected theorem Multipliable.prod_mul_tprod_subtype_compl [T2Space α] {f : β → α}
@@ -352,8 +353,8 @@ theorem tendsto_tprod_compl_atTop_one (f : α → G) :
   by_cases H : Multipliable f
   · intro e he
     obtain ⟨s, hs⟩ := H.tprod_vanishing he
-    rw [Filter.mem_map, mem_atTop_sets]
-    exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
+    simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]
+    exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
   · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
     rwa [Finset.multipliable_compl_iff]
 

Mathlib/Topology/FiberBundle/Basic.lean

@@ -276,7 +276,7 @@ theorem totalSpaceMk_isClosedEmbedding [T1Space B] (x : B) :
 This is useful to transfer topological properties of the model fiber. -/
 noncomputable def homeomorphAt (b : B) : E b ≃ₜ F :=
   ((totalSpaceMk_isEmbedding F E b).toHomeomorph.trans <|
-    Homeomorph.ofEqSubtypes <| TotalSpace.range_mk b).trans <|
+    Homeomorph.setCongr <| TotalSpace.range_mk b).trans <|
     (trivializationAt F E b).preimageSingletonHomeomorph <| mem_baseSet_trivializationAt' b
 
 lemma t0Space [T0Space F] (b : B) : T0Space (E b) :=