bump to nightly-2023-03-21-00

mathlib commit leanprover-community/mathlib@7ec2946

Mathbin/Algebra/BigOperators/Finsupp.lean

@@ -943,6 +943,12 @@ theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 :
     exact h2
 #align finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.prod_dvd_prod_of_subset_of_dvd
 
+/- warning: finsupp.indicator_eq_sum_single -> Finsupp.indicator_eq_sum_single is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {M : Type.{u2}} [_inst_4 : AddCommMonoid.{u2} M] (s : Finset.{u1} α) (f : forall (a : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) -> M), Eq.{max (succ u1) (succ u2)} (Finsupp.{u1, u2} α M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4)))) (Finsupp.indicator.{u1, u2} α M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4))) s f) (Finset.sum.{max u1 u2, u1} (Finsupp.{u1, u2} α M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4)))) (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) (Finsupp.addCommMonoid.{u1, u2} α M _inst_4) (Finset.attach.{u1} α s) (fun (x : Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) => Finsupp.single.{u1, u2} α M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4))) ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (HasLiftT.mk.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (CoeTCₓ.coe.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeBase.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeSubtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s))))) x) (f ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (HasLiftT.mk.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (CoeTCₓ.coe.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeBase.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeSubtype.{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.{u1}} {M : Type.{u2}} [_inst_4 : AddCommMonoid.{u2} M] (s : Finset.{u1} α) (f : forall (a : α), (Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) a s) -> M), Eq.{max (succ u1) (succ u2)} (Finsupp.{u1, u2} α M (AddMonoid.toZero.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4))) (Finsupp.indicator.{u1, u2} α M (AddMonoid.toZero.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4)) s f) (Finset.sum.{max u2 u1, u1} (Finsupp.{u1, u2} α M (AddMonoid.toZero.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4))) (Subtype.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s)) (Finsupp.addCommMonoid.{u1, u2} α M _inst_4) (Finset.attach.{u1} α s) (fun (x : Subtype.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s)) => Finsupp.single.{u1, u2} α M (AddMonoid.toZero.{u2} M (AddCommMonoid.toAddMonoid.{u2} M _inst_4)) (Subtype.val.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x) (f (Subtype.val.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x) (Subtype.property.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x))))
+Case conversion may be inaccurate. Consider using '#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_singleₓ'. -/
 theorem indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) :
     indicator s f = ∑ x in s.attach, single x (f x x.2) :=
   by
@@ -953,6 +959,12 @@ theorem indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈
   rw [not_mem_support_iff.mp hi, single_zero]
 #align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_single
 
