update to Lean 4.28.0-rc1

Author: m4lvin

Pdl/BuildTree.lean

@@ -166,6 +166,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
           have := List.of_concat_eq_concat this
           cases this
           subst_eqs
+          rw! [unload_boxes, LoadFormula.unload]
           grind
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications
@@ -205,6 +206,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
           have := List.of_concat_eq_concat this
           cases this
           subst_eqs
+          rw! [unload_boxes, LoadFormula.unload]
           grind
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications

Pdl/Flip.lean

@@ -315,6 +315,7 @@ lemma LoadedPathRepeat.flip_flip {Hist X} (lpr : LoadedPathRepeat Hist X) :
   rcases lpr with ⟨k, hk⟩
   simp [LoadedPathRepeat.flip]
   rw! [Sequent.map_flip_map_flip, Sequent.flip_flip]
+  rfl
 
 /-- (┛ಠ_ಠ)┛彡┻━┻ -/
 def Tableau.flip {Hist X} : Tableau Hist X → Tableau (Hist.map Sequent.flip) X.flip
@@ -369,6 +370,7 @@ def PathIn.flip {Hist X} {tab : Tableau Hist X} : PathIn tab → PathIn tab.flip
         (by
           have := tail.flip; convert this using 1
           rw! [@Sequent.flip_flip Y]
+          rfl
         )
   | .pdl tail => .pdl tail.flip
 
@@ -396,7 +398,9 @@ lemma PathIn.nodeAt_flip {Hist X} {tab : Tableau Hist X} {e : PathIn tab} :
     simp only [nodeAt, List.map_cons]
     convert rfl
     · rw! (castMode := .all) [@Sequent.flip_flip Y]
+      rfl
     · simp_all
     · rw! (castMode := .all) [@Sequent.flip_flip Y]
+      rfl
     · simp_all
   case pdl => simp_all [PathIn.flip]

Pdl/Game.lean

