chore: silence deprecation warning in DirectSumIsInternal (#6416)

@eric-wieser, would you be able to find a better solution to this?



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Counterexamples/DirectSumIsInternal.lean

@@ -87,7 +87,7 @@ theorem withSign.not_injective :
     intro h
     -- porting note: `DFinsupp.singleAddHom_apply` doesn't work so we have to unfold
     dsimp [DirectSum.lof_eq_of, DirectSum.of, DFinsupp.singleAddHom] at h
-    replace h := DFinsupp.ext_iff.mp h 1
+    replace h := FunLike.congr_fun h 1
     rw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same,
       DFinsupp.single_eq_of_ne UnitsInt.one_ne_neg_one.symm, add_zero, Subtype.ext_iff,
       Submodule.coe_zero] at h

Mathlib/Algebra/DirectSum/Basic.lean

@@ -47,6 +47,9 @@ instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
 instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
   inferInstanceAs (AddCommMonoid (Π₀ i, β i))
 
+instance [∀ i, AddCommMonoid (β i)] : FunLike (DirectSum ι β) _ fun i : ι => β i :=
+  inferInstanceAs (FunLike (Π₀ i, β i) _ _)
+
 instance [∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i :=
   inferInstanceAs (CoeFun (Π₀ i, β i) fun _ => ∀ i : ι, β i)