bump to nightly-2023-07-20-03

mathlib commit leanprover-community/mathlib@8ea5598

Mathbin/Order/InitialSeg.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 
 ! This file was ported from Lean 3 source module order.initial_seg
-! leanprover-community/mathlib commit 730c6d4cab72b9d84fcfb9e95e8796e9cd8f40ba
+! leanprover-community/mathlib commit 8ea5598db6caeddde6cb734aa179cc2408dbd345
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathbin.Logic.Equiv.Set
 import Mathbin.Order.RelIso.Set
 import Mathbin.Order.WellFounded
 
@@ -506,6 +507,26 @@ theorem ofElement_top {α : Type _} (r : α → α → Prop) (a : α) : (ofEleme
 #align principal_seg.of_element_top PrincipalSeg.ofElement_top
 -/
 
+/-- For any principal segment `r ≺i s`, there is a `subrel` of `s` order isomorphic to `r`. -/
+@[simps symm_apply]
+noncomputable def subrelIso (f : r ≺i s) : Subrel s {b | s b f.top} ≃r r :=
+  RelIso.symm
+    { toEquiv :=
+        (Equiv.ofInjective f f.Injective).trans
+          (Equiv.setCongr (funext fun x => propext f.down.symm))
+      map_rel_iff' := fun a₁ a₂ => f.map_rel_iff }
+#align principal_seg.subrel_iso PrincipalSeg.subrelIso
+
+@[simp]
+theorem apply_subrelIso (f : r ≺i s) (b : {b | s b f.top}) : f (f.subrelIso b) = b :=
+  Equiv.apply_ofInjective_symm f.Injective _
+#align principal_seg.apply_subrel_iso PrincipalSeg.apply_subrelIso
+
+@[simp]
+theorem subrelIso_apply (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.down.mpr ⟨a, rfl⟩⟩ = a :=
+  Equiv.ofInjective_symm_apply f.Injective _
+#align principal_seg.subrel_iso_apply PrincipalSeg.subrelIso_apply
+
 #print PrincipalSeg.codRestrict /-
 /-- Restrict the codomain of a principal segment -/
 def codRestrict (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) : r ≺i Subrel s p :=

Mathbin/SetTheory/Ordinal/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 
 ! This file was ported from Lean 3 source module set_theory.ordinal.basic
-! leanprover-community/mathlib commit 8da9e30545433fdd8fe55a0d3da208e5d9263f03
+! leanprover-community/mathlib commit 8ea5598db6caeddde6cb734aa179cc2408dbd345
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -607,32 +607,41 @@ theorem typein_inj (r : α → α → Prop) [IsWellOrder α r] {a b} : typein r
 #align ordinal.typein_inj Ordinal.typein_inj
 -/
 
+#print Ordinal.typein.principalSeg /-
+/-- Principal segment version of the `typein` function, embedding a well order into
+  ordinals as a principal segment. -/
+def typein.principalSeg (r : α → α → Prop) [IsWellOrder α r] :
+    r ≺i ((· < ·) : Ordinal → Ordinal → Prop) :=
+  ⟨⟨⟨typein r, typein_injective r⟩, fun a b => typein_lt_typein r⟩, type r, fun o =>
+    ⟨typein_surj r, fun ⟨a, h⟩ => h ▸ typein_lt_type r a⟩⟩
+#align ordinal.typein.principal_seg Ordinal.typein.principalSeg
+-/
+
+#print Ordinal.typein.principalSeg_coe /-
+@[simp]
+theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] :
+    (typein.principalSeg r : α → Ordinal) = typein r :=
+  rfl
+#align ordinal.typein.principal_seg_coe Ordinal.typein.principalSeg_coe
+-/
+
 /-! ### Enumerating elements in a well-order with ordinals. -/
 
 
 #print Ordinal.enum /-
 /-- `enum r o h` is the `o`-th element of `α` ordered by `r`.
   That is, `enum` maps an initial segment of the ordinals, those
   less than the order type of `r`, to the elements of `α`. -/
-def enum (r : α → α → Prop) [IsWellOrder α r] (o) : o < type r → α :=
-  Quot.recOn' o (fun ⟨β, s, _⟩ h => (Classical.choice h).top) fun ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨h⟩ =>
-    by
-    skip; refine' funext fun H₂ : type t < type r => _
-    have H₁ : type s < type r := by rwa [type_eq.2 ⟨h⟩]
-    have :
-      ∀ {o e} (H : o < type r),
-        @Eq.ndrec (fun o : Ordinal => o < type r → α)
-            (fun h : type s < type r => (Classical.choice h).top) e H =
-          (Classical.choice H₁).top :=
-      by intros; subst e
-    exact (this H₂).trans (PrincipalSeg.top_eq h (Classical.choice H₁) (Classical.choice H₂))
+def enum (r : α → α → Prop) [IsWellOrder α r] (o) (h : o < type r) : α :=
+  (typein.principalSeg r).subrelIso ⟨o, h⟩
 #align ordinal.enum Ordinal.enum
 -/
 
 #print Ordinal.enum_type /-
 theorem enum_type {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
     (f : s ≺i r) {h : type s < type r} : enum r (type s) h = f.top :=
-  PrincipalSeg.top_eq (RelIso.refl _) _ _
+  (typein.principalSeg r).Injective <|
+    ((typein.principalSeg r).apply_subrelIso _).trans (typein_top _).symm
 #align ordinal.enum_type Ordinal.enum_type
 -/
 
@@ -680,18 +689,8 @@ theorem relIso_enum {α β : Type u} {r : α → α → Prop} {s : β → β →
 
 #print Ordinal.lt_wf /-
 theorem lt_wf : @WellFounded Ordinal (· < ·) :=
-  ⟨fun a =>
-    inductionOn a fun α r wo =>
-      suffices ∀ a, Acc (· < ·) (typein r a) from
-        ⟨_, fun o h =>
-          let ⟨a, e⟩ := typein_surj r h
-          e ▸ this a⟩
-      fun a =>
-      Acc.recOn (wo.wf.apply a) fun x H IH =>
-        ⟨_, fun o h =>
-          by
-          rcases typein_surj r (lt_trans h (typein_lt_type r _)) with ⟨b, rfl⟩
-          exact IH _ ((typein_lt_typein r).1 h)⟩⟩
+  wellFounded_iff_wellFounded_subrel.mpr fun a =>
+    inductionOn a fun α r wo => RelHomClass.wellFounded (typein.principal_seg r).subrelIso wo.wf
 #align ordinal.lt_wf Ordinal.lt_wf
 -/
 
@@ -707,24 +706,6 @@ theorem induction {p : Ordinal.{u} → Prop} (i : Ordinal.{u}) (h : ∀ j, (∀
 #align ordinal.induction Ordinal.induction
 -/
 
-#print Ordinal.typein.principalSeg /-
-/-- Principal segment version of the `typein` function, embedding a well order into
-  ordinals as a principal segment. -/
-def typein.principalSeg {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :
-    @PrincipalSeg α Ordinal.{u} r (· < ·) :=
-  ⟨RelEmbedding.ofMonotone (typein r) fun a b => (typein_lt_typein r).2, type r, fun b =>
-    ⟨fun h => ⟨enum r _ h, typein_enum r h⟩, fun ⟨a, e⟩ => e ▸ typein_lt_type _ _⟩⟩
-#align ordinal.typein.principal_seg Ordinal.typein.principalSeg
--/
-
-#print Ordinal.typein.principalSeg_coe /-
-@[simp]
-theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] :
-    (typein.principalSeg r : α → Ordinal) = typein r :=
-  rfl
-#align ordinal.typein.principal_seg_coe Ordinal.typein.principalSeg_coe
--/
-
 /-! ### Cardinality of ordinals -/
 
 
@@ -1415,25 +1396,18 @@ theorem le_enum_succ {o : Ordinal} (a : (succ o).out.α) :
 @[simp]
 theorem enum_inj {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : Ordinal} (h₁ : o₁ < type r)
     (h₂ : o₂ < type r) : enum r o₁ h₁ = enum r o₂ h₂ ↔ o₁ = o₂ :=
-  ⟨fun h => by
-    by_contra hne
-    cases' lt_or_gt_of_ne hne with hlt hlt <;> apply (IsWellOrder.isIrrefl r).1
-    · rwa [← @enum_lt_enum α r _ o₁ o₂ h₁ h₂, h] at hlt 
-    · change _ < _ at hlt ; rwa [← @enum_lt_enum α r _ o₂ o₁ h₂ h₁, h] at hlt , fun h => by
-    simp_rw [h]⟩
+  (typein.principalSeg r).subrelIso.Injective.eq_iff.trans Subtype.mk_eq_mk
 #align ordinal.enum_inj Ordinal.enum_inj
 -/
 
 #print Ordinal.enumIso /-
 /-- A well order `r` is order isomorphic to the set of ordinals smaller than `type r`. -/
 @[simps]
-def enumIso (r : α → α → Prop) [IsWellOrder α r] : Subrel (· < ·) (· < type r) ≃r r
-    where
-  toFun x := enum r x.1 x.2
-  invFun x := ⟨typein r x, typein_lt_type r x⟩
-  left_inv := fun ⟨o, h⟩ => Subtype.ext_val (typein_enum _ _)
-  right_inv h := enum_typein _ _
-  map_rel_iff' := by rintro ⟨a, _⟩ ⟨b, _⟩; apply enum_lt_enum
+def enumIso (r : α → α → Prop) [IsWellOrder α r] : Subrel (· < ·) (· < type r) ≃r r :=
+  {
+    (typein.principalSeg r).subrelIso with
+    toFun := fun x => enum r x.1 x.2
+    invFun := fun x => ⟨typein r x, typein_lt_type r x⟩ }
 #align ordinal.enum_iso Ordinal.enumIso
 -/
 

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`bf2428c9486c407ca38b5b3fb10b87dad0bc99fa`](https://github.com/leanprover-community/mathlib/commit/bf2428c9486c407ca38b5b3fb10b87dad0bc99fa)
+Tracking mathlib commit: [`8ea5598db6caeddde6cb734aa179cc2408dbd345`](https://github.com/leanprover-community/mathlib/commit/8ea5598db6caeddde6cb734aa179cc2408dbd345)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2f15b935791f08db21b6464f38b5327db545b82a",
+    "rev": "6b6536d89e3cebab3e19482bf34b08021cb67033",
     "name": "lean3port",
-    "inputRev?": "2f15b935791f08db21b6464f38b5327db545b82a"}},
+    "inputRev?": "6b6536d89e3cebab3e19482bf34b08021cb67033"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-07-20-01"
+def tag : String := "nightly-2023-07-20-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2f15b935791f08db21b6464f38b5327db545b82a"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6b6536d89e3cebab3e19482bf34b08021cb67033"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-bf2428c9486c407ca38b5b3fb10b87dad0bc99fa
+8ea5598db6caeddde6cb734aa179cc2408dbd345