bump to nightly-2023-07-01-23

mathlib commit leanprover-community/mathlib@9240e8b

Mathbin/RepresentationTheory/FdRep.lean

@@ -45,10 +45,12 @@ open CategoryTheory
 open CategoryTheory.Limits
 
 /- ./././Mathport/Syntax/Translate/Command.lean:328:31: unsupported: @[derive] abbrev -/
+#print FdRep /-
 /-- The category of finite dimensional `k`-linear representations of a monoid `G`. -/
 abbrev FdRep (k G : Type u) [Field k] [Monoid G] :=
   Action (FGModuleCat.{u} k) (MonCat.of G)
 #align fdRep FdRep
+-/
 
 namespace FdRep
 
@@ -73,37 +75,47 @@ instance (V W : FdRep k G) : FiniteDimensional k (V ⟶ W) :=
   FiniteDimensional.of_injective ((forget₂ (FdRep k G) (FGModuleCat k)).mapLinearMap k)
     (Functor.map_injective _)
 
+#print FdRep.ρ /-
 /-- The monoid homomorphism corresponding to the action of `G` onto `V : fdRep k G`. -/
 def ρ (V : FdRep k G) : G →* V →ₗ[k] V :=
   V.ρ
 #align fdRep.ρ FdRep.ρ
+-/
 
+#print FdRep.isoToLinearEquiv /-
 /-- The underlying `linear_equiv` of an isomorphism of representations. -/
 def isoToLinearEquiv {V W : FdRep k G} (i : V ≅ W) : V ≃ₗ[k] W :=
   FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)
 #align fdRep.iso_to_linear_equiv FdRep.isoToLinearEquiv
+-/
 
+#print FdRep.Iso.conj_ρ /-
 theorem Iso.conj_ρ {V W : FdRep k G} (i : V ≅ W) (g : G) :
     W.ρ g = (FdRep.isoToLinearEquiv i).conj (V.ρ g) :=
   by
   rw [FdRep.isoToLinearEquiv, ← FGModuleCat.Iso.conj_eq_conj, iso.conj_apply]
   rw [iso.eq_inv_comp ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)]
   exact (i.hom.comm g).symm
 #align fdRep.iso.conj_ρ FdRep.Iso.conj_ρ
+-/
 
+#print FdRep.of /-
 /-- Lift an unbundled representation to `fdRep`. -/
 @[simps ρ]
 def of {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
     (ρ : Representation k G V) : FdRep k G :=
   ⟨FGModuleCat.of k V, ρ⟩
 #align fdRep.of FdRep.of
+-/
 
 instance : HasForget₂ (FdRep k G) (Rep k G)
     where forget₂ := (forget₂ (FGModuleCat k) (ModuleCat k)).mapAction (MonCat.of G)
 
+#print FdRep.forget₂_ρ /-
 theorem forget₂_ρ (V : FdRep k G) : ((forget₂ (FdRep k G) (Rep k G)).obj V).ρ = V.ρ := by ext g v;
   rfl
 #align fdRep.forget₂_ρ FdRep.forget₂_ρ
+-/
 
 -- Verify that the monoidal structure is available.
 example : MonoidalCategory (FdRep k G) := by infer_instance
@@ -120,12 +132,15 @@ open scoped Classical
 -- deterministic timeout.
 instance : HasKernels (FdRep k G) := by infer_instance
 
+#print FdRep.finrank_hom_simple_simple /-
 -- Verify that Schur's lemma applies out of the box.
 theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FdRep k G) [Simple V] [Simple W] :
     finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0 :=
   CategoryTheory.finrank_hom_simple_simple k V W
 #align fdRep.finrank_hom_simple_simple FdRep.finrank_hom_simple_simple
+-/
 
