diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean
index 60a683a4cbef8..d1e2078afece0 100644
--- a/Mathlib/Analysis/BoxIntegral/Integrability.lean
+++ b/Mathlib/Analysis/BoxIntegral/Integrability.lean
@@ -141,19 +141,15 @@ theorem HasIntegral.of_aeEq_zero {l : IntegrationParams} {I : Box ι} {f : (ι 
     exact hJ.2 ▸ Nat.le_ceil _
   refine' (norm_sum_le_of_le _ this).trans _; clear this
   rw [← sum_mul, ← Prepartition.measure_iUnion_toReal]
-  -- Adaption note: v4.7.0-rc1
-  -- The behaviour of `generalize` was changed in https://github.com/leanprover/lean4/pull/3575
-  -- to use transparancy `instances` (rather than `default`)
-  -- `generalize'` is a temporary backwards compatibility shim.
-  -- Hopefully we will be able to refactor this proof to use `generalize` again, and then drop
-  -- `generalize'`.
-  generalize' hm : μ (π.filter fun J => N (π.tag J) = n).iUnion = m
+  let m := μ (π.filter fun J => N (π.tag J) = n).iUnion
+  show m.toReal * ↑n ≤ ↑(δ n)
   have : m < δ n / n := by
     simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
-    refine' hm ▸ (measure_mono _).trans_lt (hμU _)
+    refine' (measure_mono _).trans_lt (hμU _)
     simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
     rintro x ⟨J, ⟨hJ, rfl⟩, hx⟩
     exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
+  clear_value m
   lift m to ℝ≥0 using ne_top_of_lt this
   rw [ENNReal.coe_toReal, ← NNReal.coe_nat_cast, ← NNReal.coe_mul, NNReal.coe_le_coe, ←
     ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_nat, mul_comm]
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index fd01dd7b1b11f..6a63f434a9562 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -210,18 +210,10 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) :
     rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
     refine' EqvGen.mono _ (D.eqvGen_of_π_eq h : _)
     rintro _ _ ⟨x⟩
-    rw [← show (sigmaIsoSigma.{u, u} _).inv _ = x from
-        ConcreteCategory.congr_hom (sigmaIsoSigma.{u, u} _).hom_inv_id x]
-  -- Adaption note: v4.7.0-rc1
-  -- The behaviour of `generalize` was changed in https://github.com/leanprover/lean4/pull/3575
-  -- to use transparancy `instances` (rather than `default`)
-  -- `generalize'` is a temporary backwards compatibility shim.
-  -- Hopefully we will be able to refactor this proof to use `generalize` again, and then drop
-  -- `generalize'`.
-    generalize' h : (sigmaIsoSigma.{u, u} D.V).hom x = x'
-    obtain ⟨⟨i, j⟩, y⟩ := x'
+    obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
+      (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
     unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
-    simp only [Opens.inclusion_apply, TopCat.comp_app, sigmaIsoSigma_inv_apply,
+    simp only [forget_map_eq_coe, Opens.inclusion_apply, TopCat.comp_app, sigmaIsoSigma_inv_apply,
       Cofan.mk_ι_app]
     rw [← comp_apply, colimit.ι_desc, ← comp_apply, colimit.ι_desc]
     erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]