bump to nightly-2023-05-04-02

mathlib commit leanprover-community/mathlib@92c69b7

Mathbin/Algebra/BigOperators/Basic.lean

@@ -140,7 +140,7 @@ theorem prod_eq_multiset_prod [CommMonoid β] (s : Finset α) (f : α → β) :
 lean 3 declaration is
   forall {β : Type.{u1}} {α : Type.{u2}} [_inst_1 : CommMonoid.{u1} β] (s : Finset.{u2} α) (f : α -> β), Eq.{succ u1} β (Finset.prod.{u1, u2} β α _inst_1 s (fun (x : α) => f x)) (Finset.fold.{u2, u1} α β (HMul.hMul.{u1, u1, u1} β β β (instHMul.{u1} β (MulOneClass.toHasMul.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1))))) (CommSemigroup.to_isCommutative.{u1} β (CommMonoid.toCommSemigroup.{u1} β _inst_1)) (Semigroup.to_isAssociative.{u1} β (Monoid.toSemigroup.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1))) (OfNat.ofNat.{u1} β 1 (OfNat.mk.{u1} β 1 (One.one.{u1} β (MulOneClass.toHasOne.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))))) f s)
 but is expected to have type
-  forall {β : Type.{u1}} {α : Type.{u2}} [_inst_1 : CommMonoid.{u1} β] (s : Finset.{u2} α) (f : α -> β), Eq.{succ u1} β (Finset.prod.{u1, u2} β α _inst_1 s (fun (x : α) => f x)) (Finset.fold.{u2, u1} α β (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.3172 : β) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.3174 : β) => HMul.hMul.{u1, u1, u1} β β β (instHMul.{u1} β (MulOneClass.toMul.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.3172 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.3174) (CommSemigroup.to_isCommutative.{u1} β (CommMonoid.toCommSemigroup.{u1} β _inst_1)) (Semigroup.to_isAssociative.{u1} β (Monoid.toSemigroup.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1))) (OfNat.ofNat.{u1} β 1 (One.toOfNat1.{u1} β (Monoid.toOne.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))) f s)
+  forall {β : Type.{u1}} {α : Type.{u2}} [_inst_1 : CommMonoid.{u1} β] (s : Finset.{u2} α) (f : α -> β), Eq.{succ u1} β (Finset.prod.{u1, u2} β α _inst_1 s (fun (x : α) => f x)) (Finset.fold.{u2, u1} α β (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.4358 : β) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.4360 : β) => HMul.hMul.{u1, u1, u1} β β β (instHMul.{u1} β (MulOneClass.toMul.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.4358 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.4360) (CommSemigroup.to_isCommutative.{u1} β (CommMonoid.toCommSemigroup.{u1} β _inst_1)) (Semigroup.to_isAssociative.{u1} β (Monoid.toSemigroup.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1))) (OfNat.ofNat.{u1} β 1 (One.toOfNat1.{u1} β (Monoid.toOne.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))) f s)
 Case conversion may be inaccurate. Consider using '#align finset.prod_eq_fold Finset.prod_eq_foldₓ'. -/
 @[to_additive]
 theorem prod_eq_fold [CommMonoid β] (s : Finset α) (f : α → β) :
@@ -1991,7 +1991,7 @@ theorem eq_prod_range_div' {M : Type _} [CommGroup M] (f : ℕ → M) (n : ℕ)
 lean 3 declaration is
   forall {α : Type.{u1}} [_inst_2 : CanonicallyOrderedAddMonoid.{u1} α] [_inst_3 : Sub.{u1} α] [_inst_4 : OrderedSub.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) (AddZeroClass.toHasAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))))) _inst_3] [_inst_5 : ContravariantClass.{u1, u1} α α (HAdd.hAdd.{u1, u1, u1} α α α (instHAdd.{u1} α (AddZeroClass.toHasAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))))))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))))] {f : Nat -> α}, (Monotone.{0, u1} Nat α (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))) f) -> (forall (n : Nat), Eq.{succ u1} α (Finset.sum.{u1, 0} α Nat (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)) (Finset.range n) (fun (i : Nat) => HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) i (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (f i))) (HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f n) (f (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero))))))
 but is expected to have type
-  forall {α : Type.{u1}} [_inst_2 : CanonicallyOrderedAddMonoid.{u1} α] [_inst_3 : Sub.{u1} α] [_inst_4 : OrderedSub.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) (AddZeroClass.toAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))))) _inst_3] [_inst_5 : ContravariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18749 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18751 : α) => HAdd.hAdd.{u1, u1, u1} α α α (instHAdd.{u1} α (AddZeroClass.toAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18749 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18751) (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18764 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18766 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18764 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.18766)] {f : Nat -> α}, (Monotone.{0, u1} Nat α (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))) f) -> (forall (n : Nat), Eq.{succ u1} α (Finset.sum.{u1, 0} α Nat (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)) (Finset.range n) (fun (i : Nat) => HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) i (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (f i))) (HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f n) (f (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))))
+  forall {α : Type.{u1}} [_inst_2 : CanonicallyOrderedAddMonoid.{u1} α] [_inst_3 : Sub.{u1} α] [_inst_4 : OrderedSub.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) (AddZeroClass.toAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))))) _inst_3] [_inst_5 : ContravariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19935 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19937 : α) => HAdd.hAdd.{u1, u1, u1} α α α (instHAdd.{u1} α (AddZeroClass.toAdd.{u1} α (AddMonoid.toAddZeroClass.{u1} α (AddCommMonoid.toAddMonoid.{u1} α (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19935 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19937) (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19950 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19952 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19950 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19952)] {f : Nat -> α}, (Monotone.{0, u1} Nat α (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2))) f) -> (forall (n : Nat), Eq.{succ u1} α (Finset.sum.{u1, 0} α Nat (OrderedAddCommMonoid.toAddCommMonoid.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)) (Finset.range n) (fun (i : Nat) => HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) i (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (f i))) (HSub.hSub.{u1, u1, u1} α α α (instHSub.{u1} α _inst_3) (f n) (f (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))))
 Case conversion may be inaccurate. Consider using '#align finset.sum_range_tsub Finset.sum_range_tsubₓ'. -/
 /-- A telescoping sum along `{0, ..., n-1}` of an `ℕ`-valued function
 reduces to the difference of the last and first terms