+#print FdRep.forget₂HomLinearEquiv /-
 /-- The forgetful functor to `Rep k G` preserves hom-sets and their vector space structure -/
 def forget₂HomLinearEquiv (X Y : FdRep k G) :
     ((forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y) ≃ₗ[k] X ⟶ Y
@@ -137,6 +152,7 @@ def forget₂HomLinearEquiv (X Y : FdRep k G) :
   left_inv _ := by ext; rfl
   right_inv _ := by ext; rfl
 #align fdRep.forget₂_hom_linear_equiv FdRep.forget₂HomLinearEquiv
+-/
 
 end FdRep
 
@@ -168,25 +184,31 @@ variable [FiniteDimensional k V]
 variable (ρV : Representation k G V) (W : FdRep k G)
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print FdRep.dualTensorIsoLinHomAux /-
 /-- Auxiliary definition for `fdRep.dual_tensor_iso_lin_hom`. -/
 noncomputable def dualTensorIsoLinHomAux :
     (FdRep.of ρV.dual ⊗ W).V ≅ (FdRep.of (linHom ρV W.ρ)).V :=
   (dualTensorHomEquiv k V W).toFGModuleCatIso
 #align fdRep.dual_tensor_iso_lin_hom_aux FdRep.dualTensorIsoLinHomAux
+-/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print FdRep.dualTensorIsoLinHom /-
 /-- When `V` and `W` are finite dimensional representations of a group `G`, the isomorphism
 `dual_tensor_hom_equiv k V W` of vector spaces induces an isomorphism of representations. -/
 noncomputable def dualTensorIsoLinHom : FdRep.of ρV.dual ⊗ W ≅ FdRep.of (linHom ρV W.ρ) :=
   by
   apply Action.mkIso (dual_tensor_iso_lin_hom_aux ρV W)
   convert dual_tensor_hom_comm ρV W.ρ
 #align fdRep.dual_tensor_iso_lin_hom FdRep.dualTensorIsoLinHom
+-/
 
+#print FdRep.dualTensorIsoLinHom_hom_hom /-
 @[simp]
 theorem dualTensorIsoLinHom_hom_hom : (dualTensorIsoLinHom ρV W).hom.hom = dualTensorHom k V W :=
   rfl
 #align fdRep.dual_tensor_iso_lin_hom_hom_hom FdRep.dualTensorIsoLinHom_hom_hom
+-/
 
 end FdRep
 

Mathbin/SetTheory/Game/Short.lean

@@ -30,14 +30,17 @@ open scoped PGame
 
 namespace PGame
 
+#print PGame.Short /-
 /-- A short game is a game with a finite set of moves at every turn. -/
 inductive Short : PGame.{u} → Type (u + 1)
   |
   mk :
     ∀ {α β : Type u} {L : α → PGame.{u}} {R : β → PGame.{u}} (sL : ∀ i : α, short (L i))
       (sR : ∀ j : β, short (R j)) [Fintype α] [Fintype β], short ⟨α, β, L, R⟩
 #align pgame.short PGame.Short
+-/
 
+#print PGame.subsingleton_short /-
 instance subsingleton_short : ∀ x : PGame, Subsingleton (Short x)
   | mk xl xr xL xR =>
     ⟨fun a b => by
@@ -49,70 +52,90 @@ instance subsingleton_short : ∀ x : PGame, Subsingleton (Short x)
         apply @Subsingleton.elim _ (subsingleton_short (xR x))⟩
 decreasing_by pgame_wf_tac
 #align pgame.subsingleton_short PGame.subsingleton_short
+-/
 
+#print PGame.Short.mk' /-
 /-- A synonym for `short.mk` that specifies the pgame in an implicit argument. -/
 def Short.mk' {x : PGame} [Fintype x.LeftMoves] [Fintype x.RightMoves]
     (sL : ∀ i : x.LeftMoves, Short (x.moveLeft i))
     (sR : ∀ j : x.RightMoves, Short (x.moveRight j)) : Short x := by
   (cases x; dsimp at *) <;> exact short.mk sL sR
 #align pgame.short.mk' PGame.Short.mk'
+-/
 
 attribute [class] short
 
+#print PGame.fintypeLeft /-
 /-- Extracting the `fintype` instance for the indexing type for Left's moves in a short game.
 This is an unindexed typeclass, so it can't be made a global instance.
 -/
 def fintypeLeft {α β : Type u} {L : α → PGame.{u}} {R : β → PGame.{u}} [S : Short ⟨α, β, L, R⟩] :
     Fintype α := by cases' S with _ _ _ _ _ _ F _; exact F
 #align pgame.fintype_left PGame.fintypeLeft
+-/
 
 attribute [local instance] fintype_left
 
+#print PGame.fintypeLeftMoves /-
 instance fintypeLeftMoves (x : PGame) [S : Short x] : Fintype x.LeftMoves := by cases x; dsimp;
   infer_instance
 #align pgame.fintype_left_moves PGame.fintypeLeftMoves
+-/
 
+#print PGame.fintypeRight /-
 /-- Extracting the `fintype` instance for the indexing type for Right's moves in a short game.
 This is an unindexed typeclass, so it can't be made a global instance.
 -/
 def fintypeRight {α β : Type u} {L : α → PGame.{u}} {R : β → PGame.{u}} [S : Short ⟨α, β, L, R⟩] :
     Fintype β := by cases' S with _ _ _ _ _ _ _ F; exact F
 #align pgame.fintype_right PGame.fintypeRight
+-/
 
 attribute [local instance] fintype_right
 
+#print PGame.fintypeRightMoves /-
 instance fintypeRightMoves (x : PGame) [S : Short x] : Fintype x.RightMoves := by cases x; dsimp;
   infer_instance
 #align pgame.fintype_right_moves PGame.fintypeRightMoves
+-/
 
+#print PGame.moveLeftShort /-
 instance moveLeftShort (x : PGame) [S : Short x] (i : x.LeftMoves) : Short (x.moveLeft i) := by
   cases' S with _ _ _ _ L _ _ _; apply L
 #align pgame.move_left_short PGame.moveLeftShort
+-/
 
+#print PGame.moveLeftShort' /-
 /-- Extracting the `short` instance for a move by Left.
 This would be a dangerous instance potentially introducing new metavariables
 in typeclass search, so we only make it an instance locally.
 -/
 def moveLeftShort' {xl xr} (xL xR) [S : Short (mk xl xr xL xR)] (i : xl) : Short (xL i) := by
   cases' S with _ _ _ _ L _ _ _; apply L
 #align pgame.move_left_short' PGame.moveLeftShort'
+-/
 
 attribute [local instance] move_left_short'
 
+#print PGame.moveRightShort /-
 instance moveRightShort (x : PGame) [S : Short x] (j : x.RightMoves) : Short (x.moveRight j) := by
   cases' S with _ _ _ _ _ R _ _; apply R
 #align pgame.move_right_short PGame.moveRightShort
+-/
 
+#print PGame.moveRightShort' /-
 /-- Extracting the `short` instance for a move by Right.
 This would be a dangerous instance potentially introducing new metavariables
 in typeclass search, so we only make it an instance locally.
 -/
 def moveRightShort' {xl xr} (xL xR) [S : Short (mk xl xr xL xR)] (j : xr) : Short (xR j) := by
   cases' S with _ _ _ _ _ R _ _; apply R
 #align pgame.move_right_short' PGame.moveRightShort'
+-/
 
 attribute [local instance] move_right_short'
 
+#print PGame.short_birthday /-
 theorem short_birthday : ∀ (x : PGame.{u}) [Short x], x.birthday < Ordinal.omega
   | ⟨xl, xr, xL, xR⟩, hs => by
     haveI := hs
@@ -129,48 +152,62 @@ theorem short_birthday : ∀ (x : PGame.{u}) [Short x], x.birthday < Ordinal.ome
     · exact move_left_short' xL xR i
     · exact move_right_short' xL xR i
 #align pgame.short_birthday PGame.short_birthday
+-/
 
+#print PGame.Short.ofIsEmpty /-
 /-- This leads to infinite loops if made into an instance. -/
 def Short.ofIsEmpty {l r xL xR} [IsEmpty l] [IsEmpty r] : Short (mk l r xL xR) :=
   Short.mk isEmptyElim isEmptyElim
 #align pgame.short.of_is_empty PGame.Short.ofIsEmpty
+-/
 
+#print PGame.short0 /-
 instance short0 : Short 0 :=
   Short.ofIsEmpty
 #align pgame.short_0 PGame.short0
+-/
 
+#print PGame.short1 /-
 instance short1 : Short 1 :=
   Short.mk (fun i => by cases i; infer_instance) fun j => by cases j
 #align pgame.short_1 PGame.short1
+-/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print PGame.ListShort /-
 /-- Evidence that every `pgame` in a list is `short`. -/
 inductive ListShort : List PGame.{u} → Type (u + 1)
   | nil : list_short []
   | cons : ∀ (hd : PGame.{u}) [Short hd] (tl : List PGame.{u}) [list_short tl], list_short (hd::tl)
 #align pgame.list_short PGame.ListShort
+-/
 
 attribute [class] list_short
 
 attribute [instance] list_short.nil list_short.cons
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print PGame.listShortNthLe /-
 instance listShortNthLe :
     ∀ (L : List PGame.{u}) [ListShort L] (i : Fin (List.length L)), Short (List.nthLe L i i.is_lt)
   | [], _, n => by exfalso; rcases n with ⟨_, ⟨⟩⟩
   | hd::tl, @list_short.cons _ S _ _, ⟨0, _⟩ => S
   | hd::tl, @list_short.cons _ _ _ S, ⟨n + 1, h⟩ =>
     @list_short_nth_le tl S ⟨n, (add_lt_add_iff_right 1).mp h⟩
 #align pgame.list_short_nth_le PGame.listShortNthLe
+-/
 
+#print PGame.shortOfLists /-
 instance shortOfLists : ∀ (L R : List PGame) [ListShort L] [ListShort R], Short (PGame.ofLists L R)
   | L, R, _, _ => by
     skip; apply short.mk
     · intros; infer_instance
     · intros; apply PGame.listShortNthLe
 #align pgame.short_of_lists PGame.shortOfLists
+-/
 
+#print PGame.shortOfRelabelling /-
 -- where does the subtype.val come from?
 /-- If `x` is a short game, and `y` is a relabelling of `x`, then `y` is also short. -/
 def shortOfRelabelling : ∀ {x y : PGame.{u}} (R : Relabelling x y) (S : Short x), Short y
@@ -183,12 +220,16 @@ def shortOfRelabelling : ∀ {x y : PGame.{u}} (R : Relabelling x y) (S : Short
         (fun i => by rw [← L.right_inv i]; apply short_of_relabelling (rL (L.symm i)) inferInstance)
         fun j => by simpa using short_of_relabelling (rR (R.symm j)) inferInstance
 #align pgame.short_of_relabelling PGame.shortOfRelabelling
+-/
 
+#print PGame.shortNeg /-
 instance shortNeg : ∀ (x : PGame.{u}) [Short x], Short (-x)
   | mk xl xr xL xR, _ => by skip; exact short.mk (fun i => short_neg _) fun i => short_neg _
 decreasing_by pgame_wf_tac
 #align pgame.short_neg PGame.shortNeg
+-/
 
+#print PGame.shortAdd /-
 instance shortAdd : ∀ (x y : PGame.{u}) [Short x] [Short y], Short (x + y)
   | mk xl xr xL xR, mk yl yr yL yR, _, _ => by
     skip
@@ -199,18 +240,26 @@ instance shortAdd : ∀ (x y : PGame.{u}) [Short x] [Short y], Short (x + y)
       · change short (mk xl xr xL xR + _); apply short_add
 decreasing_by pgame_wf_tac
 #align pgame.short_add PGame.shortAdd
+-/
 
+#print PGame.shortNat /-
 instance shortNat : ∀ n : ℕ, Short n
   | 0 => PGame.short0
   | n + 1 => @PGame.shortAdd _ _ (short_nat n) PGame.short1
 #align pgame.short_nat PGame.shortNat
+-/
 
+#print PGame.shortBit0 /-
 instance shortBit0 (x : PGame.{u}) [Short x] : Short (bit0 x) := by dsimp [bit0]; infer_instance
 #align pgame.short_bit0 PGame.shortBit0
+-/
 
+#print PGame.shortBit1 /-
 instance shortBit1 (x : PGame.{u}) [Short x] : Short (bit1 x) := by dsimp [bit1]; infer_instance
 #align pgame.short_bit1 PGame.shortBit1
+-/
 
+#print PGame.leLfDecidable /-
 /-- Auxiliary construction of decidability instances.
 We build `decidable (x ≤ y)` and `decidable (x ⧏ y)` in a simultaneous induction.
 Instances for the two projections separately are provided below.
@@ -238,22 +287,31 @@ def leLfDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤
         apply (@le_lf_decidable _ _ _ _).1 <;> infer_instance
 decreasing_by pgame_wf_tac
 #align pgame.le_lf_decidable PGame.leLfDecidable
+-/
 
+#print PGame.leDecidable /-
 instance leDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ≤ y) :=
   (leLfDecidable x y).1
 #align pgame.le_decidable PGame.leDecidable
+-/
 
+#print PGame.lfDecidable /-
 instance lfDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ⧏ y) :=
   (leLfDecidable x y).2
 #align pgame.lf_decidable PGame.lfDecidable
+-/
 
+#print PGame.ltDecidable /-
 instance ltDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x < y) :=
   And.decidable
 #align pgame.lt_decidable PGame.ltDecidable
+-/
 
+#print PGame.equivDecidable /-
 instance equivDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ≈ y) :=
   And.decidable
 #align pgame.equiv_decidable PGame.equivDecidable
+-/
 
 example : Short 0 := by infer_instance
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "d02e9c50596b1518b38413b9fd1f7a6406ee9e0b",
+    "rev": "6ac5a771ccae5d8f694ce5e65622fb3f2636d362",
     "name": "lean3port",
-    "inputRev?": "d02e9c50596b1518b38413b9fd1f7a6406ee9e0b"}},
+    "inputRev?": "6ac5a771ccae5d8f694ce5e65622fb3f2636d362"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "d055df4832d11e9a165ef37c1bd0de6b867165bb",
+    "rev": "b4a49ec957e2e6e0ca95ae65f92aa9f8212e7f70",
     "name": "mathlib",
-    "inputRev?": "d055df4832d11e9a165ef37c1bd0de6b867165bb"}},
+    "inputRev?": "b4a49ec957e2e6e0ca95ae65f92aa9f8212e7f70"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,