+/- warning: finsupp.prod_indicator_index -> Finsupp.prod_indicator_index is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {M : Type.{u2}} {N : Type.{u3}} [_inst_4 : Zero.{u2} M] [_inst_5 : CommMonoid.{u3} N] {s : Finset.{u1} α} (f : forall (a : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) -> M) {h : α -> M -> N}, (forall (a : α), (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a s) -> (Eq.{succ u3} N (h a (OfNat.ofNat.{u2} M 0 (OfNat.mk.{u2} M 0 (Zero.zero.{u2} M _inst_4)))) (OfNat.ofNat.{u3} N 1 (OfNat.mk.{u3} N 1 (One.one.{u3} N (MulOneClass.toHasOne.{u3} N (Monoid.toMulOneClass.{u3} N (CommMonoid.toMonoid.{u3} N _inst_5)))))))) -> (Eq.{succ u3} N (Finsupp.prod.{u1, u2, u3} α M N _inst_4 _inst_5 (Finsupp.indicator.{u1, u2} α M _inst_4 s f) h) (Finset.prod.{u3, u1} N (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) _inst_5 (Finset.attach.{u1} α s) (fun (x : Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) => h ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (HasLiftT.mk.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (CoeTCₓ.coe.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeBase.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeSubtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s))))) x) (f ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (HasLiftT.mk.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (CoeTCₓ.coe.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeBase.{succ u1, succ u1} (Subtype.{succ u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) x s)) α (coeSubtype.{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.{u1}} {M : Type.{u3}} {N : Type.{u2}} [_inst_4 : Zero.{u3} M] [_inst_5 : CommMonoid.{u2} N] {s : Finset.{u1} α} (f : forall (a : α), (Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) a s) -> M) {h : α -> M -> N}, (forall (a : α), (Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) a s) -> (Eq.{succ u2} N (h a (OfNat.ofNat.{u3} M 0 (Zero.toOfNat0.{u3} M _inst_4))) (OfNat.ofNat.{u2} N 1 (One.toOfNat1.{u2} N (Monoid.toOne.{u2} N (CommMonoid.toMonoid.{u2} N _inst_5)))))) -> (Eq.{succ u2} N (Finsupp.prod.{u1, u3, u2} α M N _inst_4 _inst_5 (Finsupp.indicator.{u1, u3} α M _inst_4 s f) h) (Finset.prod.{u2, u1} N (Subtype.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s)) _inst_5 (Finset.attach.{u1} α s) (fun (x : Subtype.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s)) => h (Subtype.val.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x) (f (Subtype.val.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x) (Subtype.property.{succ u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Finset.{u1} α) (Finset.instMembershipFinset.{u1} α) x s) x)))))
+Case conversion may be inaccurate. Consider using '#align finsupp.prod_indicator_index Finsupp.prod_indicator_indexₓ'. -/
 @[simp, to_additive]
 theorem prod_indicator_index [Zero M] [CommMonoid N] {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N}
     (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s f).Prod h = ∏ x in s.attach, h x (f x x.2) :=

Mathbin/Data/Finsupp/Defs.lean

@@ -454,6 +454,12 @@ theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α)
     single (f x) y (f z) = single x y z := by classical simp only [single_apply, hf.eq_iff]
 #align finsupp.single_apply_left Finsupp.single_apply_left
 
+/- warning: finsupp.single_eq_set_indicator -> Finsupp.single_eq_set_indicator is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {M : Type.{u2}} [_inst_1 : Zero.{u2} M] {a : α} {b : M}, Eq.{max (succ u1) (succ u2)} (α -> M) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (Finsupp.{u1, u2} α M _inst_1) (fun (_x : Finsupp.{u1, u2} α M _inst_1) => α -> M) (Finsupp.coeFun.{u1, u2} α M _inst_1) (Finsupp.single.{u1, u2} α M _inst_1 a b)) (Set.indicator.{u1, u2} α M _inst_1 (Singleton.singleton.{u1, u1} α (Set.{u1} α) (Set.hasSingleton.{u1} α) a) (fun (_x : α) => b))
+but is expected to have type
+  forall {α : Type.{u2}} {M : Type.{u1}} [_inst_1 : Zero.{u1} M] {a : α} {b : M}, Eq.{max (succ u2) (succ u1)} (forall (ᾰ : α), (fun (x._@.Mathlib.Data.Finsupp.Defs._hyg.779 : α) => M) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Finsupp.{u2, u1} α M _inst_1) α (fun (_x : α) => (fun (x._@.Mathlib.Data.Finsupp.Defs._hyg.779 : α) => M) _x) (Finsupp.funLike.{u2, u1} α M _inst_1) (Finsupp.single.{u2, u1} α M _inst_1 a b)) (Set.indicator.{u2, u1} α M _inst_1 (Singleton.singleton.{u2, u2} α (Set.{u2} α) (Set.instSingletonSet.{u2} α) a) (fun (_x : α) => b))
+Case conversion may be inaccurate. Consider using '#align finsupp.single_eq_set_indicator Finsupp.single_eq_set_indicatorₓ'. -/
 theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by
   classical
     ext

Mathbin/Data/Finsupp/Indicator.lean

