Bump mathlib

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Dec 7, 2023 · 1fffd82 · 1fffd82
1 parent 688a8ab
commit 1fffd82
Show file tree

Hide file tree

Showing 7 changed files with 20 additions and 19 deletions.
diff --git a/ConNF/BaseType/NearLitter.lean b/ConNF/BaseType/NearLitter.lean
@@ -63,7 +63,7 @@ protected theorem IsNearLitter.nonempty (hs : IsNearLitter L s) : s.Nonempty :=
 @[simp]
 theorem isNearLitter_litterSet_iff : IsNearLitter L₁ (litterSet L₂) ↔ L₁ = L₂ := by
   refine ⟨fun h => ?_, ?_⟩
-  · by_contra'
+  · by_contra this
     refine ((mk_litterSet L₁).symm.trans_le <| mk_le_mk_of_subset ?_).not_lt h
     change litterSet L₁ ≤ _
     exact (le_symmDiff_iff_left _ _).2 (pairwise_disjoint_litterSet this)

diff --git a/ConNF/Foa/Action/FillAtomOrbits.lean b/ConNF/Foa/Action/FillAtomOrbits.lean
@@ -98,8 +98,9 @@ theorem mk_diff_dom_ran (L : Litter) :
   · refine' ⟨⟨fun a => a.1.2, _⟩⟩
     intro a b h
     exact Subtype.coe_injective (Prod.ext (a.prop.1.trans b.prop.1.symm) h)
-  · by_contra' h
-    have := add_lt_of_lt κ_isRegular.aleph0_le h (Small.union φ.atomMap_dom_small φ.atomMap_ran_small)
+  · by_contra h
+    have := add_lt_of_lt κ_isRegular.aleph0_le (lt_of_not_le h)
+      (Small.union φ.atomMap_dom_small φ.atomMap_ran_small)
     have := (le_mk_diff_add_mk (litterSet L) _).trans_lt this
     simp only [mk_litterSet, lt_self_iff_false] at this
 

diff --git a/ConNF/Foa/Action/FillAtomRange.lean b/ConNF/Foa/Action/FillAtomRange.lean
@@ -110,8 +110,8 @@ theorem mk_mapped_outside_domain (L : Litter) :
   refine' le_antisymm _ _
   · rw [← mk_litterSet]
     exact mk_subtype_mono fun x hx => hx.1
-  by_contra' h
-  have := Small.union h φ.atomMap_dom_small
+  by_contra h
+  have := Small.union (lt_of_not_le h) φ.atomMap_dom_small
   rw [diff_union_self] at this
   exact (mk_litterSet L).not_lt (Small.mono (subset_union_left _ _) this)
 

diff --git a/ConNF/Foa/Action/NearLitterAction.lean b/ConNF/Foa/Action/NearLitterAction.lean
@@ -122,14 +122,14 @@ theorem mk_not_bannedLitter : #{L | ¬φ.BannedLitter L} = #μ := by
   have := mk_sum_compl {L | φ.BannedLitter L}
   rw [compl_setOf, mk_litter] at this
   rw [← this, add_eq_right]
-  · by_contra' h
-    have h' := add_le_add (le_of_lt φ.bannedLitter_small) h.le
+  · by_contra h
+    have h' := add_le_add (le_of_lt φ.bannedLitter_small) (le_of_not_le h)
     rw [this] at h'
     refine' not_lt_of_le h' _
     refine' Cardinal.add_lt_of_lt μ_isStrongLimit.isLimit.aleph0_le κ_lt_μ _
     exact lt_of_le_of_lt κ_isRegular.aleph0_le κ_lt_μ
-  · by_contra' h
-    have h' := add_le_add (le_of_lt φ.bannedLitter_small) h.le
+  · by_contra h
+    have h' := add_le_add (le_of_lt φ.bannedLitter_small) (le_of_not_le h)
     rw [this] at h'
     refine' not_lt_of_le h' _
     refine' Cardinal.add_lt_of_lt μ_isStrongLimit.isLimit.aleph0_le κ_lt_μ _

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "bf8a6ea960d5a99f8e30cbf5597ab05cd233eadf",
+   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "60b5e23731ea672fd38f73364e1d3115213fcd04",
+   "rev": "f516ea2c0961f8b3b800a2f70d4981af830b703c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "3cc5df1be7f6db5ac13f26edda3fc258e199ab5f",
+   "rev": "53ecc225fea834acd7f32b9dc1aed880b79d70b9",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,10 +2,10 @@ import Lake
 open Lake DSL
 
 package ConNF where
-  moreServerArgs := #[
-    "-DautoImplicit=false",
-    "-DrelaxedAutoImplicit=false",
-    "-Dpp.proofs.withType=false"
+  moreServerOptions := #[
+    ⟨`autoImplicit, false⟩,
+    ⟨`relaxedAutoImplicit, false⟩,
+    ⟨`pp.proofs.withType, false⟩
   ]
 
 require mathlib from git

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.4.0-rc1