bump to nightly-2023-11-01-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Combinatorics/Catalan.lean

@@ -199,8 +199,8 @@ def treesOfNumNodesEq : ℕ → Finset (Tree Unit)
   | 0 => {nil}
   | n + 1 =>
     (Finset.Nat.antidiagonal n).attach.biUnion fun ijh =>
-      have := Nat.lt_succ_of_le (fst_le ijh.2)
-      have := Nat.lt_succ_of_le (snd_le ijh.2)
+      have := Nat.lt_succ_of_le (Finset.antidiagonal.fst_le ijh.2)
+      have := Nat.lt_succ_of_le (Finset.antidiagonal.snd_le ijh.2)
       pairwiseNode (trees_of_num_nodes_eq ijh.1.1) (trees_of_num_nodes_eq ijh.1.2)
 #align tree.trees_of_num_nodes_eq Tree.treesOfNumNodesEq
 -/

Mathbin/Combinatorics/Composition.lean

@@ -849,26 +849,26 @@ theorem sum_take_map_length_splitWrtComposition (l : List α) (c : Composition l
 #align list.sum_take_map_length_split_wrt_composition List.sum_take_map_length_splitWrtComposition
 -/
 
-#print List.nthLe_splitWrtCompositionAux /-
-theorem nthLe_splitWrtCompositionAux (l : List α) (ns : List ℕ) {i : ℕ} (hi) :
+#print List.get_splitWrtCompositionAux /-
+theorem get_splitWrtCompositionAux (l : List α) (ns : List ℕ) {i : ℕ} (hi) :
     nthLe (l.splitWrtCompositionAux ns) i hi =
       (l.take (ns.take (i + 1)).Sum).drop (ns.take i).Sum :=
   by
   induction' ns with n ns IH generalizing l i; · cases hi
   cases i <;> simp [IH]
   rw [add_comm n, drop_add, drop_take]
-#align list.nth_le_split_wrt_composition_aux List.nthLe_splitWrtCompositionAux
+#align list.nth_le_split_wrt_composition_aux List.get_splitWrtCompositionAux
 -/
 
-#print List.nthLe_splitWrtComposition /-
+#print List.get_splitWrtComposition' /-
 /-- The `i`-th sublist in the splitting of a list `l` along a composition `c`, is the slice of `l`
 between the indices `c.size_up_to i` and `c.size_up_to (i+1)`, i.e., the indices in the `i`-th
 block of the composition. -/
-theorem nthLe_splitWrtComposition (l : List α) (c : Composition n) {i : ℕ}
+theorem get_splitWrtComposition' (l : List α) (c : Composition n) {i : ℕ}
     (hi : i < (l.splitWrtComposition c).length) :
     nthLe (l.splitWrtComposition c) i hi = (l.take (c.sizeUpTo (i + 1))).drop (c.sizeUpTo i) :=
-  nthLe_splitWrtCompositionAux _ _ _
-#align list.nth_le_split_wrt_composition List.nthLe_splitWrtComposition
+  get_splitWrtCompositionAux _ _ _
+#align list.nth_le_split_wrt_composition List.get_splitWrtComposition'
 -/
 
 #print List.join_splitWrtCompositionAux /-

Mathbin/Data/Finset/NatAntidiagonal.lean

@@ -28,21 +28,17 @@ namespace Finset
 
 namespace Nat
 
-#print Finset.Nat.antidiagonal /-
 /-- The antidiagonal of a natural number `n` is
     the finset of pairs `(i, j)` such that `i + j = n`. -/
 def antidiagonal (n : ℕ) : Finset (ℕ × ℕ) :=
   ⟨Multiset.Nat.antidiagonal n, Multiset.Nat.nodup_antidiagonal n⟩
 #align finset.nat.antidiagonal Finset.Nat.antidiagonal
--/
 
-#print Finset.Nat.mem_antidiagonal /-
 /-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
 @[simp]
 theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n := by
   rw [antidiagonal, mem_def, Multiset.Nat.mem_antidiagonal]
 #align finset.nat.mem_antidiagonal Finset.Nat.mem_antidiagonal
--/
 
 #print Finset.Nat.card_antidiagonal /-
 /-- The cardinality of the antidiagonal of `n` is `n + 1`. -/
@@ -101,44 +97,44 @@ theorem antidiagonal_succ_succ' {n : ℕ} :
 #align finset.nat.antidiagonal_succ_succ' Finset.Nat.antidiagonal_succ_succ'
 -/
 
-#print Finset.Nat.map_swap_antidiagonal /-
-theorem map_swap_antidiagonal {n : ℕ} :
+#print Finset.map_swap_antidiagonal /-
+theorem Finset.map_swap_antidiagonal {n : ℕ} :
     (antidiagonal n).map ⟨Prod.swap, Prod.swap_rightInverse.Injective⟩ = antidiagonal n :=
   eq_of_veq <| by simp [antidiagonal, Multiset.Nat.map_swap_antidiagonal]
-#align finset.nat.map_swap_antidiagonal Finset.Nat.map_swap_antidiagonal
+#align finset.nat.map_swap_antidiagonal Finset.map_swap_antidiagonal
 -/
 
-#print Finset.Nat.antidiagonal_congr /-
+#print Finset.antidiagonal_congr /-
 /-- A point in the antidiagonal is determined by its first co-ordinate. -/
-theorem antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ antidiagonal n)
+theorem Finset.antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ antidiagonal n)
     (hq : q ∈ antidiagonal n) : p = q ↔ p.fst = q.fst :=
   by
   refine' ⟨congr_arg Prod.fst, fun h => Prod.ext h ((add_right_inj q.fst).mp _)⟩
   rw [mem_antidiagonal] at hp hq 
   rw [hq, ← h, hp]
