bump to nightly-2023-07-12-07

mathlib commit leanprover-community/mathlib@4e24c4b

Counterexamples/DirectSumIsInternal.lean

@@ -94,8 +94,8 @@ theorem withSign.not_injective :
     intro h
     dsimp [z, DirectSum.lof_eq_of, DirectSum.of] at h 
     replace h := dfinsupp.ext_iff.mp h 1
-    rw [Dfinsupp.zero_apply, Dfinsupp.add_apply, Dfinsupp.single_eq_same,
-      Dfinsupp.single_eq_of_ne units_int.one_ne_neg_one.symm, add_zero, Subtype.ext_iff,
+    rw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same,
+      DFinsupp.single_eq_of_ne units_int.one_ne_neg_one.symm, add_zero, Subtype.ext_iff,
       Submodule.coe_zero] at h 
     apply zero_ne_one h.symm
   apply hinj.ne this

Mathbin/Algebra/DirectLimit.lean

@@ -224,8 +224,8 @@ theorem toModule_totalize_of_le {x : DirectSum ι G} {i j : ι} (hij : i ≤ j)
     DirectSum.toModule R ι (G j) (fun k => totalize G f k j) x =
       f i j hij (DirectSum.toModule R ι (G i) (fun k => totalize G f k i) x) :=
   by
