bump to nightly-2023-06-21-09

mathlib commit leanprover-community/mathlib@f2ad364

Mathbin/Control/Bitraversable/Basic.lean

@@ -68,9 +68,9 @@ def bisequence {t m} [Bitraversable t] [Applicative m] {α β} : t (m α) (m β)
 
 open Functor
 
-#print IsLawfulBitraversable /-
+#print LawfulBitraversable /-
 /-- Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful. -/
-class IsLawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends
+class LawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends
     LawfulBifunctor t where
   id_bitraverse : ∀ {α β} (x : t α β), bitraverse id.mk id.mk x = id.mk x
   comp_bitraverse :
@@ -85,18 +85,18 @@ class IsLawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t]
     ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
       (η : ApplicativeTransformation F G) {α α' β β'} (f : α → F β) (f' : α' → F β') (x : t α α'),
       η (bitraverse f f' x) = bitraverse (@η _ ∘ f) (@η _ ∘ f') x
-#align is_lawful_bitraversable IsLawfulBitraversable
+#align is_lawful_bitraversable LawfulBitraversable
 -/
 
-export IsLawfulBitraversable (id_bitraverse comp_bitraverse bitraverse_eq_bimap_id)
+export LawfulBitraversable (id_bitraverse comp_bitraverse bitraverse_eq_bimap_id)
 
-open IsLawfulBitraversable
+open LawfulBitraversable
 
 attribute [higher_order bitraverse_id_id] id_bitraverse
 
 attribute [higher_order bitraverse_comp] comp_bitraverse
 
 attribute [higher_order] binaturality bitraverse_eq_bimap_id
 
-export IsLawfulBitraversable (bitraverse_id_id bitraverse_comp)
+export LawfulBitraversable (bitraverse_id_id bitraverse_comp)
 

Mathbin/Control/Bitraversable/Instances.lean

@@ -40,94 +40,116 @@ section
 
 variable {F : Type u → Type u} [Applicative F]
 
+#print Prod.bitraverse /-
 /-- The bitraverse function for `α × β`. -/
 def Prod.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : α × β → F (α' × β')
   | (x, y) => Prod.mk <$> f x <*> f' y
 #align prod.bitraverse Prod.bitraverse
+-/
 
 instance : Bitraversable Prod where bitraverse := @Prod.bitraverse
 
-instance : IsLawfulBitraversable Prod := by
+instance : LawfulBitraversable Prod := by
   constructor <;> intros <;> cases x <;> simp [bitraverse, Prod.bitraverse, functor_norm] <;> rfl
 
 open Functor
 
+#print Sum.bitraverse /-
 /-- The bitraverse function for `α ⊕ β`. -/
 def Sum.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : Sum α β → F (Sum α' β')
   | Sum.inl x => Sum.inl <$> f x
   | Sum.inr x => Sum.inr <$> f' x
 #align sum.bitraverse Sum.bitraverse
+-/
 
 instance : Bitraversable Sum where bitraverse := @Sum.bitraverse
 
-instance : IsLawfulBitraversable Sum := by
+instance : LawfulBitraversable Sum := by
   constructor <;> intros <;> cases x <;> simp [bitraverse, Sum.bitraverse, functor_norm] <;> rfl
 
+#print Const.bitraverse /-
 /-- The bitraverse function for `const`. It throws away the second map. -/
 @[nolint unused_arguments]
 def Const.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : Const α β → F (Const α' β') :=
   f
 #align const.bitraverse Const.bitraverse
+-/
 
+#print Bitraversable.const /-
 instance Bitraversable.const : Bitraversable Const where bitraverse := @Const.bitraverse
 #align bitraversable.const Bitraversable.const
+-/
 
-instance IsLawfulBitraversable.const : IsLawfulBitraversable Const := by
+#print LawfulBitraversable.const /-
+instance LawfulBitraversable.const : LawfulBitraversable Const := by
   constructor <;> intros <;> simp [bitraverse, Const.bitraverse, functor_norm] <;> rfl