-#align finset.nat.antidiagonal_congr Finset.Nat.antidiagonal_congr
+#align finset.nat.antidiagonal_congr Finset.antidiagonal_congr
 -/
 
-#print Finset.Nat.antidiagonal.fst_le /-
-theorem antidiagonal.fst_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.1 ≤ n :=
+#print Finset.antidiagonal.fst_le /-
+theorem Finset.antidiagonal.fst_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.1 ≤ n :=
   by
   rw [le_iff_exists_add]
   use kl.2
   rwa [mem_antidiagonal, eq_comm] at hlk 
-#align finset.nat.antidiagonal.fst_le Finset.Nat.antidiagonal.fst_le
+#align finset.nat.antidiagonal.fst_le Finset.antidiagonal.fst_le
 -/
 
-#print Finset.Nat.antidiagonal.snd_le /-
-theorem antidiagonal.snd_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n :=
+#print Finset.antidiagonal.snd_le /-
+theorem Finset.antidiagonal.snd_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n :=
   by
   rw [le_iff_exists_add]
   use kl.1
   rwa [mem_antidiagonal, eq_comm, add_comm] at hlk 
-#align finset.nat.antidiagonal.snd_le Finset.Nat.antidiagonal.snd_le
+#align finset.nat.antidiagonal.snd_le Finset.antidiagonal.snd_le
 -/
 
