diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
index 1608c8f3a73275..d583ba95bba822 100644
--- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
+++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@@ -52,8 +52,16 @@ def FormalMultilinearSeries (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 
   ∀ n : ℕ, E [×n]→L[𝕜] F
 deriving Inhabited
 
-set_option backward.inferInstanceAs.wrap.data false in
-deriving instance AddCommMonoid for FormalMultilinearSeries
+section AddCommMonoid
+
+/-- Copy `Pi.addCommMonoid`, ensuring the pointwise operations hold by defeq. -/
+instance : AddCommMonoid (FormalMultilinearSeries 𝕜 E F) where
+  __ := Pi.addCommMonoid
+  zero _ := 0
+  add x y n := x n + y n
+  nsmul k x n := k • x n
+
+end AddCommMonoid
 
 section Module
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp.lean b/Mathlib/CategoryTheory/Monoidal/Grp.lean
index 738100d40f13e7..23c64ca9e1ef94 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp.lean
@@ -93,12 +93,10 @@ namespace Grp
 /-- An additive group object is an additive monoid object. -/]
 abbrev toMon (A : Grp C) : Mon C := ⟨A.X⟩
 
-set_option backward.inferInstanceAs.wrap.data false in
 variable (C) in
 /-- The trivial group object. -/
 @[to_additive (attr := simps!) /-- The trivial additive group object. -/]
-def trivial : Grp C :=
-  { Mon.trivial C with grp := inferInstanceAs (GrpObj (𝟙_ C)) }
+def trivial : Grp C := { Mon.trivial C with grp := GrpObj.instTensorUnit }
 
 @[to_additive]
 instance : Inhabited (Grp C) where
diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean
index 012023be38310b..72dc27723d7bb1 100644
--- a/Mathlib/GroupTheory/Torsion.lean
+++ b/Mathlib/GroupTheory/Torsion.lean
@@ -348,13 +348,19 @@ end CommGroup
 
 section AddCommGroup
 
-set_option backward.inferInstanceAs.wrap.data false in
 instance {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] :
     Module R (M ⧸ AddCommGroup.torsion M) :=
-  letI : Submodule R M := { AddCommGroup.torsion M with smul_mem' := fun r m ⟨n, hn, hn'⟩ ↦
+  -- Upgrade the torsion subgroup to a submodule.
+  letI S : Submodule R M := { AddCommGroup.torsion M with smul_mem' := fun r m ⟨n, hn, hn'⟩ ↦
     ⟨n, hn, by { simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
       smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }⟩ }
-  inferInstanceAs (Module R (M ⧸ this))
+  -- The quotients are the same.
+  let e : (M ⧸ AddCommGroup.torsion M) ≃+ (M ⧸ S) := QuotientAddGroup.congr _ _ (.refl _)
+    (by simp [S])
+  -- So we can copy over scalar multiplication.
+  letI : SMul R (M ⧸ AddCommGroup.torsion M) := ⟨fun r m => e.symm (r • e m)⟩
+  Function.Injective.module R e.toAddMonoidHom e.injective (fun _ _ =>
+    e.symm.injective (e.symm_apply_apply _))
 
 end AddCommGroup
 
diff --git a/Mathlib/RingTheory/Etale/Kaehler.lean b/Mathlib/RingTheory/Etale/Kaehler.lean
index 5e8c1ce4360dfa..f548898ec50c78 100644
--- a/Mathlib/RingTheory/Etale/Kaehler.lean
+++ b/Mathlib/RingTheory/Etale/Kaehler.lean
@@ -271,7 +271,6 @@ end Extension
 
 variable {S}
 
-set_option backward.inferInstanceAs.wrap.data false in
 set_option backward.isDefEq.respectTransparency false in
 /-- let `p` be a submonoid of an `R`-algebra `S`. Then `Sₚ ⊗ H¹(L_{S/R}) ≃ H¹(L_{Sₚ/R})`. -/
 noncomputable