chore: backports for leanprover/lean4#4814 (part 39) (#15636)

Mathlib/Data/DFinsupp/Basic.lean

@@ -479,8 +479,6 @@ theorem subtypeDomain_sub [∀ i, AddGroup (β i)] {p : ι → Prop} [DecidableP
 
 end FilterAndSubtypeDomain
 
-variable [DecidableEq ι]
-
 section Basic
 
 variable [∀ i, Zero (β i)]
@@ -489,6 +487,9 @@ theorem finite_support (f : Π₀ i, β i) : Set.Finite { i | f i ≠ 0 } :=
   Trunc.induction_on f.support' fun xs ↦
     xs.1.finite_toSet.subset fun i H ↦ ((xs.prop i).resolve_right H)
 
+section DecidableEq
+variable [DecidableEq ι]
+
 /-- Create an element of `Π₀ i, β i` from a finset `s` and a function `x`
 defined on this `Finset`. -/
 def mk (s : Finset ι) (x : ∀ i : (↑s : Set ι), β (i : ι)) : Π₀ i, β i :=
@@ -515,6 +516,8 @@ theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β _ _ s) := b
   dsimp only [mk_apply, Subtype.coe_mk] at h1
   simpa only [dif_pos hi] using h1
 
+end DecidableEq
+
 instance unique [∀ i, Subsingleton (β i)] : Unique (Π₀ i, β i) :=
   DFunLike.coe_injective.unique
 
@@ -534,6 +537,8 @@ def equivFunOnFintype [Fintype ι] : (Π₀ i, β i) ≃ ∀ i, β i where
 theorem equivFunOnFintype_symm_coe [Fintype ι] (f : Π₀ i, β i) : equivFunOnFintype.symm f = f :=
   Equiv.symm_apply_apply _ _
 
+variable [DecidableEq ι]
+
 /-- The function `single i b : Π₀ i, β i` sends `i` to `b`
 and all other points to `0`. -/
 def single (i : ι) (b : β i) : Π₀ i, β i :=
@@ -757,6 +762,9 @@ end Update
 
 end Basic
 
+section DecidableEq
+variable [DecidableEq ι]
+
 section AddMonoid
 
 variable [∀ i, AddZeroClass (β i)]
@@ -1154,6 +1162,8 @@ instance [∀ i, Zero (β i)] [∀ i, DecidableEq (β i)] : DecidableEq (Π₀ i
       rw [hf, hg],
      by rintro rfl; simp⟩
 
+end DecidableEq
+
 section Equiv
 
 open Finset
@@ -1194,8 +1204,9 @@ theorem comapDomain_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMu
   rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]
 
 @[simp]
-theorem comapDomain_single [DecidableEq κ] [∀ i, Zero (β i)] (h : κ → ι) (hh : Function.Injective h)
-    (k : κ) (x : β (h k)) : comapDomain h hh (single (h k) x) = single k x := by
+theorem comapDomain_single [DecidableEq ι] [DecidableEq κ] [∀ i, Zero (β i)] (h : κ → ι)
+    (hh : Function.Injective h) (k : κ) (x : β (h k)) :
+    comapDomain h hh (single (h k) x) = single k x := by
   ext i
   rw [comapDomain_apply]
   obtain rfl | hik := Decidable.eq_or_ne i k
@@ -1286,6 +1297,8 @@ instance distribMulAction₂ [Monoid γ] [∀ i j, AddMonoid (δ i j)]
     [∀ i j, DistribMulAction γ (δ i j)] : DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j) :=
   @DFinsupp.distribMulAction ι _ (fun i => Π₀ j, δ i j) _ _ _
 
+variable [DecidableEq ι]
+
 /-- The natural map between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.  -/
 def sigmaCurry [∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
     Π₀ (i) (j), δ i j where
@@ -1363,33 +1376,32 @@ def sigmaUncurry [∀ i j, Zero (δ i j)] [DecidableEq ι] (f : Π₀ (i) (j), 
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
 @[simp]
-theorem sigmaUncurry_apply [∀ i j, Zero (δ i j)] [DecidableEq ι]
+theorem sigmaUncurry_apply [∀ i j, Zero (δ i j)]
     (f : Π₀ (i) (j), δ i j) (i : ι) (j : α i) :
     sigmaUncurry f ⟨i, j⟩ = f i j :=
   rfl
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
 @[simp]
-theorem sigmaUncurry_zero [∀ i j, Zero (δ i j)] [DecidableEq ι] :
+theorem sigmaUncurry_zero [∀ i j, Zero (δ i j)] :
     sigmaUncurry (0 : Π₀ (i) (j), δ i j) = 0 :=
   rfl
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
 @[simp]
-theorem sigmaUncurry_add [∀ i j, AddZeroClass (δ i j)] [DecidableEq ι]
-    (f g : Π₀ (i) (j), δ i j) :
+theorem sigmaUncurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i) (j), δ i j) :
     sigmaUncurry (f + g) = sigmaUncurry f + sigmaUncurry g :=
   DFunLike.coe_injective rfl
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
 @[simp]
