chore: address more adaptation notes from leanprover/lean4#5020 (#16528)

We make miscellaneous changes to either remove or clarify `adaptation_notes` coming from leanprover/lean4#5020.



Co-authored-by: Kim Morrison <[email protected]>

Mathlib/Algebra/Group/Subgroup/MulOpposite.lean

@@ -28,8 +28,11 @@ protected def op (H : Subgroup G) : Subgroup Gᵐᵒᵖ where
   mul_mem' ha hb := H.mul_mem hb ha
   inv_mem' := H.inv_mem
 
-#adaptation_note /-- After lean4#5020, some instances need to be copied to obtain the correct
-discrimination tree key. -/
+/- We redeclare this instance to get keys
+`SMul (@Subtype (MulOpposite _) (@Membership.mem (MulOpposite _)
+  (Subgroup (MulOpposite _) _) _ (@Subgroup.op _ _ _))) _`
+compared to the keys for `Submonoid.smul`
+`SMul (@Subtype _ (@Membership.mem _ (Submonoid _ _) _ _)) _` -/
 @[to_additive] instance instSMul (H : Subgroup G) : SMul H.op G := Submonoid.smul ..
 
 @[to_additive (attr := simp)]

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -200,8 +200,10 @@ lemma even_card_of_isPerfectMatching [DecidableEq V] [DecidableRel G.Adj]
     Even (Fintype.card c.supp) := by
   #adaptation_note
   /--
-  After lean4#5020, many instances for Lie algebras and manifolds are no longer found.
-  See https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/.2316244.20adaptations.20for.20nightly-2024-08-28/near/466219124
+  After lean4#5020, some instances that use the chain of coercions
+  `[SetLike X], X → Set α → Sort _` are
+  blocked by the discrimination tree. This can be fixed by redeclaring the instance for `X`
+  using the double coercion but the proper fix seems to avoid the double coercion.
   -/
   letI : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
   simpa using (hM.induce_connectedComponent_isMatching c).even_card

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -109,13 +109,7 @@ theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fint
   use x
   rw [← Set.range_iff_surjective, ← coe_zpowers]
   rw [← Fintype.card_congr (Equiv.Set.univ α), ← Fintype.card_zpowers] at hx
-  #adaptation_note
-  /--
-  After lean4#5020, many instances for Lie algebras and manifolds are no longer found.
-  See https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/.2316244.20adaptations.20for.20nightly-2024-08-28/near/466219124
-  -/
-  letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
-  exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
+  convert Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
 @[deprecated (since := "2024-02-21")]
 alias isAddCyclic_of_orderOf_eq_card := isAddCyclic_of_addOrderOf_eq_card
 

Mathlib/ModelTheory/PartialEquiv.lean

@@ -347,8 +347,8 @@ lemma partialEquivLimit_comp_inclusion {i : ι} :
 
 theorem le_partialEquivLimit (i : ι) : S i ≤ partialEquivLimit S :=
   ⟨le_iSup (f := fun i ↦ (S i).dom) _, by
-    #adaptation_note /-- After lean4#5020, `simp` can no longer apply this lemma here. -/
-    rw [partialEquivLimit_comp_inclusion]
+    #adaptation_note /-- After lean4#5020, these two `simp` calls cannot be combined. -/
+    simp only [partialEquivLimit_comp_inclusion]
     simp only [cod_partialEquivLimit, dom_partialEquivLimit, ← Embedding.comp_assoc,
       subtype_comp_inclusion]⟩
 

Mathlib/Topology/MetricSpace/Polish.lean

@@ -256,6 +256,8 @@ theorem dist_val_le_dist (x y : CompleteCopy s) : dist x.1 y.1 ≤ dist x y :=
   le_add_of_nonneg_right (abs_nonneg _)
 
 instance : TopologicalSpace (CompleteCopy s) := inferInstanceAs (TopologicalSpace s)
+instance [SecondCountableTopology α] : SecondCountableTopology (CompleteCopy s) :=
+  inferInstanceAs (SecondCountableTopology s)
 instance : T0Space (CompleteCopy s) := inferInstanceAs (T0Space s)
 
 /-- A metric space structure on a subset `s` of a metric space, designed to make it complete
@@ -329,10 +331,6 @@ theorem _root_.IsOpen.polishSpace {α : Type*} [TopologicalSpace α] [PolishSpac
     (hs : IsOpen s) : PolishSpace s := by
   letI := upgradePolishSpace α
   lift s to Opens α using hs
-  #adaptation_note /-- After lean4#5020, many instances for Lie algebras and manifolds are no
-  longer found. -/
-  have : SecondCountableTopology s.CompleteCopy :=
-    TopologicalSpace.Subtype.secondCountableTopology _
   exact inferInstanceAs (PolishSpace s.CompleteCopy)
 
 end CompleteCopy

Mathlib/Topology/Sets/Opens.lean

@@ -75,6 +75,9 @@ instance : SetLike (Opens α) α where
 instance : CanLift (Set α) (Opens α) (↑) IsOpen :=
   ⟨fun s h => ⟨⟨s, h⟩, rfl⟩⟩
 
+instance instSecondCountableOpens [SecondCountableTopology α] (U : Opens α) :
+    SecondCountableTopology U := inferInstanceAs (SecondCountableTopology U.1)
+
 theorem «forall» {p : Opens α → Prop} : (∀ U, p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p ⟨U, hU⟩ :=
   ⟨fun h _ _ => h _, fun h _ => h _ _⟩