fix

Author: sgouezel

Mathlib/CategoryTheory/Localization/LocallySmall.lean

@@ -41,12 +41,13 @@ noncomputable def hasLocalizationOfLocallySmall
   D := ShrinkHoms D
   L := L ⋙ (ShrinkHoms.equivalence D).functor
 
+-- adding `@[implicit_reducible]` causes downstream breakage
+set_option warn.classDefReducibility false in
 /-- If `L : C ⥤ D` is a localization functor for a class of morphisms
 `W : MorphismProperty C`, and `D` is locally `w`-small, we may obtain
 a `HasLocalization.{w} W` instance. This should be used only in the
 unlikely situation where the types of objects of `C` and `D` are in
 different universes. Otherwise, use `hasLocalizationOfLocallySmall`. -/
-@[implicit_reducible]
 noncomputable irreducible_def hasLocalizationOfLocallySmall'
     {D : Type u₂} [Category.{v₂} D] [LocallySmall.{w} D]
     (L : C ⥤ D) [L.IsLocalization W] :

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -287,7 +287,9 @@ lemma even_card_of_isPerfectMatching [Fintype V] [DecidableEq V] [DecidableRel G
   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
+  have := (hM.induce_connectedComponent_isMatching c).even_card
+  simp only [Subgraph.induce_verts, Set.toFinset_card] at this
+  exact this
 
 set_option backward.isDefEq.respectTransparency false in
 lemma odd_matches_node_outside [Finite V] {u : Set V}

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

@@ -197,7 +197,7 @@ theorem IsSRGWith.matrix_eq {α : Type*} [Semiring α] (h : G.IsSRGWith n k ℓ
   ext v w
   simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply,
     adjMatrix_apply, compl_adj]
-  rw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
+  erw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
   obtain rfl | hn := eq_or_ne v w
   · rw [← Set.toFinset_card]
     simp [commonNeighbors, ← neighborFinset_def, h.regular v]