bump to nightly-2024-04-24-08

mathlib commit leanprover-community/mathlib@65a1391

Archive/Imo/Imo1962Q1.lean

@@ -50,7 +50,7 @@ theorem without_digits {n : ℕ} (h1 : ProblemPredicate n) : ∃ c : ℕ, Proble
   · have h2 : ¬problem_predicate 0 := by norm_num [problem_predicate]
     contradiction
   · rw [problem_predicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,
-      List.concat_eq_append'] at h1
+      List.concat_eq_append] at h1
     constructor
     · rw [← h1.left, div_add_mod (n + 1) 10]
     · rw [← h1.right, of_digits_append, of_digits_digits, of_digits_singleton, add_comm, mul_comm]

Mathbin/Algebra/Group/Nat.lean

@@ -105,12 +105,12 @@ protected theorem Nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n :=
 #align nat.nsmul_eq_mul Nat.nsmul_eq_mul
 -/
 
-#print Nat.cancelCommMonoidWithZero /-
-instance Nat.cancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ :=
+#print Nat.instCancelCommMonoidWithZero /-
+instance Nat.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ :=
   { Nat.commSemiring with
     hMul_left_cancel_of_ne_zero := fun _ _ _ h1 h2 =>
       Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zero h1) h2 }
-#align nat.cancel_comm_monoid_with_zero Nat.cancelCommMonoidWithZero
+#align nat.cancel_comm_monoid_with_zero Nat.instCancelCommMonoidWithZero
 -/
 
 attribute [simp] Nat.not_lt_zero Nat.succ_ne_zero Nat.succ_ne_self Nat.zero_ne_one Nat.one_ne_zero

Mathbin/Algebra/Group/ULift.lean

@@ -221,7 +221,7 @@ theorem down_intCast [IntCast α] (n : ℤ) : down (n : ULift α) = n :=
 #print ULift.addMonoidWithOne /-
 instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (ULift α) :=
   { ULift.one, ULift.addMonoid,
-    ULift.natCast with
+    ULift.instNatCast with
     natCast_zero := congr_arg ULift.up Nat.cast_zero
     natCast_succ := fun n => congr_arg ULift.up (Nat.cast_succ _) }
 #align ulift.add_monoid_with_one ULift.addMonoidWithOne

Mathbin/Algebra/Order/Group/Nat.lean

@@ -26,15 +26,15 @@ universe u v
 /-! ### instances -/
 
 
-#print Nat.orderBot /-
-instance Nat.orderBot : OrderBot ℕ where
+#print Nat.instOrderBot /-
+instance Nat.instOrderBot : OrderBot ℕ where
   bot := 0
   bot_le := Nat.zero_le
-#align nat.order_bot Nat.orderBot
+#align nat.order_bot Nat.instOrderBot
 -/
 
 instance : LinearOrderedCommSemiring ℕ :=
-  { Nat.commSemiring, Nat.linearOrder with
+  { Nat.commSemiring, Nat.instLinearOrder with
     lt := Nat.lt
     add_le_add_left := @Nat.add_le_add_left
     le_of_add_le_add_left := @Nat.le_of_add_le_add_left
@@ -71,7 +71,7 @@ instance : LinearOrderedCancelAddCommMonoid ℕ :=
   inferInstance
 
 instance : CanonicallyOrderedCommSemiring ℕ :=
-  { Nat.nontrivial, Nat.orderBot, (inferInstance : OrderedAddCommMonoid ℕ),
+  { Nat.nontrivial, Nat.instOrderBot, (inferInstance : OrderedAddCommMonoid ℕ),
     (inferInstance : LinearOrderedSemiring ℕ),
     (inferInstance :
       CommSemiring
@@ -81,7 +81,7 @@ instance : CanonicallyOrderedCommSemiring ℕ :=
     eq_zero_or_eq_zero_of_mul_eq_zero := fun a b => Nat.eq_zero_of_mul_eq_zero }
 
 instance : CanonicallyLinearOrderedAddCommMonoid ℕ :=
-  { (inferInstance : CanonicallyOrderedAddCommMonoid ℕ), Nat.linearOrder with }
+  { (inferInstance : CanonicallyOrderedAddCommMonoid ℕ), Nat.instLinearOrder with }
 
 variable {a b m n k l : ℕ}
 

Mathbin/Computability/TuringMachine.lean

@@ -352,7 +352,7 @@ def ListBlank.nth {Γ} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) : Γ :=
       cases' lt_or_le _ _ with h h; · rw [List.getI_append _ _ _ h]
       rw [List.getI_eq_default _ h]
       cases' le_or_lt _ _ with h₂ h₂; · rw [List.getI_eq_default _ h₂]
-      rw [List.getI_eq_nthLe _ h₂, List.nthLe_append_right h, List.nthLe_replicate])
+      rw [List.getI_eq_get _ h₂, List.nthLe_append_right h, List.nthLe_replicate])
 #align turing.list_blank.nth Turing.ListBlank.nth
 -/
 
@@ -404,10 +404,10 @@ theorem ListBlank.ext {Γ} [Inhabited Γ] {L₁ L₂ : ListBlank Γ} :
       cases' lt_or_le i l₁.length with h' h'
       ·
         simp only [List.nthLe_append _ h', List.nthLe_get? h, List.nthLe_get? h', ←
-          List.getI_eq_nthLe _ h, ← List.getI_eq_nthLe _ h', H]
+          List.getI_eq_get _ h, ← List.getI_eq_get _ h', H]
       ·
         simp only [List.nthLe_append_right h', List.nthLe_replicate, List.nthLe_get? h,
-          List.get?_len_le h', ← List.getI_eq_default _ h', H, List.getI_eq_nthLe _ h]
+          List.get?_len_le h', ← List.getI_eq_default _ h', H, List.getI_eq_get _ h]
 #align turing.list_blank.ext Turing.ListBlank.ext
 -/
 
@@ -3040,7 +3040,7 @@ theorem tr_respects_aux₂ {k q v} {S : ∀ k, List (Γ k)} {L : ListBlank (∀
     · subst k';
       split_ifs <;> simp only [List.reverse_cons, Function.update_same, list_blank.nth_mk, List.map]
       ·
-        rw [List.getI_eq_nthLe, List.nthLe_append_right] <;>
+        rw [List.getI_eq_get, List.nthLe_append_right] <;>
           simp only [h, List.nthLe_singleton, List.length_map, List.length_reverse, Nat.succ_pos',
             List.length_append, lt_add_iff_pos_right, List.length]
       rw [← proj_map_nth, hL, list_blank.nth_mk]

Mathbin/Data/List/Basic.lean

@@ -550,10 +550,10 @@ theorem subset_append_of_subset_left (l l₁ l₂ : List α) : l ⊆ l₁ → l
 #align list.subset_append_of_subset_left List.subset_append_of_subset_left
 -/
 
-#print List.subset_append_of_subset_right' /-
-theorem subset_append_of_subset_right' (l l₁ l₂ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ := fun s =>
+#print List.subset_append_of_subset_right /-
+theorem subset_append_of_subset_right (l l₁ l₂ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ := fun s =>
   Subset.trans s <| subset_append_right _ _
-#align list.subset_append_of_subset_right List.subset_append_of_subset_right'
+#align list.subset_append_of_subset_right List.subset_append_of_subset_right
 -/
 
 #print List.cons_subset /-
@@ -1006,11 +1006,11 @@ theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l
 #align list.concat_cons List.concat_cons
 -/
 
-#print List.concat_eq_append' /-
+#print List.concat_eq_append /-
 @[simp]
-theorem concat_eq_append' (a : α) (l : List α) : concat l a = l ++ [a] := by
+theorem concat_eq_append (a : α) (l : List α) : concat l a = l ++ [a] := by
   induction l <;> simp only [*, concat] <;> constructor <;> rfl
-#align list.concat_eq_append List.concat_eq_append'
+#align list.concat_eq_append List.concat_eq_append
 -/
 
 #print List.init_eq_of_concat_eq /-
@@ -1041,10 +1041,10 @@ theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l
 #align list.concat_append List.concat_append
 -/
 
-#print List.length_concat' /-
-theorem length_concat' (a : α) (l : List α) : length (concat l a) = succ (length l) := by
+#print List.length_concat /-
+theorem length_concat (a : α) (l : List α) : length (concat l a) = succ (length l) := by
   simp only [concat_eq_append, length_append, length]
-#align list.length_concat List.length_concat'
+#align list.length_concat List.length_concat
 -/
 
 #print List.append_concat /-
@@ -2264,8 +2264,8 @@ theorem nthLe_cons_length (x : α) (xs : List α) (n : ℕ) (h : n = xs.length)
 #align list.nth_le_cons_length List.nthLe_cons_length
 -/
 
-#print List.take_one_drop_eq_of_lt_length' /-
-theorem take_one_drop_eq_of_lt_length' {l : List α} {n : ℕ} (h : n < l.length) :
+#print List.take_one_drop_eq_of_lt_length /-
+theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length) :
     (l.drop n).take 1 = [l.nthLe n h] :=
   by
   induction' l with x l ih generalizing n
@@ -2274,7 +2274,7 @@ theorem take_one_drop_eq_of_lt_length' {l : List α} {n : ℕ} (h : n < l.length
     · subst h₁; rw [nth_le_singleton]; simp [lt_succ_iff] at h; subst h; simp
     have h₂ := h; rw [length_cons, Nat.lt_succ_iff, le_iff_eq_or_lt] at h₂
     cases n; · simp; rw [drop, nth_le]; apply ih
-#align list.take_one_drop_eq_of_lt_length List.take_one_drop_eq_of_lt_length'
+#align list.take_one_drop_eq_of_lt_length List.take_one_drop_eq_of_lt_length
 -/
 
 #print List.ext /-
@@ -5826,22 +5826,22 @@ theorem enum_map (l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Pr
 #align list.enum_map List.enum_map
 -/
 
-#print List.nthLe_enumFrom /-
-theorem nthLe_enumFrom (l : List α) (n i : ℕ) (hi' : i < (l.enumFrom n).length)
+#print List.get_enumFrom /-
+theorem get_enumFrom (l : List α) (n i : ℕ) (hi' : i < (l.enumFrom n).length)
     (hi : i < l.length := (by simpa [length_enum_from] using hi')) :
     (l.enumFrom n).nthLe i hi' = (n + i, l.nthLe i hi) :=
   by
   rw [← Option.some_inj, ← nth_le_nth]
   simp [enum_from_nth, nth_le_nth hi]
-#align list.nth_le_enum_from List.nthLe_enumFrom
+#align list.nth_le_enum_from List.get_enumFrom
 -/
 
-#print List.nthLe_enum /-
-theorem nthLe_enum (l : List α) (i : ℕ) (hi' : i < l.enum.length)
+#print List.get_enum /-
+theorem get_enum (l : List α) (i : ℕ) (hi' : i < l.enum.length)
     (hi : i < l.length := (by simpa [length_enum] using hi')) :
     l.enum.nthLe i hi' = (i, l.nthLe i hi) := by convert nth_le_enum_from _ _ _ hi';
   exact (zero_add _).symm
-#align list.nth_le_enum List.nthLe_enum
+#align list.nth_le_enum List.get_enum
 -/
 
 section Choose
@@ -6396,14 +6396,16 @@ theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d :=
   rfl
 #align list.nthd_cons_succ List.getD_cons_succₓ
 
-theorem getD_eq_nthLe {n : ℕ} (hn : n < l.length) : l.getD n d = l.nthLe n hn :=
+#print List.getD_eq_get /-
+theorem getD_eq_get {n : ℕ} (hn : n < l.length) : l.getD n d = l.nthLe n hn :=
   by
   induction' l with hd tl IH generalizing n
   · exact absurd hn (not_lt_of_ge (Nat.zero_le _))
   · cases n
     · exact nthd_cons_zero _ _ _
     · exact IH _
-#align list.nthd_eq_nth_le List.getD_eq_nthLeₓ
+#align list.nthd_eq_nth_le List.getD_eq_get
+-/
 
 theorem getD_eq_default {n : ℕ} (hn : l.length ≤ n) : l.getD n d = d :=
   by
@@ -6481,10 +6483,10 @@ theorem getI_cons_succ : getI (x :: xs) (n + 1) = getI xs n :=
 #align list.inth_cons_succ List.getI_cons_succ
 -/
 
-#print List.getI_eq_nthLe /-
-theorem getI_eq_nthLe {n : ℕ} (hn : n < l.length) : l.getI n = l.nthLe n hn :=
-  getD_eq_nthLe _ _ _
-#align list.inth_eq_nth_le List.getI_eq_nthLe
+#print List.getI_eq_get /-
+theorem getI_eq_get {n : ℕ} (hn : n < l.length) : l.getI n = l.nthLe n hn :=
+  getD_eq_get _ _ _
+#align list.inth_eq_nth_le List.getI_eq_get
 -/
 
 #print List.getI_eq_default /-

Mathbin/Data/List/ToFinsupp.lean

@@ -82,7 +82,7 @@ theorem toFinsupp_support :
 
 #print List.toFinsupp_apply_lt' /-
 theorem toFinsupp_apply_lt' (hn : n < l.length) : l.toFinsupp n = l.nthLe n hn :=
-  getD_eq_nthLe _ _ _
+  getD_eq_get _ _ _
 #align list.to_finsupp_apply_lt List.toFinsupp_apply_lt'
 -/
 

Mathbin/Data/Nat/Nth.lean

@@ -79,7 +79,7 @@ theorem nth_eq_getD_sort (h : (setOf p).Finite) (n : ℕ) :
 #print Nat.nth_eq_orderEmbOfFin /-
 theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFinset.card) :
     nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩ := by
-  rw [nth_eq_nthd_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_nthLe]; rfl
+  rw [nth_eq_nthd_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get]; rfl
 #align nat.nth_eq_order_emb_of_fin Nat.nth_eq_orderEmbOfFin
 -/
 

Mathbin/Order/Filter/FilterProduct.lean

@@ -42,7 +42,7 @@ local notation "β*" => Germ (φ : Filter α) β
 
 instance [DivisionSemiring β] : DivisionSemiring β* :=
   { Germ.semiring, Germ.divInvMonoid,
-    Germ.nontrivial with
+    Germ.instNontrivial with
     mul_inv_cancel := fun f =>
       inductionOn f fun f hf =>
         coe_eq.2 <|
@@ -189,7 +189,7 @@ instance [OrderedCommRing β] : OrderedCommRing β* :=
 
 instance [StrictOrderedSemiring β] : StrictOrderedSemiring β* :=
   { Germ.orderedSemiring, Germ.orderedCancelAddCommMonoid,
-    Germ.nontrivial with
+    Germ.instNontrivial with
     mul_lt_mul_of_pos_left := fun x y z =>
       inductionOn₃ x y z fun f g h hfg hh =>
         coe_lt.2 <| (coe_lt.1 hh).mp <| (coe_lt.1 hfg).mono fun a => mul_lt_mul_of_pos_left

Mathbin/Order/Filter/Germ.lean

@@ -604,11 +604,11 @@ section Ring
 
 variable {R : Type _}
 
-#print Filter.Germ.nontrivial /-
-instance nontrivial [Nontrivial R] [NeBot l] : Nontrivial (Germ l R) :=
+#print Filter.Germ.instNontrivial /-
+instance instNontrivial [Nontrivial R] [NeBot l] : Nontrivial (Germ l R) :=
   let ⟨x, y, h⟩ := exists_pair_ne R
   ⟨⟨↑x, ↑y, mt const_inj.1 h⟩⟩
-#align filter.germ.nontrivial Filter.Germ.nontrivial
+#align filter.germ.nontrivial Filter.Germ.instNontrivial
 -/
 
 instance [MulZeroClass R] : MulZeroClass (Germ l R)
@@ -679,41 +679,41 @@ instance [Monoid M] [MulAction M β] : MulAction M (Germ l β)
   one_smul f := inductionOn f fun f => by norm_cast; simp only [one_smul]
   hMul_smul c₁ c₂ f := inductionOn f fun f => by norm_cast; simp only [mul_smul]
 
-#print Filter.Germ.mulAction' /-
+#print Filter.Germ.instMulAction' /-
 @[to_additive]
-instance mulAction' [Monoid M] [MulAction M β] : MulAction (Germ l M) (Germ l β)
+instance instMulAction' [Monoid M] [MulAction M β] : MulAction (Germ l M) (Germ l β)
     where
   one_smul f := inductionOn f fun f => by simp only [← coe_one, ← coe_smul', one_smul]
   hMul_smul c₁ c₂ f := inductionOn₃ c₁ c₂ f fun c₁ c₂ f => by norm_cast; simp only [mul_smul]
-#align filter.germ.mul_action' Filter.Germ.mulAction'
-#align filter.germ.add_action' Filter.Germ.addAction'
+#align filter.germ.mul_action' Filter.Germ.instMulAction'
+#align filter.germ.add_action' Filter.Germ.instAddAction'
 -/
 
 instance [Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction M (Germ l N)
     where
   smul_add c f g := inductionOn₂ f g fun f g => by norm_cast; simp only [smul_add]
   smul_zero c := by simp only [← coe_zero, ← coe_smul, smul_zero]
 
-#print Filter.Germ.distribMulAction' /-
-instance distribMulAction' [Monoid M] [AddMonoid N] [DistribMulAction M N] :
+#print Filter.Germ.instDistribMulAction' /-
+instance instDistribMulAction' [Monoid M] [AddMonoid N] [DistribMulAction M N] :
     DistribMulAction (Germ l M) (Germ l N)
     where
   smul_add c f g := inductionOn₃ c f g fun c f g => by norm_cast; simp only [smul_add]
   smul_zero c := inductionOn c fun c => by simp only [← coe_zero, ← coe_smul', smul_zero]
-#align filter.germ.distrib_mul_action' Filter.Germ.distribMulAction'
+#align filter.germ.distrib_mul_action' Filter.Germ.instDistribMulAction'
 -/
 
 instance [Semiring R] [AddCommMonoid M] [Module R M] : Module R (Germ l M)
     where
   add_smul c₁ c₂ f := inductionOn f fun f => by norm_cast; simp only [add_smul]
   zero_smul f := inductionOn f fun f => by norm_cast; simp only [zero_smul, coe_zero]
 
-#print Filter.Germ.module' /-
-instance module' [Semiring R] [AddCommMonoid M] [Module R M] : Module (Germ l R) (Germ l M)
+#print Filter.Germ.instModule' /-
+instance instModule' [Semiring R] [AddCommMonoid M] [Module R M] : Module (Germ l R) (Germ l M)
     where
   add_smul c₁ c₂ f := inductionOn₃ c₁ c₂ f fun c₁ c₂ f => by norm_cast; simp only [add_smul]
   zero_smul f := inductionOn f fun f => by simp only [← coe_zero, ← coe_smul', zero_smul]
-#align filter.germ.module' Filter.Germ.module'
+#align filter.germ.module' Filter.Germ.instModule'
 -/
 
 end Module

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "5b96848cc28fea8b782392a020db7a20824d9409",
+   "rev": "e408da18380ef42acf7b8337c6b0536bfac09105",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5b96848cc28fea8b782392a020db7a20824d9409",
+   "inputRev": "e408da18380ef42acf7b8337c6b0536bfac09105",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "df4fde5e5167e06404cc5ca52c01444dadd6b96c",
+   "rev": "b46a6dd515e6a8fd03b7f056f79a793a041a0e0e",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "df4fde5e5167e06404cc5ca52c01444dadd6b96c",
+   "inputRev": "b46a6dd515e6a8fd03b7f056f79a793a041a0e0e",
    "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-2024-04-23-08"
+def tag : String := "nightly-2024-04-24-08"
 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"@"df4fde5e5167e06404cc5ca52c01444dadd6b96c"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b46a6dd515e6a8fd03b7f056f79a793a041a0e0e"
 
 @[default_target]
 lean_lib Mathbin where