Bump Lean version to v4.13.0 and add test cases

.gitignore

@@ -1,6 +1,7 @@
 /Lean/Egg/Tests/Dataflow\ Rewriter/.lake
 /Lean/Egg/Tests/batteries/batteries
 /Lean/Egg/Tests/mathlib4/mathlib4
+/Lean/Egg/Tests/Andrés/.lake
 /Rust/Egg/Cargo.lock
 /Rust/Egg/target
 /Rust/Slotted/Cargo.lock

Lean/Egg/Tests/Andrés/Andrés.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `«Andrés»` library.
+-- Import modules here that should be built as part of the library.
+import «Andrés».Basic

Lean/Egg/Tests/Andrés/Andrés/Basic.lean

@@ -0,0 +1,77 @@
+import Mathlib
+import Egg
+
+-- cast_smul_eq_nnqsmul
+namespace NNRat
+
+variable (R S : Type*) [DivisionSemiring R] [CharZero R] [Semiring S] [Module ℚ≥0 S]
+
+example [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
+  refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
+  egg [
+    mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, smul_assoc,
+    nsmul_eq_mul q.den (α := R), cast_natCast, cast_mul, den_mul_eq_num, cast_natCast,
+    Nat.cast_smul_eq_nsmul
+  ]
+
+-- TODO: This saturates in slotted? I'm guessing there's something wrong with the saturation
+--       condition/progress measure.
+set_option egg.slotted true in
+example [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
+  refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
+  egg [
+    mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, smul_assoc,
+    nsmul_eq_mul q.den (α := R), cast_natCast, cast_mul, den_mul_eq_num, cast_natCast,
+    Nat.cast_smul_eq_nsmul
+  ]
+
+end NNRat
+
+-- mem_sInf
+namespace Order.Ideal
+
+open Function Set
+variable {P : Type*} [SemilatticeSup P] [OrderBot P] {x : P} {S : Set (Ideal P)}
+
+example : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s := by
+  egg [SetLike.mem_coe, coe_sInf, mem_iInter₂]
+
+set_option egg.slotted true in
+example : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s := by
+  egg [SetLike.mem_coe, coe_sInf, mem_iInter₂]
+
+end Order.Ideal
+
+-- not_modEq_iff_ne_add_zsmul
+namespace AddCommGroup
+
+variable {α : Type*} [AddCommGroup α] {p a a₁ a₂ b b₁ b₂ c : α} {n : ℕ} {z : ℤ}
+
+example : ¬a ≡ b [PMOD p] ↔ ∀ z : ℤ, b ≠ a + z • p := by
+  egg [modEq_iff_eq_add_zsmul, not_exists]
+
+set_option egg.slotted true in
+example : ¬a ≡ b [PMOD p] ↔ ∀ z : ℤ, b ≠ a + z • p := by
+  egg [modEq_iff_eq_add_zsmul, not_exists]
+
+end AddCommGroup
+
+-- trans_eq_none
+namespace PEquiv
+
+open Mathlib.Tactic.PushNeg
+
+example (f : α ≃. β) (g : β ≃. γ) (a : α) : f.trans g a = none ↔ ∀ b c, b ∉ f a ∨ c ∉ g b := by
+  egg [
+    Option.eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm, forall_swap, not_exists_eq,
+    not_and_eq
+  ]
+
+set_option egg.slotted true in
+example (f : α ≃. β) (g : β ≃. γ) (a : α) : f.trans g a = none ↔ ∀ b c, b ∉ f a ∨ c ∉ g b := by
+  egg [
+    Option.eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm, forall_swap, not_exists_eq,
+    not_and_eq
+  ]
+
+end PEquiv

Lean/Egg/Tests/Andrés/lake-manifest.json

@@ -0,0 +1,102 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.43",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d5ab93e3a3afadaf265a583a92f7e7c47203b540",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.13.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/nomeata/lean-calcify",
+   "type": "git",
+   "subDir": null,
+   "scope": "nomeata",
+   "rev": "dbc14d28fad2b090158ad60e490da9067b4519be",
+   "name": "calcify",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "egg",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../../../..",
+   "configFile": "lakefile.lean"}],
+ "name": "«Andrés»",
+ "lakeDir": ".lake"}

Lean/Egg/Tests/Andrés/lakefile.toml

@@ -0,0 +1,16 @@
+name = "Andrés"
+version = "0.1.0"
+keywords = ["math"]
+defaultTargets = ["«Andrés»"]
+
+[[require]]
+name    = "mathlib"
+scope   = "leanprover-community"
+version = "git#v4.13.0"
+
+[[require]]
+name = "egg"
+path = "../../../.."
+
+[[lean_lib]]
+name = "«Andrés»"

Lean/Egg/Tests/Andrés/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.13.0