-#print Finset.Nat.filter_fst_eq_antidiagonal /-
-theorem filter_fst_eq_antidiagonal (n m : ℕ) :
+#print Finset.filter_fst_eq_antidiagonal /-
+theorem Finset.filter_fst_eq_antidiagonal (n m : ℕ) :
     filter (fun x : ℕ × ℕ => x.fst = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅ :=
   by
   ext ⟨x, y⟩
@@ -148,26 +144,26 @@ theorem filter_fst_eq_antidiagonal (n m : ℕ) :
   · rw [not_le] at h 
     simp only [not_mem_empty, iff_false_iff, not_and]
     exact fun hn => ne_of_lt (lt_of_le_of_lt (le_self_add.trans hn.le) h)
-#align finset.nat.filter_fst_eq_antidiagonal Finset.Nat.filter_fst_eq_antidiagonal
+#align finset.nat.filter_fst_eq_antidiagonal Finset.filter_fst_eq_antidiagonal
 -/
 
-#print Finset.Nat.filter_snd_eq_antidiagonal /-
-theorem filter_snd_eq_antidiagonal (n m : ℕ) :
+#print Finset.filter_snd_eq_antidiagonal /-
+theorem Finset.filter_snd_eq_antidiagonal (n m : ℕ) :
     filter (fun x : ℕ × ℕ => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅ :=
   by
   have : (fun x : ℕ × ℕ => x.snd = m) ∘ Prod.swap = fun x : ℕ × ℕ => x.fst = m := by ext; simp
   rw [← map_swap_antidiagonal]
   simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
-#align finset.nat.filter_snd_eq_antidiagonal Finset.Nat.filter_snd_eq_antidiagonal
+#align finset.nat.filter_snd_eq_antidiagonal Finset.filter_snd_eq_antidiagonal
 -/
 
 section EquivProd
 
-#print Finset.Nat.sigmaAntidiagonalEquivProd /-
+#print Finset.sigmaAntidiagonalEquivProd /-
 /-- The disjoint union of antidiagonals `Σ (n : ℕ), antidiagonal n` is equivalent to the product
     `ℕ × ℕ`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`. -/
 @[simps]
-def sigmaAntidiagonalEquivProd : (Σ n : ℕ, antidiagonal n) ≃ ℕ × ℕ
+def Finset.sigmaAntidiagonalEquivProd : (Σ n : ℕ, antidiagonal n) ≃ ℕ × ℕ
     where
   toFun x := x.2
   invFun x := ⟨x.1 + x.2, x, mem_antidiagonal.mpr rfl⟩
@@ -176,7 +172,7 @@ def sigmaAntidiagonalEquivProd : (Σ n : ℕ, antidiagonal n) ≃ ℕ × ℕ
     rw [mem_antidiagonal] at h 
     exact Sigma.subtype_ext h rfl
   right_inv x := rfl
-#align finset.nat.sigma_antidiagonal_equiv_prod Finset.Nat.sigmaAntidiagonalEquivProd
+#align finset.nat.sigma_antidiagonal_equiv_prod Finset.sigmaAntidiagonalEquivProd
 -/
 
 end EquivProd

Mathbin/Data/Finsupp/Antidiagonal.lean

@@ -38,33 +38,29 @@ def antidiagonal' (f : α →₀ ℕ) : (α →₀ ℕ) × (α →₀ ℕ) →
 #align finsupp.antidiagonal' Finsupp.antidiagonal'
 -/
 
-#print Finsupp.antidiagonal /-
 /-- The antidiagonal of `s : α →₀ ℕ` is the finset of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)`
 such that `t₁ + t₂ = s`. -/
 def antidiagonal (f : α →₀ ℕ) : Finset ((α →₀ ℕ) × (α →₀ ℕ)) :=
   f.antidiagonal'.support
 #align finsupp.antidiagonal Finsupp.antidiagonal
--/
 
-#print Finsupp.mem_antidiagonal /-
 @[simp]
 theorem mem_antidiagonal {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
     p ∈ antidiagonal f ↔ p.1 + p.2 = f :=
   by
   rcases p with ⟨p₁, p₂⟩
   simp [antidiagonal, antidiagonal', ← and_assoc, ← finsupp.to_multiset.apply_eq_iff_eq]
 #align finsupp.mem_antidiagonal Finsupp.mem_antidiagonal
--/
 
-#print Finsupp.swap_mem_antidiagonal /-
 theorem swap_mem_antidiagonal {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
     f.symm ∈ antidiagonal n ↔ f ∈ antidiagonal n := by
   simp only [mem_antidiagonal, add_comm, Prod.swap]
 #align finsupp.swap_mem_antidiagonal Finsupp.swap_mem_antidiagonal
--/
 
-#print Finsupp.antidiagonal_filter_fst_eq /-
-theorem antidiagonal_filter_fst_eq (f g : α →₀ ℕ)
+/- warning: finsupp.antidiagonal_filter_fst_eq clashes with finset.nat.filter_fst_eq_antidiagonal -> Finset.filter_fst_eq_antidiagonal
+Case conversion may be inaccurate. Consider using '#align finsupp.antidiagonal_filter_fst_eq Finset.filter_fst_eq_antidiagonalₓ'. -/
+#print Finset.filter_fst_eq_antidiagonal /-
+theorem filter_fst_eq_antidiagonal (f g : α →₀ ℕ)
     [D : ∀ p : (α →₀ ℕ) × (α →₀ ℕ), Decidable (p.1 = g)] :
     ((antidiagonal f).filterₓ fun p => p.1 = g) = if g ≤ f then {(g, f - g)} else ∅ :=
   by
@@ -74,11 +70,13 @@ theorem antidiagonal_filter_fst_eq (f g : α →₀ ℕ)
   rintro rfl; constructor
   · rintro rfl; exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
   · rintro ⟨h, rfl⟩; exact add_tsub_cancel_of_le h
-#align finsupp.antidiagonal_filter_fst_eq Finsupp.antidiagonal_filter_fst_eq
+#align finsupp.antidiagonal_filter_fst_eq Finset.filter_fst_eq_antidiagonal
 -/
 
-#print Finsupp.antidiagonal_filter_snd_eq /-
-theorem antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
+/- warning: finsupp.antidiagonal_filter_snd_eq clashes with finset.nat.filter_snd_eq_antidiagonal -> Finset.filter_snd_eq_antidiagonal
+Case conversion may be inaccurate. Consider using '#align finsupp.antidiagonal_filter_snd_eq Finset.filter_snd_eq_antidiagonalₓ'. -/
+#print Finset.filter_snd_eq_antidiagonal /-
+theorem filter_snd_eq_antidiagonal (f g : α →₀ ℕ)
     [D : ∀ p : (α →₀ ℕ) × (α →₀ ℕ), Decidable (p.2 = g)] :
     ((antidiagonal f).filterₓ fun p => p.2 = g) = if g ≤ f then {(f - g, g)} else ∅ :=
   by
@@ -88,7 +86,7 @@ theorem antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
   rintro rfl; constructor
   · rintro rfl; exact ⟨le_add_left le_rfl, (add_tsub_cancel_right _ _).symm⟩
   · rintro ⟨h, rfl⟩; exact tsub_add_cancel_of_le h
-#align finsupp.antidiagonal_filter_snd_eq Finsupp.antidiagonal_filter_snd_eq
+#align finsupp.antidiagonal_filter_snd_eq Finset.filter_snd_eq_antidiagonal
 -/
 
 #print Finsupp.antidiagonal_zero /-

Mathbin/Data/Sym/Sym2.lean

@@ -729,15 +729,12 @@ end SymEquiv
 
 section Decidable
 
-#print Sym2.relBool /-
 /-- An algorithm for computing `sym2.rel`.
 -/
 def relBool [DecidableEq α] (x y : α × α) : Bool :=
   if x.1 = y.1 then x.2 = y.2 else if x.1 = y.2 then x.2 = y.1 else false
 #align sym2.rel_bool Sym2.relBool
--/
 
-#print Sym2.relBool_spec /-
 theorem relBool_spec [DecidableEq α] (x y : α × α) : ↥(relBool x y) ↔ Rel α x y :=
   by
   cases' x with x₁ x₂; cases' y with y₁ y₂
@@ -748,7 +745,6 @@ theorem relBool_spec [DecidableEq α] (x y : α × α) : ↥(relBool x y) ↔ Re
     · subst h1 <;> apply Sym2.Rel.swap
     · cases h1 <;> cc
 #align sym2.rel_bool_spec Sym2.relBool_spec
--/
 
 /-- Given `[decidable_eq α]` and `[fintype α]`, the following instance gives `fintype (sym2 α)`.
 -/

Mathbin/RingTheory/PowerSeries/Basic.lean

@@ -2715,7 +2715,7 @@ theorem X_pow_order_dvd (h : (order φ).Dom) : X ^ (order φ).get h ∣ φ :=
   refine' ⟨PowerSeries.mk fun n => coeff R (n + (order φ).get h) φ, _⟩
   ext n
   simp only [coeff_mul, coeff_X_pow, coeff_mk, boole_mul, Finset.sum_ite,
-    Finset.Nat.filter_fst_eq_antidiagonal, Finset.sum_const_zero, add_zero]
+    Finset.filter_fst_eq_antidiagonal, Finset.sum_const_zero, add_zero]
   split_ifs with hn hn
   · simp [tsub_add_cancel_of_le hn]
   · simp only [Finset.sum_empty]

Mathbin/Topology/Algebra/InfiniteSum/Ring.lean

@@ -249,7 +249,7 @@ variable [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α}
 theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal :
     (Summable fun x : ℕ × ℕ => f x.1 * g x.2) ↔
       Summable fun x : Σ n : ℕ, Nat.antidiagonal n => f (x.2 : ℕ × ℕ).1 * g (x.2 : ℕ × ℕ).2 :=
-  Nat.sigmaAntidiagonalEquivProd.summable_iff.symm
+  Finset.sigmaAntidiagonalEquivProd.summable_iff.symm
 #align summable_mul_prod_iff_summable_mul_sigma_antidiagonal summable_mul_prod_iff_summable_mul_sigma_antidiagonal
 -/
 

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "a057bbbfed5a00b825b9d93a02a9f59e7d815d4a",
+    "rev": "f5130f6316c5b9fd4b9e1f645aa7814c394d3552",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "a057bbbfed5a00b825b9d93a02a9f59e7d815d4a",
+    "inputRev?": "f5130f6316c5b9fd4b9e1f645aa7814c394d3552",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "41b0e9c7f0d1ab669a24a957b1bd07886fd13749",
+    "rev": "85a1f28fbf7e973dd67fb9f1f27ee50fccd148fc",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "41b0e9c7f0d1ab669a24a957b1bd07886fd13749",
+    "inputRev?": "85a1f28fbf7e973dd67fb9f1f27ee50fccd148fc",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",

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-10-31-06"
+def tag : String := "nightly-2023-11-01-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a057bbbfed5a00b825b9d93a02a9f59e7d815d4a"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f5130f6316c5b9fd4b9e1f645aa7814c394d3552"
 
 @[default_target]
 lean_lib Mathbin where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.2.0