@@ -289,7 +289,7 @@ lemma not_in_cone_of_move {i g} {p q : g.Pos} (q_in : q ∈ g.moves p) (sI : Str
     · apply Relation.TransGen.trans _ (Relation.TransGen.single m_to_p)
       aesop
   absurd claim
-  exact IsAsymm.asymm p p claim
+  exact Std.Irrefl.irrefl p
 
 lemma same_winner_of_same_in_cone {i g} {sI : Strategy g i} {sJ sJ' : Strategy g (other i)}
     {p : g.Pos}

Pdl/LocalTableau.lean

@@ -1437,7 +1437,7 @@ lemma non_eq_of_ltSequent : lt_Sequent X Y → X ≠ Y := by
   subst X_eq_Y
   absurd lt
   -- This us easy, because DM ordering is irreflexive.
-  have := WellFounded.isIrrefl (instWellFoundedRelationSequent.2)
+  have := WellFounded.irrefl (instWellFoundedRelationSequent.2)
   apply this.1
 
 /-- If `X` is not basic, then for all end nodes `Y` of a
@@ -1451,7 +1451,7 @@ theorem endNodesOf_nonbasic_non_eq {X Y} (lt : LocalTableau X) (X_nonbas : ¬ X.
 -- upstream me / Haitian? ;-)
 lemma IsDershowitzMannaLT.irrefl [Preorder α] [WellFoundedLT α] (X : Multiset α) :
     ¬ Multiset.IsDershowitzMannaLT X X := by
-  apply (WellFounded.isIrrefl (?_)).1
+  apply (WellFounded.irrefl (?_)).1
   exact (@Multiset.instWellFoundedIsDershowitzMannaLT α _ _).2
 
 /-- If a sequent is lower according to the DM-ordering, then they are multiset-different.

Pdl/Soundness.lean

@@ -364,7 +364,7 @@ notation s:arg " <ᶜ " t:arg => before s t
 
 /-- The `<ᶜ` relation is irreflexive. -/
 theorem before.irrefl :
-    IsIrrefl _ (@before X tab) := by
+    Std.Irrefl (@before X tab) := by
   constructor
   intro p
   simp [before]
@@ -383,7 +383,7 @@ theorem before.trans :
 
 /-- The transitive closure of `<ᶜ` (which in fact is the same as `<ᶜ`) is irreflexive. -/
 theorem trans_before.irrefl {X tab} :
-    IsIrrefl _ (Relation.TransGen (@before X tab)) := by
+    Std.Irrefl (Relation.TransGen (@before X tab)) := by
   rw [Relation.transGen_eq_self before.trans]
   exact before.irrefl
 
@@ -394,14 +394,14 @@ theorem before.wellFounded :
 
 /-- The converse of `<ᶜ` is irreflexive. -/
 theorem flip_before.irrefl :
-    IsIrrefl _ (flip (@before X tab)) := by
+    Std.Irrefl (flip (@before X tab)) := by
   constructor
   intro p
   simp [flip, before]
 
 /-- The transtive closure of the converse of `<ᶜ` is irreflexive. -/
 theorem trans_flip_before.irrefl :
-    IsIrrefl _ (Relation.TransGen (flip (@before X tab))) := by
+    Std.Irrefl (Relation.TransGen (flip (@before X tab))) := by
   constructor
   intro p
   rw [Relation.TransGen.flip_iff]

Pdl/TableauPath.lean

@@ -318,7 +318,7 @@ theorem edge.wellFounded : WellFounded (@edge Hist X tab) := by
   rcases this with ⟨nat_wf⟩
   convert nat_wf
 
-instance edge.isAsymm : IsAsymm (PathIn tab) edge := by
+instance edge.isAsymm : @Std.Asymm (PathIn tab) edge := by
   constructor
   apply WellFounded.asymmetric edge.wellFounded
 
@@ -329,7 +329,7 @@ instance : LT (PathIn tab) := ⟨Relation.TransGen edge⟩
 instance : LE (PathIn tab) := ⟨Relation.ReflTransGen edge⟩
 
 /-- The "<" in a tableau is antisymmetric. -/
-instance edge.TransGen_isAsymm : IsAsymm (PathIn tab) (Relation.TransGen edge) :=
+instance edge.TransGen_isAsymm : @Std.Asymm (PathIn tab) (Relation.TransGen edge) :=
   ⟨WellFounded.asymmetric (WellFounded.transGen wellFounded)⟩
 
 theorem not_path_nil {a : PathIn tab} : ¬(a < PathIn.nil) := by
@@ -1370,7 +1370,7 @@ instance PathIn.instFintype {tab : Tableau Hist X} : Fintype (PathIn tab) := by
 
 -- mathlib?
 theorem Finite.wellfounded_of_irrefl_TC {α : Type} [Finite α] (r : α → α → Prop)
-    (h : IsIrrefl α (Relation.TransGen r)) : WellFounded r :=
+    (h : Std.Irrefl (Relation.TransGen r)) : WellFounded r :=
   let wf := Finite.wellFounded_of_trans_of_irrefl (Relation.TransGen r)
   ⟨fun a => acc_transGen_iff.mp <| wf.apply a⟩
 
@@ -1417,7 +1417,7 @@ lemma single_of_transgen {α} {r} {a c : α} : Relation.TransGen r a c → ∃ b
   case single b e => use b
   case tail d e ih => assumption
 
-instance flipEdge.instIsIrrefl : IsIrrefl (PathIn tab) (Relation.TransGen (flip edge)) := by
+instance flipEdge.instIsIrrefl : @Std.Irrefl (PathIn tab) (Relation.TransGen (flip edge)) := by
   constructor
   intro p p_p
   rw [Relation.transGen_swap] at p_p

docbuild/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "05bb84181739ecc0897184a3e2906241267bcdfd",
+   "rev": "4dbbb80a2d54797f61d5a830b6dd82c087b0a7c2",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
@@ -22,7 +22,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba",
+   "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9",
+   "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -62,17 +62,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,7 +92,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -102,17 +102,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -122,7 +122,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -132,7 +132,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

docbuild/lakefile.toml

@@ -10,4 +10,4 @@ path = ".."
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.27.0-rc1"
+rev = "v4.28.0-rc1"

docbuild/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.28.0-rc1

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "pdl",