bump to nightly-2023-05-08-04

mathlib commit leanprover-community/mathlib@08e1d8d

Mathbin/Algebra/BigOperators/Basic.lean

@@ -1544,13 +1544,25 @@ theorem prod_dite_irrel (p : Prop) [Decidable p] (s : Finset α) (f : p → α 
 #align finset.sum_dite_irrel Finset.sum_dite_irrel
 -/
 
+/- warning: finset.prod_pi_mul_single' -> Finset.prod_pi_mulSingle' is a dubious translation:
+lean 3 declaration is
+  forall {β : Type.{u1}} {α : Type.{u2}} [_inst_1 : CommMonoid.{u1} β] [_inst_2 : DecidableEq.{succ u2} α] (a : α) (x : β) (s : Finset.{u2} α), Eq.{succ u1} β (Finset.prod.{u1, u2} β α _inst_1 s (fun (a' : α) => Pi.mulSingle.{u2, u1} α (fun (a : α) => β) (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => MulOneClass.toHasOne.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1))) a x a')) (ite.{succ u1} β (Membership.Mem.{u2, u2} α (Finset.{u2} α) (Finset.hasMem.{u2} α) a s) (Finset.decidableMem.{u2} α (fun (a : α) (b : α) => _inst_2 a b) a s) x (OfNat.ofNat.{u1} β 1 (OfNat.mk.{u1} β 1 (One.one.{u1} β (MulOneClass.toHasOne.{u1} β (Monoid.toMulOneClass.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))))))
+but is expected to have type
+  forall {β : Type.{u1}} {α : Type.{u2}} [_inst_1 : CommMonoid.{u1} β] [_inst_2 : DecidableEq.{succ u2} α] (a : α) (x : β) (s : Finset.{u2} α), Eq.{succ u1} β (Finset.prod.{u1, u2} β α _inst_1 s (fun (a' : α) => Pi.mulSingle.{u2, u1} α (fun (a : α) => β) (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => Monoid.toOne.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)) a x a')) (ite.{succ u1} β (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) (Finset.decidableMem.{u2} α (fun (a : α) (b : α) => _inst_2 a b) a s) x (OfNat.ofNat.{u1} β 1 (One.toOfNat1.{u1} β (Monoid.toOne.{u1} β (CommMonoid.toMonoid.{u1} β _inst_1)))))
+Case conversion may be inaccurate. Consider using '#align finset.prod_pi_mul_single' Finset.prod_pi_mulSingle'ₓ'. -/
 @[simp, to_additive]
-theorem prod_pi_mul_single' [DecidableEq α] (a : α) (x : β) (s : Finset α) :
+theorem prod_pi_mulSingle' [DecidableEq α] (a : α) (x : β) (s : Finset α) :
     (∏ a' in s, Pi.mulSingle a x a') = if a ∈ s then x else 1 :=
   prod_dite_eq' _ _ _
-#align finset.prod_pi_mul_single' Finset.prod_pi_mul_single'
+#align finset.prod_pi_mul_single' Finset.prod_pi_mulSingle'
 #align finset.sum_pi_single' Finset.sum_pi_single'
 
+/- warning: finset.prod_pi_mul_single -> Finset.prod_pi_mulSingle is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {β : α -> Type.{u2}} [_inst_2 : DecidableEq.{succ u1} α] [_inst_3 : forall (a : α), CommMonoid.{u2} (β a)] (a : α) (f : forall (a : α), β a) (s : Finset.{u1} α), Eq.{succ u2} (β a) (Finset.prod.{u2, u1} (β a) α (_inst_3 a) s (fun (a' : α) => Pi.mulSingle.{u1, u2} α (fun (a' : α) => β a') (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => MulOneClass.toHasOne.{u2} (β i) (Monoid.toMulOneClass.{u2} (β i) (CommMonoid.toMonoid.{u2} (β i) (_inst_3 i)))) a' (f a') a)) (ite.{succ u2} (β a) (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) (Finset.decidableMem.{u1} α (fun (a : α) (b : α) => _inst_2 a b) a s) (f a) (OfNat.ofNat.{u2} (β a) 1 (OfNat.mk.{u2} (β a) 1 (One.one.{u2} (β a) (MulOneClass.toHasOne.{u2} (β a) (Monoid.toMulOneClass.{u2} (β a) (CommMonoid.toMonoid.{u2} (β a) (_inst_3 a))))))))
+but is expected to have type
+  forall {α : Type.{u2}} {β : α -> Type.{u1}} [_inst_2 : DecidableEq.{succ u2} α] [_inst_3 : forall (a : α), CommMonoid.{u1} (β a)] (a : α) (f : forall (a : α), β a) (s : Finset.{u2} α), Eq.{succ u1} (β a) (Finset.prod.{u1, u2} (β a) α (_inst_3 a) s (fun (a' : α) => Pi.mulSingle.{u2, u1} α β (fun (a : α) (b : α) => _inst_2 a b) (fun (i : α) => Monoid.toOne.{u1} (β i) (CommMonoid.toMonoid.{u1} (β i) (_inst_3 i))) a' (f a') a)) (ite.{succ u1} (β a) (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) (Finset.decidableMem.{u2} α (fun (a : α) (b : α) => _inst_2 a b) a s) (f a) (OfNat.ofNat.{u1} (β a) 1 (One.toOfNat1.{u1} (β a) (Monoid.toOne.{u1} (β a) (CommMonoid.toMonoid.{u1} (β a) (_inst_3 a))))))
+Case conversion may be inaccurate. Consider using '#align finset.prod_pi_mul_single Finset.prod_pi_mulSingleₓ'. -/
 @[simp, to_additive]
 theorem prod_pi_mulSingle {β : α → Type _} [DecidableEq α] [∀ a, CommMonoid (β a)] (a : α)
     (f : ∀ a, β a) (s : Finset α) :
@@ -1991,7 +2003,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.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)))))
+  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.19930 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19932 : α) => 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.19930 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19932) (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19945 : α) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19947 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommMonoid.toPartialOrder.{u1} α (CanonicallyOrderedAddMonoid.toOrderedAddCommMonoid.{u1} α _inst_2)))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19945 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.19947)] {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
@@ -2372,6 +2384,12 @@ theorem prod_ite_one {f : α → Prop} [DecidablePred f] (hf : (s : Set α).Pair
 #align finset.prod_ite_one Finset.prod_ite_one
 #align finset.sum_ite_zero Finset.sum_ite_zero
 
+/- warning: finset.prod_erase_lt_of_one_lt -> Finset.prod_erase_lt_of_one_lt is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {γ : Type.{u2}} [_inst_2 : DecidableEq.{succ u1} α] [_inst_3 : OrderedCommMonoid.{u2} γ] [_inst_4 : CovariantClass.{u2, u2} γ γ (HMul.hMul.{u2, u2, u2} γ γ γ (instHMul.{u2} γ (MulOneClass.toHasMul.{u2} γ (Monoid.toMulOneClass.{u2} γ (CommMonoid.toMonoid.{u2} γ (OrderedCommMonoid.toCommMonoid.{u2} γ _inst_3)))))) (LT.lt.{u2} γ (Preorder.toLT.{u2} γ (PartialOrder.toPreorder.{u2} γ (OrderedCommMonoid.toPartialOrder.{u2} γ _inst_3))))] {s : Finset.{u1} α} {d : α}, (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) d s) -> (forall {f : α -> γ}, (LT.lt.{u2} γ (Preorder.toLT.{u2} γ (PartialOrder.toPreorder.{u2} γ (OrderedCommMonoid.toPartialOrder.{u2} γ _inst_3))) (OfNat.ofNat.{u2} γ 1 (OfNat.mk.{u2} γ 1 (One.one.{u2} γ (MulOneClass.toHasOne.{u2} γ (Monoid.toMulOneClass.{u2} γ (CommMonoid.toMonoid.{u2} γ (OrderedCommMonoid.toCommMonoid.{u2} γ _inst_3))))))) (f d)) -> (LT.lt.{u2} γ (Preorder.toLT.{u2} γ (PartialOrder.toPreorder.{u2} γ (OrderedCommMonoid.toPartialOrder.{u2} γ _inst_3))) (Finset.prod.{u2, u1} γ α (OrderedCommMonoid.toCommMonoid.{u2} γ _inst_3) (Finset.erase.{u1} α (fun (a : α) (b : α) => _inst_2 a b) s d) (fun (m : α) => f m)) (Finset.prod.{u2, u1} γ α (OrderedCommMonoid.toCommMonoid.{u2} γ _inst_3) s (fun (m : α) => f m))))
+but is expected to have type
+  forall {α : Type.{u2}} {γ : Type.{u1}} [_inst_2 : DecidableEq.{succ u2} α] [_inst_3 : OrderedCommMonoid.{u1} γ] [_inst_4 : CovariantClass.{u1, u1} γ γ (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23803 : γ) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23805 : γ) => HMul.hMul.{u1, u1, u1} γ γ γ (instHMul.{u1} γ (MulOneClass.toMul.{u1} γ (Monoid.toMulOneClass.{u1} γ (CommMonoid.toMonoid.{u1} γ (OrderedCommMonoid.toCommMonoid.{u1} γ _inst_3))))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23803 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23805) (fun (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23818 : γ) (x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23820 : γ) => LT.lt.{u1} γ (Preorder.toLT.{u1} γ (PartialOrder.toPreorder.{u1} γ (OrderedCommMonoid.toPartialOrder.{u1} γ _inst_3))) x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23818 x._@.Mathlib.Algebra.BigOperators.Basic._hyg.23820)] {s : Finset.{u2} α} {d : α}, (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) d s) -> (forall {f : α -> γ}, (LT.lt.{u1} γ (Preorder.toLT.{u1} γ (PartialOrder.toPreorder.{u1} γ (OrderedCommMonoid.toPartialOrder.{u1} γ _inst_3))) (OfNat.ofNat.{u1} γ 1 (One.toOfNat1.{u1} γ (Monoid.toOne.{u1} γ (CommMonoid.toMonoid.{u1} γ (OrderedCommMonoid.toCommMonoid.{u1} γ _inst_3))))) (f d)) -> (LT.lt.{u1} γ (Preorder.toLT.{u1} γ (PartialOrder.toPreorder.{u1} γ (OrderedCommMonoid.toPartialOrder.{u1} γ _inst_3))) (Finset.prod.{u1, u2} γ α (OrderedCommMonoid.toCommMonoid.{u1} γ _inst_3) (Finset.erase.{u2} α (fun (a : α) (b : α) => _inst_2 a b) s d) (fun (m : α) => f m)) (Finset.prod.{u1, u2} γ α (OrderedCommMonoid.toCommMonoid.{u1} γ _inst_3) s (fun (m : α) => f m))))
+Case conversion may be inaccurate. Consider using '#align finset.prod_erase_lt_of_one_lt Finset.prod_erase_lt_of_one_ltₓ'. -/
 @[to_additive]
 theorem prod_erase_lt_of_one_lt {γ : Type _} [DecidableEq α] [OrderedCommMonoid γ]
     [CovariantClass γ γ (· * ·) (· < ·)] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ}