bump to nightly-2023-03-19-20

mathlib commit leanprover-community/mathlib@1f4705c

Mathbin/Algebra/BigOperators/Ring.lean

@@ -138,7 +138,7 @@ variable [CommSemiring β]
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : CommSemiring.{u2} β] {δ : α -> Type.{u3}} [_inst_2 : DecidableEq.{succ u1} α] [_inst_3 : forall (a : α), DecidableEq.{succ u3} (δ a)] {s : Finset.{u1} α} {t : forall (a : α), Finset.{u3} (δ a)} {f : forall (a : α), (δ a) -> β}, Eq.{succ u2} β (Finset.prod.{u2, u1} β α (CommSemiring.toCommMonoid.{u2} β _inst_1) s (fun (a : α) => Finset.sum.{u2, u3} β (δ a) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u2} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} β (Semiring.toNonAssocSemiring.{u2} β (CommSemiring.toSemiring.{u2} β _inst_1)))) (t a) (fun (b : δ a) => f a b))) (Finset.sum.{u2, max u1 u3} β (forall (a : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) -> (δ a)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u2} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} β (Semiring.toNonAssocSemiring.{u2} β (CommSemiring.toSemiring.{u2} β _inst_1)))) (Finset.pi.{u1, u3} α (fun (a : α) => δ a) (fun (a : α) (b : α) => _inst_2 a b) s t) (fun (p : forall (a : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) -> (δ a)) => Finset.prod.{u2, u1} β (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) (CommSemiring.toCommMonoid.{u2} β _inst_1) (Finset.attach.{u1} α s) (fun (x : Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) => f (Subtype.val.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s) x) (p (Subtype.val.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s) x) (Subtype.property.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s) x)))))
 but is expected to have type
-  forall {α : Type.{u2}} {β : Type.{u3}} [_inst_1 : CommSemiring.{u3} β] {δ : α -> Type.{u1}} [_inst_2 : DecidableEq.{succ u2} α] [_inst_3 : forall (a : α), DecidableEq.{succ u1} (δ a)] {s : Finset.{u2} α} {t : forall (a : α), Finset.{u1} (δ a)} {f : forall (a : α), (δ a) -> β}, Eq.{succ u3} β (Finset.prod.{u3, u2} β α (CommSemiring.toCommMonoid.{u3} β _inst_1) s (fun (a : α) => Finset.sum.{u3, u1} β (δ a) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} β (Semiring.toNonAssocSemiring.{u3} β (CommSemiring.toSemiring.{u3} β _inst_1)))) (t a) (fun (b : δ a) => f a b))) (Finset.sum.{u3, max u2 u1} β (forall (a : α), (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) -> (δ a)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} β (Semiring.toNonAssocSemiring.{u3} β (CommSemiring.toSemiring.{u3} β _inst_1)))) (Finset.pi.{u2, u1} α (fun (a : α) => δ a) (fun (a : α) (b : α) => _inst_2 a b) s t) (fun (p : forall (a : α), (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) -> (δ a)) => Finset.prod.{u3, u2} β (Subtype.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s)) (CommSemiring.toCommMonoid.{u3} β _inst_1) (Finset.attach.{u2} α s) (fun (x : Subtype.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s)) => f (Subtype.val.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x) (p (Subtype.val.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x) (Subtype.property.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x)))))
+  forall {α : Type.{u2}} {β : Type.{u3}} [_inst_1 : CommSemiring.{u3} β] {δ : α -> Type.{u1}} [_inst_2 : DecidableEq.{succ u2} α] [_inst_3 : forall (a : α), DecidableEq.{succ u1} (δ a)] {s : Finset.{u2} α} {t : forall (a : α), Finset.{u1} (δ a)} {f : forall (a : α), (δ a) -> β}, Eq.{succ u3} β (Finset.prod.{u3, u2} β α (CommSemiring.toCommMonoid.{u3} β _inst_1) s (fun (a : α) => Finset.sum.{u3, u1} β (δ a) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} β (Semiring.toNonAssocSemiring.{u3} β (CommSemiring.toSemiring.{u3} β _inst_1)))) (t a) (fun (b : δ a) => f a b))) (Finset.sum.{u3, max u2 u1} β (forall (a : α), (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) -> (δ a)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} β (Semiring.toNonAssocSemiring.{u3} β (CommSemiring.toSemiring.{u3} β _inst_1)))) (Finset.pi.{u1, u2} α (fun (a : α) => δ a) (fun (a : α) (b : α) => _inst_2 a b) s t) (fun (p : forall (a : α), (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a s) -> (δ a)) => Finset.prod.{u3, u2} β (Subtype.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s)) (CommSemiring.toCommMonoid.{u3} β _inst_1) (Finset.attach.{u2} α s) (fun (x : Subtype.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s)) => f (Subtype.val.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x) (p (Subtype.val.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x) (Subtype.property.{succ u2} α (fun (x : α) => Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) x s) x)))))
 Case conversion may be inaccurate. Consider using '#align finset.prod_sum Finset.prod_sumₓ'. -/
 /-- The product over a sum can be written as a sum over the product of sets, `finset.pi`.
   `finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/