-#align is_lawful_bitraversable.const IsLawfulBitraversable.const
+#align is_lawful_bitraversable.const LawfulBitraversable.const
+-/
 
+#print flip.bitraverse /-
 /-- The bitraverse function for `flip`. -/
 def flip.bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : flip t α β → F (flip t α' β') :=
   (bitraverse f' f : t β α → F (t β' α'))
 #align flip.bitraverse flip.bitraverse
+-/
 
+#print Bitraversable.flip /-
 instance Bitraversable.flip : Bitraversable (flip t) where bitraverse := @flip.bitraverse t _
 #align bitraversable.flip Bitraversable.flip
+-/
 
-open IsLawfulBitraversable
+open LawfulBitraversable
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic tactic.apply_assumption -/
-instance IsLawfulBitraversable.flip [IsLawfulBitraversable t] : IsLawfulBitraversable (flip t) := by
-  constructor <;> intros <;> casesm IsLawfulBitraversable t <;>
+#print LawfulBitraversable.flip /-
+instance LawfulBitraversable.flip [LawfulBitraversable t] : LawfulBitraversable (flip t) := by
+  constructor <;> intros <;> casesm LawfulBitraversable t <;>
     run_tac
       tactic.apply_assumption
-#align is_lawful_bitraversable.flip IsLawfulBitraversable.flip
+#align is_lawful_bitraversable.flip LawfulBitraversable.flip
+-/
 
 open Bitraversable Functor
 
+#print Bitraversable.traversable /-
 instance (priority := 10) Bitraversable.traversable {α} : Traversable (t α)
     where traverse := @tsnd t _ _
 #align bitraversable.traversable Bitraversable.traversable
+-/
 
-instance (priority := 10) Bitraversable.isLawfulTraversable [IsLawfulBitraversable t] {α} :
+#print Bitraversable.isLawfulTraversable /-
+instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable t] {α} :
     IsLawfulTraversable (t α) :=
   by
   constructor <;> intros <;> simp [traverse, comp_tsnd, functor_norm]
   · rfl
   · simp [tsnd_eq_snd_id]; rfl
   · simp [tsnd, binaturality, Function.comp, functor_norm]
 #align bitraversable.is_lawful_traversable Bitraversable.isLawfulTraversable
+-/
 
 end
 
-open Bifunctor Traversable IsLawfulTraversable IsLawfulBitraversable
+open Bifunctor Traversable IsLawfulTraversable LawfulBitraversable
 
 open Function (bicompl bicompr)
 
 section Bicompl
 
 variable (F G : Type u → Type u) [Traversable F] [Traversable G]
 
+#print Bicompl.bitraverse /-
 /-- The bitraverse function for `bicompl`. -/
 def Bicompl.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f' : α' → m β') :
     bicompl t F G α α' → m (bicompl t F G β β') :=
   (bitraverse (traverse f) (traverse f') : t (F α) (G α') → m _)
 #align bicompl.bitraverse Bicompl.bitraverse
+-/
 
 instance : Bitraversable (bicompl t F G) where bitraverse := @Bicompl.bitraverse t _ F G _ _
 
-instance [IsLawfulTraversable F] [IsLawfulTraversable G] [IsLawfulBitraversable t] :
-    IsLawfulBitraversable (bicompl t F G) :=
+instance [IsLawfulTraversable F] [IsLawfulTraversable G] [LawfulBitraversable t] :
+    LawfulBitraversable (bicompl t F G) :=
   by
   constructor <;> intros <;>
     simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
@@ -142,15 +164,17 @@ section Bicompr
 
 variable (F : Type u → Type u) [Traversable F]
 
+#print Bicompr.bitraverse /-
 /-- The bitraverse function for `bicompr`. -/
 def Bicompr.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m β) (f' : α' → m β') :
     bicompr F t α α' → m (bicompr F t β β') :=
   (traverse (bitraverse f f') : F (t α α') → m _)
 #align bicompr.bitraverse Bicompr.bitraverse