@@ -118,7 +118,7 @@ theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s :=
 lean 3 declaration is
   forall {ι : Type.{u1}} {α : Type.{u2}} [_inst_1 : Zero.{u2} α] (i : ι) (b : α), Eq.{max (succ u1) (succ u2)} (Finsupp.{u1, u2} ι α _inst_1) (Finsupp.single.{u1, u2} ι α _inst_1 i b) (Finsupp.indicator.{u1, u2} ι α _inst_1 (Singleton.singleton.{u1, u1} ι (Finset.{u1} ι) (Finset.hasSingleton.{u1} ι) i) (fun (_x : ι) (_x : Membership.Mem.{u1, u1} ι (Finset.{u1} ι) (Finset.hasMem.{u1} ι) _x (Singleton.singleton.{u1, u1} ι (Finset.{u1} ι) (Finset.hasSingleton.{u1} ι) i)) => b))
 but is expected to have type
-  forall {ι : Type.{u2}} {α : Type.{u1}} [_inst_1 : Zero.{u1} α] {i : ι} {b : α}, Eq.{max (succ u2) (succ u1)} (forall (a : ι), (fun (x._@.Mathlib.Data.Finsupp.Defs._hyg.779 : ι) => α) a) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Finsupp.{u2, u1} ι α _inst_1) ι (fun (a : ι) => (fun (x._@.Mathlib.Data.Finsupp.Defs._hyg.779 : ι) => α) a) (Finsupp.funLike.{u2, u1} ι α _inst_1) (Finsupp.single.{u2, u1} ι α _inst_1 i b)) (Set.indicator.{u2, u1} ι α _inst_1 (Singleton.singleton.{u2, u2} ι (Set.{u2} ι) (Set.instSingletonSet.{u2} ι) i) (fun (_x : ι) => b))
+  forall {ι : Type.{u2}} {α : Type.{u1}} [_inst_1 : Zero.{u1} α] (i : ι) (b : α), Eq.{max (succ u2) (succ u1)} (Finsupp.{u2, u1} ι α _inst_1) (Finsupp.single.{u2, u1} ι α _inst_1 i b) (Finsupp.indicator.{u2, u1} ι α _inst_1 (Singleton.singleton.{u2, u2} ι (Finset.{u2} ι) (Finset.instSingletonFinset.{u2} ι) i) (fun (_x : ι) (_x : Membership.mem.{u2, u2} ι (Finset.{u2} ι) (Finset.instMembershipFinset.{u2} ι) _x (Singleton.singleton.{u2, u2} ι (Finset.{u2} ι) (Finset.instSingletonFinset.{u2} ι) i)) => b))
 Case conversion may be inaccurate. Consider using '#align finsupp.single_eq_indicator Finsupp.single_eq_indicatorₓ'. -/
 theorem single_eq_indicator (i : ι) (b : α) : single i b = indicator {i} fun _ _ => b := by
   classical

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "bc44317f5fd1814f6e0207de17587b48d12dedd9",
+    "rev": "5097133e02ec1006a96cc6eb1496ace8797ade16",
     "name": "lean3port",
-    "inputRev?": "bc44317f5fd1814f6e0207de17587b48d12dedd9"}},
+    "inputRev?": "5097133e02ec1006a96cc6eb1496ace8797ade16"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "f411c38bb48177c7d2ea8f45c0540a41aa7f9d25",
+    "rev": "aa0f33a524d745d7dac130aaa4bc62a6db8a01b7",
     "name": "mathlib",
-    "inputRev?": "f411c38bb48177c7d2ea8f45c0540a41aa7f9d25"}},
+    "inputRev?": "aa0f33a524d745d7dac130aaa4bc62a6db8a01b7"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-20-22"
+def tag : String := "nightly-2023-03-21-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"bc44317f5fd1814f6e0207de17587b48d12dedd9"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5097133e02ec1006a96cc6eb1496ace8797ade16"
 
 @[default_target]
 lean_lib Mathbin where