chore(DirectSum): clean up instances (leanprover-community#37135)

Clean up instances on `DirectSum` using `InferInstanceAs`.
Clean up instances in `TensorProduct/Graded`, which depend on the `DirectSum` instances.
Golf away some `backward` options.

Author: JovanGerb

Mathlib/Algebra/DirectSum/Basic.lean

@@ -105,6 +105,11 @@ variable {β}
 theorem add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i :=
   rfl
 
+@[simp]
+theorem sum_apply {α} (s : Finset α) (g : α → ⨁ i, β i) (i : ι) :
+    (∑ a ∈ s, g a) i = ∑ a ∈ s, g a i :=
+  DFinsupp.finset_sum_apply s g i
+
 section DecidableEq
 
 variable [DecidableEq ι]
@@ -135,16 +140,12 @@ lemma of_apply {i : ι} (j : ι) (x : β i) : of β i x j = if h : i = j then Eq
   DFinsupp.single_apply
 
 theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
-    mk β s f n = f ⟨n, hn⟩ := by
-  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
-  -- Previously, `DFinsupp.mk_apply` was in the `dsimp only`
-  rw [DFinsupp.mk_apply, dif_pos hn]
+    mk β s f n = f ⟨n, hn⟩ :=
+  DFinsupp.mk_of_mem hn
 
 theorem mk_apply_of_notMem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) :
-    mk β s f n = 0 := by
-  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
-  -- Previously, `DFinsupp.mk_apply` was in the `dsimp only`
-  rw [DFinsupp.mk_apply, dif_neg hn]
+    mk β s f n = 0 :=
+  DFinsupp.mk_of_notMem hn
 
 @[simp]
 theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅ :=