+-/
 
 instance : Bitraversable (bicompr F t) where bitraverse := @Bicompr.bitraverse t _ F _
 
-instance [IsLawfulTraversable F] [IsLawfulBitraversable t] : IsLawfulBitraversable (bicompr F t) :=
+instance [IsLawfulTraversable 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/Bitraversable/Lemmas.lean

@@ -69,7 +69,7 @@ def tsnd {α α'} (f : α → F α') : t β α → F (t β α') :=
 #align bitraversable.tsnd Bitraversable.tsnd
 -/
 
-variable [IsLawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G]
+variable [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G]
 
 #print Bitraversable.id_tfst /-
 @[higher_order tfst_id]

Mathbin/Control/Random.lean

@@ -65,7 +65,7 @@ def Rand :=
 #align rand Rand
 -/
 
-instance (g : Type) : Uliftable (RandG.{u} g) (RandG.{v} g) :=
+instance (g : Type) : ULiftable (RandG.{u} g) (RandG.{v} g) :=
   @StateT.uliftable' _ _ _ _ _ (Equiv.ulift.trans Equiv.ulift.symm)
 
 open ULift hiding Inhabited
@@ -130,7 +130,7 @@ def random : RandG g α :=
 
 /-- generate an infinite series of random values of type `α` -/
 def randomSeries : RandG g (Stream' α) := do
-  let gen ← Uliftable.up (split g)
+  let gen ← ULiftable.up (split g)
   pure <| Stream'.corecState (Random.random α g) gen
 #align rand.random_series Rand.randomSeries
 
@@ -146,7 +146,7 @@ def randomR [Preorder α] [BoundedRandom α] (x y : α) (h : x ≤ y) : RandG g
 /-- generate an infinite series of random values of type `α` between `x` and `y` inclusive. -/
 def randomSeriesR [Preorder α] [BoundedRandom α] (x y : α) (h : x ≤ y) :
     RandG g (Stream' (x .. y)) := do
-  let gen ← Uliftable.up (split g)
+  let gen ← ULiftable.up (split g)
   pure <| corec_state (BoundedRandom.randomR g x y h) gen
 #align rand.random_series_r Rand.randomSeriesR
 

Mathbin/Control/Uliftable.lean

@@ -43,107 +43,127 @@ universe u₀ u₁ v₀ v₁ v₂ w w₀ w₁
 
 variable {s : Type u₀} {s' : Type u₁} {r r' w w' : Type _}
 
+#print ULiftable /-
 /- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`congr] [] -/
 /-- Given a universe polymorphic type family `M.{u} : Type u₁ → Type
 u₂`, this class convert between instantiations, from
 `M.{u} : Type u₁ → Type u₂` to `M.{v} : Type v₁ → Type v₂` and back -/
-class Uliftable (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) where
+class ULiftable (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) where
   congr {α β} : α ≃ β → f α ≃ g β
-#align uliftable Uliftable
+#align uliftable ULiftable
+-/
 
-namespace Uliftable
+namespace ULiftable
 
+#print ULiftable.up /-
 /-- The most common practical use `uliftable` (together with `up`), this function takes
 `x : M.{u} α` and lifts it to M.{max u v} (ulift.{v} α) -/
 @[reducible]
-def up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [Uliftable f g] {α} :
+def up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α} :
     f α → g (ULift α) :=
-  (Uliftable.congr f g Equiv.ulift.symm).toFun
-#align uliftable.up Uliftable.up
+  (ULiftable.congr f g Equiv.ulift.symm).toFun
+#align uliftable.up ULiftable.up
+-/
 
+#print ULiftable.down /-
 /-- The most common practical use of `uliftable` (together with `up`), this function takes
 `x : M.{max u v} (ulift.{v} α)` and lowers it to `M.{u} α` -/
 @[reducible]
-def down {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [Uliftable f g] {α} :
+def down {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α} :
     g (ULift α) → f α :=
-  (Uliftable.congr f g Equiv.ulift.symm).invFun
-#align uliftable.down Uliftable.down
+  (ULiftable.congr f g Equiv.ulift.symm).invFun
+#align uliftable.down ULiftable.down
+-/
 
+#print ULiftable.adaptUp /-
 /-- convenient shortcut to avoid manipulating `ulift` -/
-def adaptUp (F : Type v₀ → Type v₁) (G : Type max v₀ u₀ → Type u₁) [Uliftable F G] [Monad G] {α β}
+def adaptUp (F : Type v₀ → Type v₁) (G : Type max v₀ u₀ → Type u₁) [ULiftable F G] [Monad G] {α β}
     (x : F α) (f : α → G β) : G β :=
   up x >>= f ∘ ULift.down
-#align uliftable.adapt_up Uliftable.adaptUp
+#align uliftable.adapt_up ULiftable.adaptUp
+-/
 
+#print ULiftable.adaptDown /-
 /-- convenient shortcut to avoid manipulating `ulift` -/
-def adaptDown {F : Type max u₀ v₀ → Type u₁} {G : Type v₀ → Type v₁} [L : Uliftable G F] [Monad F]
+def adaptDown {F : Type max u₀ v₀ → Type u₁} {G : Type v₀ → Type v₁} [L : ULiftable G F] [Monad F]
     {α β} (x : F α) (f : α → G β) : G β :=
   @down.{v₀, v₁, max u₀ v₀} G F L β <| x >>= @up.{v₀, v₁, max u₀ v₀} G F L β ∘ f
-#align uliftable.adapt_down Uliftable.adaptDown
+#align uliftable.adapt_down ULiftable.adaptDown
+-/
 
+#print ULiftable.upMap /-
 /-- map function that moves up universes -/
-def upMap {F : Type u₀ → Type u₁} {G : Type max u₀ v₀ → Type v₁} [inst : Uliftable F G] [Functor G]
+def upMap {F : Type u₀ → Type u₁} {G : Type max u₀ v₀ → Type v₁} [inst : ULiftable F G] [Functor G]
     {α β} (f : α → β) (x : F α) : G β :=
   Functor.map (f ∘ ULift.down) (up x)
-#align uliftable.up_map Uliftable.upMap
+#align uliftable.up_map ULiftable.upMap
+-/
 
+#print ULiftable.downMap /-
 /-- map function that moves down universes -/
-def downMap {F : Type max u₀ v₀ → Type u₁} {G : Type u₀ → Type v₁} [inst : Uliftable G F]
+def downMap {F : Type max u₀ v₀ → Type u₁} {G : Type u₀ → Type v₁} [inst : ULiftable G F]
     [Functor F] {α β} (f : α → β) (x : F α) : G β :=
   down (Functor.map (ULift.up ∘ f) x : F (ULift β))
-#align uliftable.down_map Uliftable.downMap
+#align uliftable.down_map ULiftable.downMap
+-/
 
+#print ULiftable.up_down /-
 @[simp]
-theorem up_down {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [Uliftable f g] {α}
+theorem up_down {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α}
     (x : g (ULift α)) : up (down x : f α) = x :=
-  (Uliftable.congr f g Equiv.ulift.symm).right_inv _
-#align uliftable.up_down Uliftable.up_down
+  (ULiftable.congr f g Equiv.ulift.symm).right_inv _
+#align uliftable.up_down ULiftable.up_down
+-/
 
+#print ULiftable.down_up /-
 @[simp]
-theorem down_up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [Uliftable f g] {α}
+theorem down_up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α}
     (x : f α) : down (up x : g _) = x :=
-  (Uliftable.congr f g Equiv.ulift.symm).left_inv _
-#align uliftable.down_up Uliftable.down_up
+  (ULiftable.congr f g Equiv.ulift.symm).left_inv _
+#align uliftable.down_up ULiftable.down_up
+-/
 
-end Uliftable
+end ULiftable
 
 open ULift
 
-instance : Uliftable id id where congr α β F := F
+instance : ULiftable id id where congr α β F := F
 
 /-- for specific state types, this function helps to create a uliftable instance -/
-def StateT.uliftable' {m : Type u₀ → Type v₀} {m' : Type u₁ → Type v₁} [Uliftable m m']
-    (F : s ≃ s') : Uliftable (StateT s m) (StateT s' m')
+def StateT.uliftable' {m : Type u₀ → Type v₀} {m' : Type u₁ → Type v₁} [ULiftable m m']
+    (F : s ≃ s') : ULiftable (StateT s m) (StateT s' m')
     where congr α β G :=
-    StateT.equiv <| Equiv.piCongr F fun _ => Uliftable.congr _ _ <| Equiv.prodCongr G F
+    StateT.equiv <| Equiv.piCongr F fun _ => ULiftable.congr _ _ <| Equiv.prodCongr G F
 #align state_t.uliftable' StateTₓ.uliftable'
 
-instance {m m'} [Uliftable m m'] : Uliftable (StateT s m) (StateT (ULift s) m') :=
+instance {m m'} [ULiftable m m'] : ULiftable (StateT s m) (StateT (ULift s) m') :=
   StateT.uliftable' Equiv.ulift.symm
 
 /-- for specific reader monads, this function helps to create a uliftable instance -/
-def ReaderT.uliftable' {m m'} [Uliftable m m'] (F : s ≃ s') :
-    Uliftable (ReaderT s m) (ReaderT s' m')
-    where congr α β G := ReaderT.equiv <| Equiv.piCongr F fun _ => Uliftable.congr _ _ G
+def ReaderT.uliftable' {m m'} [ULiftable m m'] (F : s ≃ s') :
+    ULiftable (ReaderT s m) (ReaderT s' m')
+    where congr α β G := ReaderT.equiv <| Equiv.piCongr F fun _ => ULiftable.congr _ _ G
 #align reader_t.uliftable' ReaderTₓ.uliftable'
 
-instance {m m'} [Uliftable m m'] : Uliftable (ReaderT s m) (ReaderT (ULift s) m') :=
+instance {m m'} [ULiftable m m'] : ULiftable (ReaderT s m) (ReaderT (ULift s) m') :=
   ReaderT.uliftable' Equiv.ulift.symm
 
+#print ContT.uliftable' /-
 /-- for specific continuation passing monads, this function helps to create a uliftable instance -/
-def ContT.uliftable' {m m'} [Uliftable m m'] (F : r ≃ r') : Uliftable (ContT r m) (ContT r' m')
-    where congr α β := ContT.equiv (Uliftable.congr _ _ F)
+def ContT.uliftable' {m m'} [ULiftable m m'] (F : r ≃ r') : ULiftable (ContT r m) (ContT r' m')
+    where congr α β := ContT.equiv (ULiftable.congr _ _ F)
 #align cont_t.uliftable' ContT.uliftable'
+-/
 
-instance {s m m'} [Uliftable m m'] : Uliftable (ContT s m) (ContT (ULift s) m') :=
+instance {s m m'} [ULiftable m m'] : ULiftable (ContT s m) (ContT (ULift s) m') :=
   ContT.uliftable' Equiv.ulift.symm
 
 /-- for specific writer monads, this function helps to create a uliftable instance -/
-def WriterT.uliftable' {m m'} [Uliftable m m'] (F : w ≃ w') :
-    Uliftable (WriterT w m) (WriterT w' m')
-    where congr α β G := WriterT.equiv <| Uliftable.congr _ _ <| Equiv.prodCongr G F
+def WriterT.uliftable' {m m'} [ULiftable m m'] (F : w ≃ w') :
+    ULiftable (WriterT w m) (WriterT w' m')
+    where congr α β G := WriterT.equiv <| ULiftable.congr _ _ <| Equiv.prodCongr G F
 #align writer_t.uliftable' WriterTₓ.uliftable'
 
-instance {m m'} [Uliftable m m'] : Uliftable (WriterT s m) (WriterT (ULift s) m') :=
+instance {m m'} [ULiftable m m'] : ULiftable (WriterT s m) (WriterT (ULift s) m') :=
   WriterT.uliftable' Equiv.ulift.symm