bump to nightly-2023-12-24-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Data/Set/NAry.lean

@@ -301,66 +301,52 @@ theorem image2_congr' (h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s
 #align set.image2_congr' Set.image2_congr'
 -/
 
-#print Set.image3 /-
 /-- The image of a ternary function `f : α → β → γ → δ` as a function
   `set α → set β → set γ → set δ`. Mathematically this should be thought of as the image of the
   corresponding function `α × β × γ → δ`.
 -/
 def image3 (g : α → β → γ → δ) (s : Set α) (t : Set β) (u : Set γ) : Set δ :=
   {d | ∃ a b c, a ∈ s ∧ b ∈ t ∧ c ∈ u ∧ g a b c = d}
 #align set.image3 Set.image3
--/
 
-#print Set.mem_image3 /-
 @[simp]
 theorem mem_image3 : d ∈ image3 g s t u ↔ ∃ a b c, a ∈ s ∧ b ∈ t ∧ c ∈ u ∧ g a b c = d :=
   Iff.rfl
 #align set.mem_image3 Set.mem_image3
--/
 
-#print Set.image3_mono /-
 theorem image3_mono (hs : s ⊆ s') (ht : t ⊆ t') (hu : u ⊆ u') :
     image3 g s t u ⊆ image3 g s' t' u' := fun x =>
   Exists₃.imp fun a b c ⟨ha, hb, hc, hx⟩ => ⟨hs ha, ht hb, hu hc, hx⟩
 #align set.image3_mono Set.image3_mono
--/
 
-#print Set.image3_congr /-
 @[congr]
 theorem image3_congr (h : ∀ a ∈ s, ∀ b ∈ t, ∀ c ∈ u, g a b c = g' a b c) :
     image3 g s t u = image3 g' s t u := by
   ext x
   constructor <;> rintro ⟨a, b, c, ha, hb, hc, rfl⟩ <;>
     exact ⟨a, b, c, ha, hb, hc, by rw [h a ha b hb c hc]⟩
 #align set.image3_congr Set.image3_congr
--/
 
-#print Set.image3_congr' /-
 /-- A common special case of `image3_congr` -/
 theorem image3_congr' (h : ∀ a b c, g a b c = g' a b c) : image3 g s t u = image3 g' s t u :=
   image3_congr fun a _ b _ c _ => h a b c
 #align set.image3_congr' Set.image3_congr'
--/
 
-#print Set.image2_image2_left /-
 theorem image2_image2_left (f : δ → γ → ε) (g : α → β → δ) :
     image2 f (image2 g s t) u = image3 (fun a b c => f (g a b) c) s t u :=
   by
   ext; constructor
   · rintro ⟨_, c, ⟨a, b, ha, hb, rfl⟩, hc, rfl⟩; refine' ⟨a, b, c, ha, hb, hc, rfl⟩
   · rintro ⟨a, b, c, ha, hb, hc, rfl⟩; refine' ⟨_, c, ⟨a, b, ha, hb, rfl⟩, hc, rfl⟩
 #align set.image2_image2_left Set.image2_image2_left
--/
 
-#print Set.image2_image2_right /-
 theorem image2_image2_right (f : α → δ → ε) (g : β → γ → δ) :
     image2 f s (image2 g t u) = image3 (fun a b c => f a (g b c)) s t u :=
   by
   ext; constructor
   · rintro ⟨a, _, ha, ⟨b, c, hb, hc, rfl⟩, rfl⟩; refine' ⟨a, b, c, ha, hb, hc, rfl⟩
   · rintro ⟨a, b, c, ha, hb, hc, rfl⟩; refine' ⟨a, _, ha, ⟨b, c, hb, hc, rfl⟩, rfl⟩
 #align set.image2_image2_right Set.image2_image2_right
--/
 
 #print Set.image_image2 /-
 theorem image_image2 (f : α → β → γ) (g : γ → δ) :

Mathbin/GroupTheory/OrderOfElement.lean

@@ -1192,21 +1192,21 @@ theorem Subgroup.pow_index_mem {G : Type _} [Group G] (H : Subgroup G) [Normal H
 #align add_subgroup.nsmul_index_mem AddSubgroup.nsmul_index_mem
 -/
 
-#print pow_eq_mod_card /-
+#print pow_mod_card /-
 @[to_additive]
-theorem pow_eq_mod_card (n : ℕ) : x ^ n = x ^ (n % Fintype.card G) := by
+theorem pow_mod_card (n : ℕ) : x ^ n = x ^ (n % Fintype.card G) := by
   rw [pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, ← pow_mod_orderOf]
-#align pow_eq_mod_card pow_eq_mod_card
-#align nsmul_eq_mod_card nsmul_eq_mod_card
+#align pow_eq_mod_card pow_mod_card
+#align nsmul_eq_mod_card mod_card_nsmul
 -/
 
-#print zpow_eq_mod_card /-
+#print zpow_mod_card /-
 @[to_additive]
-theorem zpow_eq_mod_card (n : ℤ) : x ^ n = x ^ (n % Fintype.card G) := by
+theorem zpow_mod_card (n : ℤ) : x ^ n = x ^ (n % Fintype.card G) := by
   rw [zpow_mod_orderOf, ← Int.emod_emod_of_dvd n (Int.coe_nat_dvd.2 orderOf_dvd_card), ←
     zpow_mod_orderOf]
-#align zpow_eq_mod_card zpow_eq_mod_card
-#align zsmul_eq_mod_card zsmul_eq_mod_card
+#align zpow_eq_mod_card zpow_mod_card
+#align zsmul_eq_mod_card mod_card_zsmul
 -/
 
 #print powCoprime /-

Mathbin/Order/Filter/NAry.lean

@@ -271,7 +271,6 @@ theorem map₂_right (h : f.ne_bot) : map₂ (fun x y => y) f g = g := by rw [ma
 #align filter.map₂_right Filter.map₂_right
 -/
 
-#print Filter.map₃ /-
 /-- The image of a ternary function `m : α → β → γ → δ` as a function
 `filter α → filter β → filter γ → filter δ`. Mathematically this should be thought of as the image
 of the corresponding function `α × β × γ → δ`. -/
@@ -293,9 +292,7 @@ def map₃ (m : α → β → γ → δ) (f : Filter α) (g : Filter β) (h : Fi
               inter_subset_right _ _).trans
           ht⟩
 #align filter.map₃ Filter.map₃
--/
 
-#print Filter.map₂_map₂_left /-
 theorem map₂_map₂_left (m : δ → γ → ε) (n : α → β → δ) :
     map₂ m (map₂ n f g) h = map₃ (fun a b c => m (n a b) c) f g h :=
   by
@@ -308,9 +305,7 @@ theorem map₂_map₂_left (m : δ → γ → ε) (n : α → β → δ) :
   · rintro ⟨s, t, u, hs, ht, hu, hw⟩
     exact ⟨_, u, image2_mem_map₂ hs ht, hu, by rwa [image2_image2_left]⟩
 #align filter.map₂_map₂_left Filter.map₂_map₂_left
--/
 
-#print Filter.map₂_map₂_right /-
 theorem map₂_map₂_right (m : α → δ → ε) (n : β → γ → δ) :
     map₂ m f (map₂ n g h) = map₃ (fun a b c => m a (n b c)) f g h :=
   by
@@ -323,7 +318,6 @@ theorem map₂_map₂_right (m : α → δ → ε) (n : β → γ → δ) :
   · rintro ⟨s, t, u, hs, ht, hu, hw⟩
     exact ⟨s, _, hs, image2_mem_map₂ ht hu, by rwa [image2_image2_right]⟩
 #align filter.map₂_map₂_right Filter.map₂_map₂_right
--/
 
 #print Filter.map_map₂ /-
 theorem map_map₂ (m : α → β → γ) (n : γ → δ) :

lake-manifest.json

@@ -49,19 +49,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "8f013c457aea2ea1b0156c0c98043c9ed018529f",
+   "rev": "a7fbc9ec101d941ce1e02955a6e130a25d5ab907",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8f013c457aea2ea1b0156c0c98043c9ed018529f",
+   "inputRev": "a7fbc9ec101d941ce1e02955a6e130a25d5ab907",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "3e3e70bcfa7ce2e56f0d330db07db13679a9f045",
+   "rev": "2b7a6e07d8a20fb48753a949ba61b3c111bf4dee",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3e3e70bcfa7ce2e56f0d330db07db13679a9f045",
+   "inputRev": "2b7a6e07d8a20fb48753a949ba61b3c111bf4dee",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

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-12-23-06"
+def tag : String := "nightly-2023-12-24-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"@"3e3e70bcfa7ce2e56f0d330db07db13679a9f045"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2b7a6e07d8a20fb48753a949ba61b3c111bf4dee"
 
 @[default_target]
 lean_lib Mathbin where