-  rw [← @Dfinsupp.sum_single ι G _ _ _ x]
-  unfold Dfinsupp.sum
+  rw [← @DFinsupp.sum_single ι G _ _ _ x]
+  unfold DFinsupp.sum
   simp only [LinearMap.map_sum]
   refine' Finset.sum_congr rfl fun k hk => _
   rw [DirectSum.single_eq_lof R k (x k), DirectSum.toModule_lof, DirectSum.toModule_lof,
@@ -248,8 +248,8 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : DirectS
           subst hxy
           constructor
           · intro i0 hi0
-            rw [Dfinsupp.mem_support_iff, DirectSum.sub_apply, ← DirectSum.single_eq_lof, ←
-              DirectSum.single_eq_lof, Dfinsupp.single_apply, Dfinsupp.single_apply] at hi0 
+            rw [DFinsupp.mem_support_iff, DirectSum.sub_apply, ← DirectSum.single_eq_lof, ←
+              DirectSum.single_eq_lof, DFinsupp.single_apply, DFinsupp.single_apply] at hi0 
             split_ifs at hi0  with hi hj hj; · rwa [hi] at hik ; · rwa [hi] at hik ;
             · rwa [hj] at hjk 
             exfalso; apply hi0; rw [sub_zero]
@@ -259,7 +259,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : DirectS
       (fun x y ⟨i, hi, hxi⟩ ⟨j, hj, hyj⟩ =>
         let ⟨k, hik, hjk⟩ := exists_ge_ge i j
         ⟨k, fun l hl =>
-          (Finset.mem_union.1 (Dfinsupp.support_add hl)).elim (fun hl => le_trans (hi _ hl) hik)
+          (Finset.mem_union.1 (DFinsupp.support_add hl)).elim (fun hl => le_trans (hi _ hl) hik)
             fun hl => le_trans (hj _ hl) hjk,
           by
           simp [LinearMap.map_add, hxi, hyj, to_module_totalize_of_le hik hi,

Mathbin/Algebra/DirectSum/Algebra.lean

@@ -77,15 +77,15 @@ instance : Algebra R (⨁ i, A i)
   map_mul' a b := by
     simp only [AddMonoidHom.comp_apply]
     rw [of_mul_of]
-    apply Dfinsupp.single_eq_of_sigma_eq (galgebra.map_mul a b)
+    apply DFinsupp.single_eq_of_sigma_eq (galgebra.map_mul a b)
   commutes' r x :=
     by
     change AddMonoidHom.mul (DirectSum.of _ _ _) x = add_monoid_hom.mul.flip (DirectSum.of _ _ _) x
     apply AddMonoidHom.congr_fun _ x
     ext i xi : 2
     dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]
     rw [of_mul_of, of_mul_of]
-    apply Dfinsupp.single_eq_of_sigma_eq (galgebra.commutes r ⟨i, xi⟩)
+    apply DFinsupp.single_eq_of_sigma_eq (galgebra.commutes r ⟨i, xi⟩)
   smul_def' r x :=
     by
     change DistribMulAction.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
@@ -94,7 +94,7 @@ instance : Algebra R (⨁ i, A i)
     dsimp only [AddMonoidHom.comp_apply, DistribMulAction.toAddMonoidHom_apply,
       AddMonoidHom.mul_apply]
     rw [DirectSum.of_mul_of, ← of_smul]
-    apply Dfinsupp.single_eq_of_sigma_eq (galgebra.smul_def r ⟨i, xi⟩)
+    apply DFinsupp.single_eq_of_sigma_eq (galgebra.smul_def r ⟨i, xi⟩)
 
 #print DirectSum.algebraMap_apply /-
 theorem algebraMap_apply (r : R) :

Mathbin/Algebra/DirectSum/Basic.lean

@@ -47,7 +47,7 @@ deriving AddCommMonoid, Inhabited
 -/
 
 instance [∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i :=
-  Dfinsupp.hasCoeToFun
+  DFinsupp.hasCoeToFun
 
 scoped[DirectSum] notation3"⨁ "(...)", "r:(scoped f => DirectSum _ f) => r
 
@@ -60,7 +60,7 @@ section AddCommGroup
 variable [∀ i, AddCommGroup (β i)]
 
 instance : AddCommGroup (DirectSum ι β) :=
-  Dfinsupp.addCommGroup
+  DFinsupp.addCommGroup
 
 variable {β}
 
@@ -98,72 +98,72 @@ variable (β)
 and has coefficient `x i` for `i` in `s`. -/
 def mk (s : Finset ι) : (∀ i : (↑s : Set ι), β i.1) →+ ⨁ i, β i
     where
-  toFun := Dfinsupp.mk s
-  map_add' _ _ := Dfinsupp.mk_add
-  map_zero' := Dfinsupp.mk_zero
+  toFun := DFinsupp.mk s
+  map_add' _ _ := DFinsupp.mk_add
+  map_zero' := DFinsupp.mk_zero
 #align direct_sum.mk DirectSum.mk
 -/
 
 #print DirectSum.of /-
 /-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`. -/
 def of (i : ι) : β i →+ ⨁ i, β i :=
-  Dfinsupp.singleAddHom β i
+  DFinsupp.singleAddHom β i
 #align direct_sum.of DirectSum.of
 -/
 
 #print DirectSum.of_eq_same /-
 @[simp]
 theorem of_eq_same (i : ι) (x : β i) : (of _ i x) i = x :=
-  Dfinsupp.single_eq_same
+  DFinsupp.single_eq_same
 #align direct_sum.of_eq_same DirectSum.of_eq_same
 -/
 
 #print DirectSum.of_eq_of_ne /-
 theorem of_eq_of_ne (i j : ι) (x : β i) (h : i ≠ j) : (of _ i x) j = 0 :=
-  Dfinsupp.single_eq_of_ne h
+  DFinsupp.single_eq_of_ne h
 #align direct_sum.of_eq_of_ne DirectSum.of_eq_of_ne
 -/
 
 #print DirectSum.support_zero /-
 @[simp]
 theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅ :=
-  Dfinsupp.support_zero
+  DFinsupp.support_zero
 #align direct_sum.support_zero DirectSum.support_zero
 -/
 
 #print DirectSum.support_of /-
 @[simp]
 theorem support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) :
     (of _ i x).support = {i} :=
-  Dfinsupp.support_single_ne_zero h
+  DFinsupp.support_single_ne_zero h
 #align direct_sum.support_of DirectSum.support_of
 -/
 
 #print DirectSum.support_of_subset /-
 theorem support_of_subset [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] {i : ι} {b : β i} :
     (of _ i b).support ⊆ {i} :=
-  Dfinsupp.support_single_subset
+  DFinsupp.support_single_subset
 #align direct_sum.support_of_subset DirectSum.support_of_subset
 -/
 
 #print DirectSum.sum_support_of /-
 theorem sum_support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (x : ⨁ i, β i) :
     ∑ i in x.support, of β i (x i) = x :=
-  Dfinsupp.sum_single
+  DFinsupp.sum_single
 #align direct_sum.sum_support_of DirectSum.sum_support_of
 -/
 
 variable {β}
 
 #print DirectSum.mk_injective /-
 theorem mk_injective (s : Finset ι) : Function.Injective (mk β s) :=
-  Dfinsupp.mk_injective s
+  DFinsupp.mk_injective s
 #align direct_sum.mk_injective DirectSum.mk_injective
 -/
 
 #print DirectSum.of_injective /-
 theorem of_injective (i : ι) : Function.Injective (of β i) :=
-  Dfinsupp.single_injective
+  DFinsupp.single_injective
 #align direct_sum.of_injective DirectSum.of_injective
 -/
 
@@ -172,7 +172,7 @@ theorem of_injective (i : ι) : Function.Injective (of β i) :=
 protected theorem induction_on {C : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (H_zero : C 0)
     (H_basic : ∀ (i : ι) (x : β i), C (of β i x)) (H_plus : ∀ x y, C x → C y → C (x + y)) : C x :=
   by
-  apply Dfinsupp.induction x H_zero
+  apply DFinsupp.induction x H_zero
   intro i b f h1 h2 ih
   solve_by_elim
 #align direct_sum.induction_on DirectSum.induction_on
@@ -183,7 +183,7 @@ protected theorem induction_on {C : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (H
 then they are equal. -/
 theorem addHom_ext {γ : Type _} [AddMonoid γ] ⦃f g : (⨁ i, β i) →+ γ⦄
     (H : ∀ (i : ι) (y : β i), f (of _ i y) = g (of _ i y)) : f = g :=
-  Dfinsupp.addHom_ext H
+  DFinsupp.addHom_ext H
 #align direct_sum.add_hom_ext DirectSum.addHom_ext
 -/
 
@@ -209,14 +209,14 @@ variable (φ : ∀ i, β i →+ γ) (ψ : (⨁ i, β i) →+ γ)
 /-- `to_add_monoid φ` is the natural homomorphism from `⨁ i, β i` to `γ`
 induced by a family `φ` of homomorphisms `β i → γ`. -/
 def toAddMonoid : (⨁ i, β i) →+ γ :=
-  Dfinsupp.liftAddHom φ
+  DFinsupp.liftAddHom φ
 #align direct_sum.to_add_monoid DirectSum.toAddMonoid
 -/
 
 #print DirectSum.toAddMonoid_of /-
 @[simp]
 theorem toAddMonoid_of (i) (x : β i) : toAddMonoid φ (of β i x) = φ i x :=
-  Dfinsupp.liftAddHom_apply_single φ i x
+  DFinsupp.liftAddHom_apply_single φ i x
 #align direct_sum.to_add_monoid_of DirectSum.toAddMonoid_of
 -/
 
@@ -270,14 +270,14 @@ variable {β}
 
 #print DirectSum.unique /-
 instance unique [∀ i, Subsingleton (β i)] : Unique (⨁ i, β i) :=
-  Dfinsupp.unique
+  DFinsupp.unique
 #align direct_sum.unique DirectSum.unique
 -/
 
 #print DirectSum.uniqueOfIsEmpty /-
 /-- A direct sum over an empty type is trivial. -/
 instance uniqueOfIsEmpty [IsEmpty ι] : Unique (⨁ i, β i) :=
-  Dfinsupp.uniqueOfIsEmpty
+  DFinsupp.uniqueOfIsEmpty
 #align direct_sum.unique_of_is_empty DirectSum.uniqueOfIsEmpty
 -/
 
@@ -306,15 +306,15 @@ variable {κ : Type _}
 #print DirectSum.equivCongrLeft /-
 /-- Reindexing terms of a direct sum.-/
 def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) :=
-  { Dfinsupp.equivCongrLeft h with map_add' := Dfinsupp.comapDomain'_add _ _ }
+  { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ _ }
 #align direct_sum.equiv_congr_left DirectSum.equivCongrLeft
 -/
 
 #print DirectSum.equivCongrLeft_apply /-
 @[simp]
 theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) :
     equivCongrLeft h f k = f (h.symm k) :=
-  Dfinsupp.comapDomain'_apply _ _ _ _
+  DFinsupp.comapDomain'_apply _ _ _ _
 #align direct_sum.equiv_congr_left_apply DirectSum.equivCongrLeft_apply
 -/
 
@@ -328,7 +328,7 @@ variable {α : Option ι → Type w} [∀ i, AddCommMonoid (α i)]
 /-- Isomorphism obtained by separating the term of index `none` of a direct sum over `option ι`.-/
 @[simps]
 noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=
-  { Dfinsupp.equivProdDfinsupp with map_add' := Dfinsupp.equivProdDfinsupp_add }
+  { DFinsupp.equivProdDFinsupp with map_add' := DFinsupp.equivProdDFinsupp_add }
 #align direct_sum.add_equiv_prod_direct_sum DirectSum.addEquivProdDirectSum
 -/
 
@@ -343,17 +343,17 @@ variable {α : ι → Type u} {δ : ∀ i, α i → Type w} [∀ i j, AddCommMon
 /-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.-/
 noncomputable def sigmaCurry : (⨁ i : Σ i, _, δ i.1 i.2) →+ ⨁ (i) (j), δ i j
     where
-  toFun := @Dfinsupp.sigmaCurry _ _ δ _
-  map_zero' := Dfinsupp.sigmaCurry_zero
-  map_add' f g := @Dfinsupp.sigmaCurry_add _ _ δ _ f g
+  toFun := @DFinsupp.sigmaCurry _ _ δ _
+  map_zero' := DFinsupp.sigmaCurry_zero
+  map_add' f g := @DFinsupp.sigmaCurry_add _ _ δ _ f g
 #align direct_sum.sigma_curry DirectSum.sigmaCurry
 -/
 
 #print DirectSum.sigmaCurry_apply /-
 @[simp]
 theorem sigmaCurry_apply (f : ⨁ i : Σ i, _, δ i.1 i.2) (i : ι) (j : α i) :
     sigmaCurry f i j = f ⟨i, j⟩ :=
-  @Dfinsupp.sigmaCurry_apply _ _ δ _ f i j
+  @DFinsupp.sigmaCurry_apply _ _ δ _ f i j
 #align direct_sum.sigma_curry_apply DirectSum.sigmaCurry_apply
 -/
 
@@ -364,9 +364,9 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ i, _, δ i.1 i.2) (i : ι) (j : α i) :
 def sigmaUncurry [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)] :
     (⨁ (i) (j), δ i j) →+ ⨁ i : Σ i, _, δ i.1 i.2
     where
-  toFun := Dfinsupp.sigmaUncurry
-  map_zero' := Dfinsupp.sigmaUncurry_zero
-  map_add' := Dfinsupp.sigmaUncurry_add
+  toFun := DFinsupp.sigmaUncurry
+  map_zero' := DFinsupp.sigmaUncurry_zero
+  map_add' := DFinsupp.sigmaUncurry_add
 #align direct_sum.sigma_uncurry DirectSum.sigmaUncurry
 -/
 
@@ -375,7 +375,7 @@ def sigmaUncurry [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)] :
 @[simp]
 theorem sigmaUncurry_apply [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)]
     (f : ⨁ (i) (j), δ i j) (i : ι) (j : α i) : sigmaUncurry f ⟨i, j⟩ = f i j :=
-  Dfinsupp.sigmaUncurry_apply f i j
+  DFinsupp.sigmaUncurry_apply f i j
 #align direct_sum.sigma_uncurry_apply DirectSum.sigmaUncurry_apply
 -/
 
@@ -384,7 +384,7 @@ theorem sigmaUncurry_apply [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ
 /-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.-/
 noncomputable def sigmaCurryEquiv [∀ i, DecidableEq (α i)] [∀ i j, DecidableEq (δ i j)] :
     (⨁ i : Σ i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j :=
-  { sigmaCurry, Dfinsupp.sigmaCurryEquiv with }
+  { sigmaCurry, DFinsupp.sigmaCurryEquiv with }
 #align direct_sum.sigma_curry_equiv DirectSum.sigmaCurryEquiv
 -/
 

Mathbin/Algebra/DirectSum/Finsupp.lean

@@ -41,15 +41,15 @@ variable (R M) (ι : Type _) [DecidableEq ι]
 copies of M indexed by ι. -/
 def finsuppLEquivDirectSum : (ι →₀ M) ≃ₗ[R] ⨁ i : ι, M :=
   haveI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
-  finsuppLequivDfinsupp R
+  finsuppLequivDFinsupp R
 #align finsupp_lequiv_direct_sum finsuppLEquivDirectSum
 -/
 
 #print finsuppLEquivDirectSum_single /-
 @[simp]
 theorem finsuppLEquivDirectSum_single (i : ι) (m : M) :
     finsuppLEquivDirectSum R M ι (Finsupp.single i m) = DirectSum.lof R ι _ i m :=
-  Finsupp.toDfinsupp_single i m
+  Finsupp.toDFinsupp_single i m
 #align finsupp_lequiv_direct_sum_single finsuppLEquivDirectSum_single
 -/
 
@@ -58,7 +58,7 @@ theorem finsuppLEquivDirectSum_single (i : ι) (m : M) :
 theorem finsuppLEquivDirectSum_symm_lof (i : ι) (m : M) :
     (finsuppLEquivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m :=
   letI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
-  Dfinsupp.toFinsupp_single i m
+  DFinsupp.toFinsupp_single i m
 #align finsupp_lequiv_direct_sum_symm_lof finsuppLEquivDirectSum_symm_lof
 -/