@@ -163,11 +164,9 @@ theorem sum_support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (x : ⨁ i
     (∑ i ∈ x.support, of β i (x i)) = x :=
   DFinsupp.sum_single
 
-set_option backward.isDefEq.respectTransparency false in
 theorem sum_univ_of [Fintype ι] (x : ⨁ i, β i) :
     ∑ i ∈ Finset.univ, of β i (x i) = x := by
-  apply DFinsupp.ext (fun i ↦ ?_)
-  rw [DFinsupp.finset_sum_apply]
+  ext i
   simp [of_apply]
 
 theorem mk_injective (s : Finset ι) : Function.Injective (mk β s) :=
@@ -217,12 +216,13 @@ def toAddMonoid : (⨁ i, β i) →+ γ :=
 theorem toAddMonoid_of (i) (x : β i) : toAddMonoid φ (of β i x) = φ i x :=
   DFinsupp.liftAddHom_apply_single φ i x
 
-set_option backward.isDefEq.respectTransparency false in
 theorem toAddMonoid.unique (f : ⨁ i, β i) : ψ f = toAddMonoid (fun i => ψ.comp (of β i)) f := by
   congr
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` applies addHom_ext' here, which isn't what we want.
   apply DFinsupp.addHom_ext'
-  simp [toAddMonoid, of]
+  intro
+  simp [toAddMonoid]
+  rfl
 
 lemma toAddMonoid_injective : Injective (toAddMonoid : (∀ i, β i →+ γ) → (⨁ i, β i) →+ γ) :=
   DFinsupp.liftAddHom.injective

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -207,16 +207,6 @@ theorem AddSubmonoidClass.IsHomogeneous.ext
 
 end AddCommMonoid
 
-/-- The `-` in the statements below doesn't resolve without this line.
-
-This seems to be a problem of synthesized vs inferred typeclasses disagreeing. If we replace
-the statement of `decompose_neg` with `@Eq (⨁ i, ℳ i) (decompose ℳ (-x)) (-decompose ℳ x)`
-instead of `decompose ℳ (-x) = -decompose ℳ x`, which forces the typeclasses needed by `⨁ i, ℳ i`
-to be found by unification rather than synthesis, then everything works fine without this
-instance. -/
-instance addCommGroupSetLike [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) :
-    AddCommGroup (⨁ i, ℳ i) := by infer_instance
-
 section AddCommGroup
 
 variable [DecidableEq ι] [AddCommGroup M]

Mathlib/Algebra/DirectSum/Module.lean

@@ -40,18 +40,18 @@ variable {ι : Type v}
 variable {M : ι → Type w} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
 
 instance : Module R (⨁ i, M i) :=
-  DFinsupp.module
+  inferInstanceAs <| Module R (Π₀ i, M i)
 
 instance {S : Type*} [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] :
     SMulCommClass R S (⨁ i, M i) :=
-  DFinsupp.smulCommClass
+  inferInstanceAs <| SMulCommClass R S (Π₀ i, M i)
 
 instance {S : Type*} [Semiring S] [SMul R S] [∀ i, Module S (M i)] [∀ i, IsScalarTower R S (M i)] :
     IsScalarTower R S (⨁ i, M i) :=
-  DFinsupp.isScalarTower
+  inferInstanceAs <| IsScalarTower R S (Π₀ i, M i)
 
 instance [∀ i, Module Rᵐᵒᵖ (M i)] [∀ i, IsCentralScalar R (M i)] : IsCentralScalar R (⨁ i, M i) :=
-  DFinsupp.isCentralScalar
+  inferInstanceAs <| IsCentralScalar R (Π₀ i, M i)
 
 theorem smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : (b • v) i = b • v i :=
   DFinsupp.smul_apply _ _ _

Mathlib/Algebra/DirectSum/Ring.lean

@@ -189,13 +189,12 @@ def mulHom : (⨁ i, A i) →+ (⨁ i, A i) →+ ⨁ i, A i :=
 instance instMul : Mul (⨁ i, A i) where
   mul := fun a b => mulHom A a b
 
-instance : NonUnitalNonAssocSemiring (⨁ i, A i) :=
-  { (inferInstance : AddCommMonoid _) with
-    zero_mul := fun _ => by simp only [Mul.mul, HMul.hMul, map_zero, AddMonoidHom.zero_apply]
-    mul_zero := fun _ => by simp only [Mul.mul, HMul.hMul, map_zero]
-    left_distrib := fun _ _ _ => by simp only [Mul.mul, HMul.hMul, map_add]
-    right_distrib := fun _ _ _ => by
-      simp only [Mul.mul, HMul.hMul, map_add, AddMonoidHom.add_apply] }
+instance : NonUnitalNonAssocSemiring (⨁ i, A i) where
+  zero_mul := fun _ => by simp only [Mul.mul, HMul.hMul, map_zero, AddMonoidHom.zero_apply]
+  mul_zero := fun _ => by simp only [Mul.mul, HMul.hMul, map_zero]
+  left_distrib := fun _ _ _ => by simp only [Mul.mul, HMul.hMul, map_add]
+  right_distrib := fun _ _ _ => by
+    simp only [Mul.mul, HMul.hMul, map_add, AddMonoidHom.add_apply]
 
 variable {A}
 
@@ -217,23 +216,20 @@ variable [∀ i, AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A]
 
 open AddMonoidHom (flipHom coe_comp compHom flip_apply)
 
-set_option backward.privateInPublic true in
 private nonrec theorem one_mul (x : ⨁ i, A i) : 1 * x = x := by
   suffices mulHom A One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
   apply addHom_ext; intro i xi
   simp only [One.one]
   rw [mulHom_of_of]
   exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)
 
-set_option backward.privateInPublic true in
 private nonrec theorem mul_one (x : ⨁ i, A i) : x * 1 = x := by
   suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
   apply addHom_ext; intro i xi
   simp only [One.one]
   rw [flip_apply, mulHom_of_of]
   exact of_eq_of_gradedMonoid_eq (mul_one <| GradedMonoid.mk i xi)
 
-set_option backward.privateInPublic true in
 private theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) := by
   -- (`fun a b c => a * b * c` as a bundled hom) = (`fun a b c => a * (b * c)` as a bundled hom)
   suffices AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ by
@@ -248,20 +244,17 @@ private theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) := by
 instance instNatCast : NatCast (⨁ i, A i) where
   natCast := fun n => of _ _ (GSemiring.natCast n)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The `Semiring` structure derived from `GSemiring A`. -/
-instance semiring : Semiring (⨁ i, A i) :=
-  { (inferInstance : NonUnitalNonAssocSemiring _) with
-    one_mul := one_mul A
-    mul_one := mul_one A
-    mul_assoc := mul_assoc A
-    toNatCast := instNatCast _
-    natCast_zero := by simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]
-    natCast_succ := fun n => by
-      simp_rw [NatCast.natCast, GSemiring.natCast_succ]
-      rw [map_add]
-      rfl }
+instance semiring : Semiring (⨁ i, A i) where
+  one_mul := private one_mul A
+  mul_one := private mul_one A
+  mul_assoc := private mul_assoc A
+  toNatCast := instNatCast _
+  natCast_zero := by simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]
+  natCast_succ := fun n => by
+    simp_rw [NatCast.natCast, GSemiring.natCast_succ]
+    rw [map_add]
+    rfl
 
 theorem ofPow {i} (a : A i) (n : ℕ) :
     of _ i a ^ n = of _ (n • i) (GradedMonoid.GMonoid.gnpow _ a) := by
@@ -297,10 +290,8 @@ theorem mul_eq_dfinsuppSum [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' :
   dsimp only [DirectSum]
   rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsuppSum_apply]
   apply congrArg _
-  simp_rw [flip_apply]
   funext x
-  simp [AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.gMulHom,
-    DirectSum.toAddMonoid]
+  simp [AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.toAddMonoid]
 
 /-- A heavily unfolded version of the definition of multiplication -/
 theorem mul_eq_sum_support_ghas_mul [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
@@ -315,20 +306,16 @@ section CommSemiring
 
 variable [∀ i, AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A]
 
-set_option backward.privateInPublic true in
 private theorem mul_comm (a b : ⨁ i, A i) : a * b = b * a := by
   suffices mulHom A = (mulHom A).flip by
     rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
   apply addHom_ext; intro ai ax; apply addHom_ext; intro bi bx
   rw [AddMonoidHom.flip_apply, mulHom_of_of, mulHom_of_of]
   exact of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The `CommSemiring` structure derived from `GCommSemiring A`. -/
-instance commSemiring : CommSemiring (⨁ i, A i) :=
-  { DirectSum.semiring A with
-    mul_comm := mul_comm A }
+instance commSemiring : CommSemiring (⨁ i, A i) where
+  mul_comm := private mul_comm A
 
 end CommSemiring
 
@@ -337,9 +324,7 @@ section NonUnitalNonAssocRing
 variable [∀ i, AddCommGroup (A i)] [Add ι] [GNonUnitalNonAssocSemiring A]
 
 /-- The `Ring` derived from `GSemiring A`. -/
-instance nonAssocRing : NonUnitalNonAssocRing (⨁ i, A i) :=
-  { (inferInstance : NonUnitalNonAssocSemiring (⨁ i, A i)),
-    (inferInstance : AddCommGroup (⨁ i, A i)) with }
+instance nonAssocRing : NonUnitalNonAssocRing (⨁ i, A i) where
 
 end NonUnitalNonAssocRing
 
@@ -349,13 +334,11 @@ variable [∀ i, AddCommGroup (A i)] [AddMonoid ι] [GRing A]
 
 -- Porting note: overspecified fields in ml4
 /-- The `Ring` derived from `GSemiring A`. -/
-instance ring : Ring (⨁ i, A i) :=
-  { DirectSum.semiring A,
-    (inferInstance : AddCommGroup (⨁ i, A i)) with
-    toIntCast.intCast := fun z => of A 0 <| (GRing.intCast z)
-    intCast_ofNat := fun _ => congrArg (of A 0) <| GRing.intCast_ofNat _
-    intCast_negSucc := fun _ =>
-      (congrArg (of A 0) <| GRing.intCast_negSucc_ofNat _).trans <| map_neg _ _ }
+instance ring : Ring (⨁ i, A i) where
+  toIntCast.intCast z := of A 0 <| (GRing.intCast z)
+  intCast_ofNat _ := congrArg (of A 0) <| GRing.intCast_ofNat _
+  intCast_negSucc _ :=
+    (congrArg (of A 0) <| GRing.intCast_negSucc_ofNat _).trans <| map_neg _ _
 
 end Ring
 
@@ -364,9 +347,7 @@ section CommRing
 variable [∀ i, AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A]
 
 /-- The `CommRing` derived from `GCommSemiring A`. -/
-instance commRing : CommRing (⨁ i, A i) :=
-  { DirectSum.ring A,
-    DirectSum.commSemiring A with }
+instance commRing : CommRing (⨁ i, A i) where
 
 end CommRing
 
@@ -610,26 +591,22 @@ variable (ι)
 /-- A direct sum of copies of a `NonUnitalNonAssocSemiring` inherits the multiplication structure.
 -/
 instance NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring {R : Type*} [AddMonoid ι]
-    [NonUnitalNonAssocSemiring R] : DirectSum.GNonUnitalNonAssocSemiring fun _ : ι => R :=
-  { -- Porting note: removed Mul.gMul ι with and we seem ok
-    mul_zero := mul_zero
-    zero_mul := zero_mul
-    mul_add := mul_add
-    add_mul := add_mul }
+    [NonUnitalNonAssocSemiring R] : DirectSum.GNonUnitalNonAssocSemiring fun _ : ι => R where
+  mul_zero := mul_zero
+  zero_mul := zero_mul
+  mul_add := mul_add
+  add_mul := add_mul
 
 /-- A direct sum of copies of a `Semiring` inherits the multiplication structure. -/
 instance Semiring.directSumGSemiring {R : Type*} [AddMonoid ι] [Semiring R] :
     DirectSum.GSemiring fun _ : ι => R where
-  __ := NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring ι
-  __ := Monoid.gMonoid ι
   natCast n := n
   natCast_zero := Nat.cast_zero
   natCast_succ := Nat.cast_succ
 
 /-- A direct sum of copies of a `Ring` inherits the multiplication structure. -/
 instance Ring.directSumGRing {R : Type*} [AddMonoid ι] [Ring R] :
     DirectSum.GRing fun _ : ι => R where
-  __ := Semiring.directSumGSemiring ι
   intCast z := z
   intCast_ofNat := Int.cast_natCast
   intCast_negSucc_ofNat := Int.cast_negSucc
@@ -644,13 +621,9 @@ example {R : Type*} [AddMonoid ι] [Semiring R] (i j : ι) (a b : R) :
 /-- A direct sum of copies of a `CommSemiring` inherits the commutative multiplication structure. -/
 instance CommSemiring.directSumGCommSemiring {R : Type*} [AddCommMonoid ι] [CommSemiring R] :
     DirectSum.GCommSemiring fun _ : ι => R where
-  __ := Semiring.directSumGSemiring ι
-  __ := CommMonoid.gCommMonoid ι
 
 /-- A direct sum of copies of a `CommRing` inherits the commutative multiplication structure. -/
 instance CommRing.directSumGCommRing {R : Type*} [AddCommMonoid ι] [CommRing R] :
     DirectSum.GCommRing fun _ : ι => R where
-  __ := Ring.directSumGRing ι
-  __ := CommMonoid.gCommMonoid ι
 
 end Uniform