bump to nightly-2023-07-06-21

mathlib commit leanprover-community/mathlib@5dc6092

Mathbin/Algebra/Free.lean

@@ -360,7 +360,7 @@ theorem mul_map_seq (x y : FreeMagma α) :
 -/
 
 @[to_additive]
-instance : IsLawfulTraversable FreeMagma.{u} :=
+instance : LawfulTraversable FreeMagma.{u} :=
   {
     FreeMagma.lawfulMonad with
     id_traverse := fun α x =>
@@ -954,7 +954,7 @@ theorem mul_map_seq (x y : FreeSemigroup α) :
 -/
 
 @[to_additive]
-instance : IsLawfulTraversable FreeSemigroup.{u} :=
+instance : LawfulTraversable FreeSemigroup.{u} :=
   {
     FreeSemigroup.lawfulMonad with
     id_traverse := fun α x =>

Mathbin/Control/Bitraversable/Instances.lean

@@ -122,7 +122,7 @@ instance (priority := 10) Bitraversable.traversable {α} : Traversable (t α)
 
 #print Bitraversable.isLawfulTraversable /-
 instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable t] {α} :
-    IsLawfulTraversable (t α) :=
+    LawfulTraversable (t α) :=
   by
   constructor <;> intros <;> simp [traverse, comp_tsnd, functor_norm]
   · rfl
@@ -133,7 +133,7 @@ instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable
 
 end
 
-open Bifunctor Traversable IsLawfulTraversable LawfulBitraversable
+open Bifunctor Traversable LawfulTraversable LawfulBitraversable
 
 open Function (bicompl bicompr)
 
@@ -151,7 +151,7 @@ def Bicompl.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f'
 
 instance : Bitraversable (bicompl t F G) where bitraverse := @Bicompl.bitraverse t _ F G _ _
 
-instance [IsLawfulTraversable F] [IsLawfulTraversable G] [LawfulBitraversable t] :
+instance [LawfulTraversable F] [LawfulTraversable G] [LawfulBitraversable t] :
     LawfulBitraversable (bicompl t F G) :=
   by
   constructor <;> intros <;>
@@ -177,7 +177,7 @@ def Bicompr.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f'
 
 instance : Bitraversable (bicompr F t) where bitraverse := @Bicompr.bitraverse t _ F _
 
-instance [IsLawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) :=
+instance [LawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) :=
   by
   constructor <;> intros <;> simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
   · simp [bitraverse_eq_bimap_id', traverse_eq_map_id']; rfl

Mathbin/Control/Fold.lean

@@ -332,9 +332,9 @@ theorem foldl.unop_ofFreeMonoid (f : β → α → β) (xs : FreeMonoid α) (a :
 
 variable (m : Type u → Type u) [Monad m] [LawfulMonad m]
 
-variable {t : Type u → Type u} [Traversable t] [IsLawfulTraversable t]
+variable {t : Type u → Type u} [Traversable t] [LawfulTraversable t]
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 #print Traversable.foldMap_hom /-
 theorem foldMap_hom [Monoid α] [Monoid β] (f : α →* β) (g : γ → α) (x : t γ) :
@@ -358,13 +358,13 @@ end ApplicativeTransformation
 
 section Equalities
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 open List (cons)
 
 variable {α β γ : Type u}
 
-variable {t : Type u → Type u} [Traversable t] [IsLawfulTraversable t]
+variable {t : Type u → Type u} [Traversable t] [LawfulTraversable t]
 
 #print Traversable.foldl.ofFreeMonoid_comp_of /-
 @[simp]

Mathbin/Control/Traversable/Basic.lean

@@ -274,14 +274,14 @@ def sequence [Traversable t] : t (f α) → f (t α) :=
 
 end Functions
 
-#print IsLawfulTraversable /-
+#print LawfulTraversable /-
 /-- A traversable functor is lawful if its `traverse` satisfies a
 number of additional properties.  It must send `id.mk` to `id.mk`,
 send the composition of applicative functors to the composition of the
 `traverse` of each, send each function `f` to `λ x, f <$> x`, and
 satisfy a naturality condition with respect to applicative
 transformations. -/
-class IsLawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
+class LawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
     Type (u + 1) where
   id_traverse : ∀ {α} (x : t α), traverse id.mk x = x
   comp_traverse :
@@ -293,13 +293,13 @@ class IsLawfulTraversable (t : Type u → Type u) [Traversable t] extends Lawful
     ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
       (η : ApplicativeTransformation F G) {α β} (f : α → F β) (x : t α),
       η (traverse f x) = traverse (@η _ ∘ f) x
-#align is_lawful_traversable IsLawfulTraversable
+#align is_lawful_traversable LawfulTraversable
 -/
 
 instance : Traversable id :=
   ⟨fun _ _ _ _ => id⟩
 
-instance : IsLawfulTraversable id := by refine' { .. } <;> intros <;> rfl
+instance : LawfulTraversable id := by refine' { .. } <;> intros <;> rfl
 
 section
 

Mathbin/Control/Traversable/Derive.lean

@@ -395,7 +395,7 @@ unsafe def traversable_law_starter (rs : List simp_arg_type) := do
 #align tactic.interactive.traversable_law_starter tactic.interactive.traversable_law_starter
 
 unsafe def derive_lawful_traversable (pre : Option Name) : tactic Unit := do
-  let q(@IsLawfulTraversable $(f) $(d)) ← target
+  let q(@LawfulTraversable $(f) $(d)) ← target
   let n := f.get_app_fn.const_name
   let eqns ← get_equations_of (.str (with_prefix pre n) "traverse")
   let eqns' ← get_equations_of (.str (with_prefix pre n) "map")
@@ -414,7 +414,7 @@ unsafe def derive_lawful_traversable (pre : Option Name) : tactic Unit := do
             (refl <|> do
               let η ←
                 get_local `η <|> do
-                    let t ← mk_const `` IsLawfulTraversable.naturality >>= infer_type >>= pp
+                    let t ← mk_const `` LawfulTraversable.naturality >>= infer_type >>= pp
                     fail
                         f! "expecting an `applicative_transformation` called `η` in
                           naturality : {t}"
@@ -468,14 +468,14 @@ unsafe def lawful_functor_derive_handler : derive_handler :=
 #align tactic.interactive.lawful_functor_derive_handler tactic.interactive.lawful_functor_derive_handler
 
 unsafe def lawful_traversable_derive_handler' (nspace : Option Name := none) : derive_handler :=
-  higher_order_derive_handler `` IsLawfulTraversable (derive_lawful_traversable nspace)
+  higher_order_derive_handler `` LawfulTraversable (derive_lawful_traversable nspace)
     [traversable_derive_handler' nspace, lawful_functor_derive_handler' nspace] nspace fun n arg =>
     mk_mapp n [arg, none]
 #align tactic.interactive.lawful_traversable_derive_handler' tactic.interactive.lawful_traversable_derive_handler'
 
 @[derive_handler]
 unsafe def lawful_traversable_derive_handler : derive_handler :=
-  guard_class `` IsLawfulTraversable lawful_traversable_derive_handler'
+  guard_class `` LawfulTraversable lawful_traversable_derive_handler'
 #align tactic.interactive.lawful_traversable_derive_handler tactic.interactive.lawful_traversable_derive_handler
 
 end Tactic.Interactive

Mathbin/Control/Traversable/Equiv.lean

@@ -137,7 +137,7 @@ parameter {t t' : Type u → Type u}
 
 parameter (eqv : ∀ α, t α ≃ t' α)
 
-variable [Traversable t] [IsLawfulTraversable t]
+variable [Traversable t] [LawfulTraversable t]
 
 variable {F G : Type u → Type u} [Applicative F] [Applicative G]
 
@@ -147,7 +147,7 @@ variable (η : ApplicativeTransformation F G)
 
 variable {α β γ : Type u}
 
-open IsLawfulTraversable Functor
+open LawfulTraversable Functor
 
 #print Equiv.id_traverse /-
 protected theorem id_traverse (x : t' α) : Equiv.traverse eqv id.mk x = x := by
@@ -181,7 +181,7 @@ protected theorem naturality (f : α → F β) (x : t' α) :
 /-- The fact that `t` is a lawful traversable functor carries over the
 equivalences to `t'`, with the traversable functor structure given by
 `equiv.traversable`. -/
-protected def isLawfulTraversable : @IsLawfulTraversable t' (Equiv.traversable eqv)
+protected def isLawfulTraversable : @LawfulTraversable t' (Equiv.traversable eqv)
     where
   to_lawfulFunctor := @Equiv.lawfulFunctor _ _ eqv _ _
   id_traverse := @Equiv.id_traverse _ _
@@ -203,7 +203,7 @@ protected def isLawfulTraversable' [_i : Traversable t']
     (h₂ :
       ∀ {F : Type u → Type u} [Applicative F],
         ∀ [LawfulApplicative F] {α β} (f : α → F β), traverse f = Equiv.traverse eqv f) :
-    IsLawfulTraversable t' :=
+    LawfulTraversable t' :=
   by
   -- we can't use the same approach as for `is_lawful_functor'` because
     -- h₂ needs a `is_lawful_applicative` assumption

Mathbin/Control/Traversable/Instances.lean

@@ -66,7 +66,7 @@ theorem Option.naturality {α β} (f : α → F β) (x : Option α) :
 
 end Option
 
-instance : IsLawfulTraversable Option :=
+instance : LawfulTraversable Option :=
   { Option.lawfulMonad with
     id_traverse := @Option.id_traverse
     comp_traverse := @Option.comp_traverse
@@ -116,7 +116,7 @@ protected theorem naturality {α β} (f : α → F β) (x : List α) :
 
 open Nat
 
-instance : IsLawfulTraversable.{u} List :=
+instance : LawfulTraversable.{u} List :=
   { List.lawfulMonad with
     id_traverse := @List.id_traverse
     comp_traverse := @List.comp_traverse
@@ -232,7 +232,7 @@ protected theorem naturality {α β} (f : α → F β) (x : Sum σ α) :
 
 end Traverse
 
-instance {σ : Type u} : IsLawfulTraversable.{u} (Sum σ) :=
+instance {σ : Type u} : LawfulTraversable.{u} (Sum σ) :=
   { Sum.lawfulMonad with
     id_traverse := @Sum.id_traverse σ
     comp_traverse := @Sum.comp_traverse σ

Mathbin/Control/Traversable/Lemmas.lean

@@ -28,21 +28,21 @@ Inspired by [The Essence of the Iterator Pattern][gibbons2009].
 
 universe u
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 open Function hiding comp
 
 open Functor
 
-attribute [functor_norm] IsLawfulTraversable.naturality
+attribute [functor_norm] LawfulTraversable.naturality
 
-attribute [simp] IsLawfulTraversable.id_traverse
+attribute [simp] LawfulTraversable.id_traverse
 
 namespace Traversable
 
 variable {t : Type u → Type u}
 
-variable [Traversable t] [IsLawfulTraversable t]
+variable [Traversable t] [LawfulTraversable t]
 
 variable (F G : Type u → Type u)
 

Mathbin/Data/Buffer/Basic.lean

@@ -237,7 +237,7 @@ def listEquivBuffer (α : Type _) : List α ≃ Buffer α := by
 instance : Traversable Buffer :=
   Equiv.traversable listEquivBuffer
 
-instance : IsLawfulTraversable Buffer :=
+instance : LawfulTraversable Buffer :=
   Equiv.isLawfulTraversable listEquivBuffer
 
 /-- A convenience wrapper around `read` that just fails if the index is out of bounds.

Mathbin/Data/Dlist/Instances.lean

@@ -42,7 +42,7 @@ def Std.DList.listEquivDList : List α ≃ Std.DList α := by
 instance : Traversable Std.DList :=
   Equiv.traversable Std.DList.listEquivDList
 
-instance : IsLawfulTraversable Std.DList :=
+instance : LawfulTraversable Std.DList :=
   Equiv.isLawfulTraversable Std.DList.listEquivDList
 
 instance {α} : Inhabited (Std.DList α) :=

Mathbin/Data/LazyList/Basic.lean

@@ -86,7 +86,7 @@ instance : Traversable LazyList
   map := @LazyList.traverse id _
   traverse := @LazyList.traverse
 
-instance : IsLawfulTraversable LazyList :=
+instance : LawfulTraversable LazyList :=
   by
   apply Equiv.isLawfulTraversable' list_equiv_lazy_list <;> intros <;> skip <;> ext
   · induction x; rfl

Mathbin/Data/Multiset/Functor.lean

@@ -37,7 +37,7 @@ theorem fmap_def {α' β'} {s : Multiset α'} (f : α' → β') : f <$> s = s.ma
 
 instance : LawfulFunctor Multiset := by refine' { .. } <;> intros <;> simp
 
-open IsLawfulTraversable CommApplicative
+open LawfulTraversable CommApplicative
 
 variable {F : Type u → Type u} [Applicative F] [CommApplicative F]
 
@@ -97,7 +97,7 @@ instance : LawfulMonad Multiset
 
 open Functor
 
-open Traversable IsLawfulTraversable
+open Traversable LawfulTraversable
 
 #print Multiset.lift_coe /-
 @[simp]
@@ -153,8 +153,7 @@ theorem traverse_map {G : Type _ → Type _} [Applicative G] [CommApplicative G]
 theorem naturality {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G]
     [CommApplicative H] (eta : ApplicativeTransformation G H) {α β : Type _} (f : α → G β)
     (x : Multiset α) : eta (traverse f x) = traverse (@eta _ ∘ f) x :=
-  Quotient.inductionOn x
-    (by intro <;> simp [traverse, IsLawfulTraversable.naturality, functor_norm])
+  Quotient.inductionOn x (by intro <;> simp [traverse, LawfulTraversable.naturality, functor_norm])
 #align multiset.naturality Multiset.naturality
 -/
 

Mathbin/Data/Vector/Basic.lean

@@ -864,7 +864,7 @@ instance : Traversable.{u} (flip Vector n)
   traverse := @Vector.traverse n
   map α β := @Vector.map.{u, u} α β n
 
-instance : IsLawfulTraversable.{u} (flip Vector n)
+instance : LawfulTraversable.{u} (flip Vector n)
     where
   id_traverse := @Vector.id_traverse n
   comp_traverse := @Vector.comp_traverse n

Mathbin/Logic/Equiv/Array.lean

@@ -52,7 +52,7 @@ variable {n : ℕ}
 instance : Traversable (Array' n) :=
   @Equiv.traversable (flip Vector n) _ (fun α => Equiv.vectorEquivArray α n) _
 
-instance : IsLawfulTraversable (Array' n) :=
+instance : LawfulTraversable (Array' n) :=
   @Equiv.isLawfulTraversable (flip Vector n) _ (fun α => Equiv.vectorEquivArray α n) _ _
 
 end Array'

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "0c0acae01188dbc3642f382c1bbacfe9a13c3161",
+    "rev": "deff1dc21c2ad0e79ddedb113db07eb539ac68e2",
     "name": "lean3port",
-    "inputRev?": "0c0acae01188dbc3642f382c1bbacfe9a13c3161"}},
+    "inputRev?": "deff1dc21c2ad0e79ddedb113db07eb539ac68e2"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "717bcc956c3e43f2245bebd39a56a2f419724a14",
+    "rev": "a691787c324b7d55862d3cd5e72d4304a5f6d4aa",
     "name": "mathlib",
-    "inputRev?": "717bcc956c3e43f2245bebd39a56a2f419724a14"}},
+    "inputRev?": "a691787c324b7d55862d3cd5e72d4304a5f6d4aa"}},
   {"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-07-06-19"
+def tag : String := "nightly-2023-07-06-21"
 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"@"0c0acae01188dbc3642f382c1bbacfe9a13c3161"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"deff1dc21c2ad0e79ddedb113db07eb539ac68e2"
 
 @[default_target]
 lean_lib Mathbin where