-theorem sigmaUncurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [DecidableEq ι]
+theorem sigmaUncurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)]
     [∀ i j, DistribMulAction γ (δ i j)]
     (r : γ) (f : Π₀ (i) (j), δ i j) : sigmaUncurry (r • f) = r • sigmaUncurry f :=
   DFunLike.coe_injective rfl
 
 @[simp]
-theorem sigmaUncurry_single [∀ i j, Zero (δ i j)] [DecidableEq ι] [∀ i, DecidableEq (α i)]
+theorem sigmaUncurry_single [∀ i j, Zero (δ i j)] [∀ i, DecidableEq (α i)]
     (i) (j : α i) (x : δ i j) :
     sigmaUncurry (single i (single j x : Π₀ j : α i, δ i j)) = single ⟨i, j⟩ (by exact x) := by
   ext ⟨i', j'⟩
@@ -1493,6 +1505,8 @@ end Equiv
 
 section ProdAndSum
 
+variable [DecidableEq ι]
+
 /-- `DFinsupp.prod f g` is the product of `g i (f i)` over the support of `f`. -/
 @[to_additive "`sum f g` is the sum of `g i (f i)` over the support of `f`."]
 def prod [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] (f : Π₀ i, β i)
@@ -1553,9 +1567,10 @@ theorem prod_comm {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι
   Finset.prod_comm
 
 @[simp]
-theorem sum_apply {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
-    [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] {f : Π₀ i₁, β₁ i₁}
-    {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {i₂ : ι} : (f.sum g) i₂ = f.sum fun i₁ b => g i₁ b i₂ :=
+theorem sum_apply {ι} {β : ι → Type v} {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁}
+    [∀ i₁, Zero (β₁ i₁)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)]
+    {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {i₂ : ι} :
+    (f.sum g) i₂ = f.sum fun i₁ b => g i₁ b i₂ :=
   map_sum (evalAddMonoidHom i₂) _ f.support
 
 theorem support_sum {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
@@ -1874,13 +1889,14 @@ theorem prod_subtypeDomain_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decid
     (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h := by
   refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop
 
-theorem subtypeDomain_sum [∀ i, AddCommMonoid (β i)] {s : Finset γ} {h : γ → Π₀ i, β i}
-    {p : ι → Prop} [DecidablePred p] :
+theorem subtypeDomain_sum {ι} {β : ι → Type v} [∀ i, AddCommMonoid (β i)] {s : Finset γ}
+    {h : γ → Π₀ i, β i} {p : ι → Prop} [DecidablePred p] :
     (∑ c ∈ s, h c).subtypeDomain p = ∑ c ∈ s, (h c).subtypeDomain p :=
   map_sum (subtypeDomainAddMonoidHom β p) _ s
 
-theorem subtypeDomain_finsupp_sum {δ : γ → Type x} [DecidableEq γ] [∀ c, Zero (δ c)]
-    [∀ (c) (x : δ c), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p]
+theorem subtypeDomain_finsupp_sum {ι} {β : ι → Type v} {δ : γ → Type x} [DecidableEq γ]
+    [∀ c, Zero (δ c)]  [∀ (c) (x : δ c), Decidable (x ≠ 0)]
+    [∀ i, AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p]
     {s : Π₀ c, δ c} {h : ∀ c, δ c → Π₀ i, β i} :
     (s.sum h).subtypeDomain p = s.sum fun c d => (h c d).subtypeDomain p :=
   subtypeDomain_sum

Mathlib/Data/DFinsupp/Notation.lean

@@ -42,7 +42,7 @@ def elabUpdate₀ : Elab.Term.TermElab
     Elab.Term.tryPostponeIfNoneOrMVar ty?
     let .some ty := ty? | Elab.throwUnsupportedSyntax
     let_expr DFinsupp _ _ _ := ← Meta.withReducible (Meta.whnf ty) | Elab.throwUnsupportedSyntax
-    Elab.Term.elabTerm (← `(DFinsupp.update $i $f $x)) ty?
+    Elab.Term.elabTerm (← `(DFinsupp.update $f $i $x)) ty?
   | _ => fun _ => Elab.throwUnsupportedSyntax
 
 /-- Unexpander for the `fun₀ | i => x` notation. -/