Mathbin/Algebra/BigOperators/Fin.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.big_operators.fin
-! leanprover-community/mathlib commit cdb01be3c499930fd29be05dce960f4d8d201c54
+! leanprover-community/mathlib commit ef997baa41b5c428be3fb50089a7139bf4ee886b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -448,6 +448,38 @@ theorem partialProd_right_inv {G : Type _} [Group G] (g : G) (f : Fin n → G) (
 #align fin.partial_prod_right_inv Fin.partialProd_right_inv
 #align fin.partial_sum_right_neg Fin.partialSum_right_neg
 
+/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
+If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
+If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
+Useful for defining group cohomology. -/
+@[to_additive
+      "Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.\nThen if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.\nIf `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.\nIf `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`\nUseful for defining group cohomology."]
+theorem inv_partialProd_mul_eq_contractNth {G : Type _} [Group G] (g : Fin (n + 1) → G)
+    (j : Fin (n + 1)) (k : Fin n) :
+    (partialProd g (j.succ.succAbove k.cast_succ))⁻¹ * partialProd g (j.succAbove k).succ =
+      j.contractNth Mul.mul g k :=
+  by
+  have := partial_prod_right_inv (1 : G) g
+  simp only [one_smul, coe_eq_cast_succ] at this
+  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
+  · rwa [succ_above_below, succ_above_below, this, contract_nth_apply_of_lt]
+    · assumption
+    · rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe]
+      exact le_of_lt h
+  · rwa [succ_above_below, succ_above_above, partial_prod_succ, cast_succ_fin_succ, ← mul_assoc,
+      this, contract_nth_apply_of_eq]
+    · simpa only [le_iff_coe_le_coe, ← h]
+    · rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe]
+      exact le_of_eq h
+  · rwa [succ_above_above, succ_above_above, partial_prod_succ, partial_prod_succ,
+      cast_succ_fin_succ, partial_prod_succ, inv_mul_cancel_left, contract_nth_apply_of_gt]
+    · exact le_iff_coe_le_coe.2 (le_of_lt h)
+    · rw [le_iff_coe_le_coe, coe_succ]
+      exact Nat.succ_le_of_lt h
+#align fin.inv_partial_prod_mul_eq_contract_nth Fin.inv_partialProd_mul_eq_contractNth
+#align fin.neg_partial_sum_add_eq_contract_nth Fin.neg_partial_sum_add_eq_contract_nth
+
 end PartialProd
 
 end Fin

Mathbin/Algebra/MonoidAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.monoid_algebra.basic
-! leanprover-community/mathlib commit 2651125b48fc5c170ab1111afd0817c903b1fc6c
+! leanprover-community/mathlib commit f69db8cecc668e2d5894d7e9bfc491da60db3b9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1701,23 +1701,23 @@ instance [Monoid R] [Semiring k] [DistribMulAction R k] :
     DistribMulAction R (AddMonoidAlgebra k G) :=
   Finsupp.distribMulAction G k
 
-instance [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k] [Nonempty G] :
+instance [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
     FaithfulSMul R (AddMonoidAlgebra k G) :=
   Finsupp.faithfulSMul
 
 instance [Semiring R] [Semiring k] [Module R k] : Module R (AddMonoidAlgebra k G) :=
   Finsupp.module G k
 
-instance [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k] [SMul R S]
-    [IsScalarTower R S k] : IsScalarTower R S (AddMonoidAlgebra k G) :=
+instance [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :
+    IsScalarTower R S (AddMonoidAlgebra k G) :=
   Finsupp.isScalarTower G k
 
-instance [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k]
-    [SMulCommClass R S k] : SMulCommClass R S (AddMonoidAlgebra k G) :=
+instance [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
+    SMulCommClass R S (AddMonoidAlgebra k G) :=
   Finsupp.smulCommClass G k
 
-instance [Monoid R] [Semiring k] [DistribMulAction R k] [DistribMulAction Rᵐᵒᵖ k]
-    [IsCentralScalar R k] : IsCentralScalar R (AddMonoidAlgebra k G) :=
+instance [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] :
+    IsCentralScalar R (AddMonoidAlgebra k G) :=
   Finsupp.isCentralScalar G k
 
 /-! It is hard to state the equivalent of `distrib_mul_action G (add_monoid_algebra k G)`