From 4fb466d6af34e370fce89afc91830dc0a244bbbb Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 15 Feb 2023 17:29:14 +0000 Subject: [PATCH 01/14] fix: add two missing #aligns (#2303) --- Mathlib/CategoryTheory/Iso.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean index 12bc23865b483..b08478fdb9a19 100644 --- a/Mathlib/CategoryTheory/Iso.lean +++ b/Mathlib/CategoryTheory/Iso.lean @@ -63,6 +63,8 @@ structure Iso {C : Type u} [Category.{v} C] (X Y : C) where is the identity on the target. -/ inv_hom_id : inv ≫ hom = 𝟙 Y := by aesop_cat #align category_theory.iso CategoryTheory.Iso +#align category_theory.iso.hom CategoryTheory.Iso.hom +#align category_theory.iso.inv CategoryTheory.Iso.inv #align category_theory.iso.inv_hom_id CategoryTheory.Iso.inv_hom_id #align category_theory.iso.hom_inv_id CategoryTheory.Iso.hom_inv_id @@ -140,7 +142,7 @@ def refl (X : C) : X ≅ X where instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩ -theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ +theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ @[simp] theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl From 89005600cfe9837fadb280caccf24cade943bd30 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 15 Feb 2023 17:38:51 +0000 Subject: [PATCH 02/14] fix: return early in library_search if initial solveByElim succeeds (#2302) Fixes a bug introduced in #856. If `solveByElim` succeeds, then we should return early. Otherwise, we look through all lemmas in the environment and find something like `namedPattern` or `Eq.mp` and unnecessarily wrap the result in that. See https://github.com/leanprover-community/mathlib4/pull/2276 for an example bad output caused by this bug. Another example is this test: https://github.com/leanprover-community/mathlib4/blob/4ed65899eca4909e9b8f23a113b52ff8cb3f5d41/test/librarySearch.lean#L15 On master, it emits `exact namedPattern p p rfl`, and after this PR it correctly emits `exact p`. --- Mathlib/Tactic/LibrarySearch.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean index 1e84160af1eb4..2c93d244e9b11 100644 --- a/Mathlib/Tactic/LibrarySearch.lean +++ b/Mathlib/Tactic/LibrarySearch.lean @@ -86,6 +86,7 @@ def librarySearch (goal : MVarId) (lemmas : DiscrTree Name s) (required : List E try solveByElim [goal] required solveByElimDepth + return none catch _ => set state0 From c2003aa6e9f2a66d28c7a228fd3a79bd2b073330 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 15 Feb 2023 17:47:34 +0000 Subject: [PATCH 03/14] fix: use rfl instead of namedPattern rfl rfl rfl (#2276) `library_search` currently has a bug where it sometimes unnecessarily wraps its output in `namedPattern`. This PR removes a usage of `namedPattern` that got introduced in https://github.com/leanprover-community/mathlib4/pull/1895, presumably due to the `library_search` bug. --- Mathlib/Data/Finsupp/Fin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index 44588712533a9..c3d67254f0596 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -51,7 +51,7 @@ theorem cons_zero : cons y s 0 = y := @[simp] theorem cons_succ : cons y s i.succ = s i := -- porting notes: was Fin.cons_succ _ _ _ - namedPattern rfl rfl rfl + rfl #align finsupp.cons_succ Finsupp.cons_succ @[simp] From 065e9956724008d1059577700fd676eaf25f35d5 Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Wed, 15 Feb 2023 17:47:35 +0000 Subject: [PATCH 04/14] feat: port CategoryTheory.Functor.Hom (#2295) --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Functor/Hom.lean | 39 +++++++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 Mathlib/CategoryTheory/Functor/Hom.lean diff --git a/Mathlib.lean b/Mathlib.lean index 37dc6e9af0a04..d848790fb1ba2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -238,6 +238,7 @@ import Mathlib.CategoryTheory.Functor.Currying import Mathlib.CategoryTheory.Functor.Default import Mathlib.CategoryTheory.Functor.FullyFaithful import Mathlib.CategoryTheory.Functor.Functorial +import Mathlib.CategoryTheory.Functor.Hom import Mathlib.CategoryTheory.Functor.InvIsos import Mathlib.CategoryTheory.Groupoid import Mathlib.CategoryTheory.Iso diff --git a/Mathlib/CategoryTheory/Functor/Hom.lean b/Mathlib/CategoryTheory/Functor/Hom.lean new file mode 100644 index 0000000000000..1db6fb49476f3 --- /dev/null +++ b/Mathlib/CategoryTheory/Functor/Hom.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2018 Reid Barton. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Reid Barton, Scott Morrison + +! This file was ported from Lean 3 source module category_theory.functor.hom +! leanprover-community/mathlib commit 369525b73f229ccd76a6ec0e0e0bf2be57599768 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.Products.Basic +import Mathlib.CategoryTheory.Types + +/-! +The hom functor, sending `(X, Y)` to the type `X ⟶ Y`. +-/ + + +universe v u + +open Opposite + +open CategoryTheory + +namespace CategoryTheory.Functor + +variable (C : Type u) [Category.{v} C] + +/-- `Functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and +covariant in `Y`. -/ +@[simps] +def hom : Cᵒᵖ × C ⥤ Type v where + obj p := unop p.1 ⟶ p.2 + map f h := f.1.unop ≫ h ≫ f.2 + map_id := by aesop_cat + map_comp := fun {X} {Y} {Z} f g => by funext b; simp +#align category_theory.functor.hom CategoryTheory.Functor.hom + +end CategoryTheory.Functor From aeba7cb89cf2d98004946d7cecabaefcd794b223 Mon Sep 17 00:00:00 2001 From: arienmalec Date: Thu, 16 Feb 2023 01:18:34 +0000 Subject: [PATCH 05/14] feat: Port/Topology.List (#2287) port of topology.list --- Mathlib.lean | 1 + Mathlib/Topology/List.lean | 238 +++++++++++++++++++++++++++++++++++++ 2 files changed, 239 insertions(+) create mode 100644 Mathlib/Topology/List.lean diff --git a/Mathlib.lean b/Mathlib.lean index d848790fb1ba2..a9593729920c6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1110,6 +1110,7 @@ import Mathlib.Topology.Hom.Open import Mathlib.Topology.Homeomorph import Mathlib.Topology.Inseparable import Mathlib.Topology.Instances.Sign +import Mathlib.Topology.List import Mathlib.Topology.LocalExtr import Mathlib.Topology.LocallyConstant.Basic import Mathlib.Topology.LocallyFinite diff --git a/Mathlib/Topology/List.lean b/Mathlib/Topology/List.lean new file mode 100644 index 0000000000000..d1d47d2cefb81 --- /dev/null +++ b/Mathlib/Topology/List.lean @@ -0,0 +1,238 @@ +/- +Copyright (c) 2019 Reid Barton. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl + +! This file was ported from Lean 3 source module topology.list +! leanprover-community/mathlib commit 48085f140e684306f9e7da907cd5932056d1aded +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Topology.Constructions +import Mathlib.Topology.Algebra.Monoid + +/-! +# Topology on lists and vectors + +-/ + + +open TopologicalSpace Set Filter + +open Topology Filter + +variable {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] + +instance : TopologicalSpace (List α) := + TopologicalSpace.mkOfNhds (traverse nhds) + +theorem nhds_list (as : List α) : 𝓝 as = traverse 𝓝 as := by + refine' nhds_mkOfNhds _ _ _ _ + · intro l + induction l + case nil => exact le_rfl + case cons a l ih => + suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by + simpa only [functor_norm] using this + exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih + · intro l s hs + rcases(mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩ + clear as hs + have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s + induction hu generalizing s + case nil _hs => + exists [] + simp only [List.forall₂_nil_left_iff, exists_eq_left] + exact ⟨trivial, hus⟩ + -- porting note -- renamed reordered variables based on previous types + case cons a s as ss hts h ht _ ih => + rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩ + rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩ + exact + ⟨u::v, List.Forall₂.cons hu hv, + Subset.trans (Set.seq_mono (Set.image_subset _ hut) hvss) hus⟩ + rcases this with ⟨v, hv, hvs⟩ + refine' ⟨sequence v, mem_traverse _ _ _, hvs, _⟩ + · exact hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha + · intro u hu + have hu := (List.mem_traverse _ _).1 hu + have : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v := + by + refine' List.Forall₂.flip _ + replace hv := hv.flip + simp only [List.forall₂_and_left, flip] at hv⊢ + exact ⟨hv.1, hu.flip⟩ + refine' mem_of_superset _ hvs + exact mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha) +#align nhds_list nhds_list + +@[simp] +theorem nhds_nil : 𝓝 ([] : List α) = pure [] := by + rw [nhds_list, List.traverse_nil _] +#align nhds_nil nhds_nil + +theorem nhds_cons (a : α) (l : List α) : 𝓝 (a::l) = List.cons <$> 𝓝 a <*> 𝓝 l := by + rw [nhds_list, List.traverse_cons _, ← nhds_list] +#align nhds_cons nhds_cons + +theorem List.tendsto_cons {a : α} {l : List α} : + Tendsto (fun p : α × List α => List.cons p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a::l)) := by + rw [nhds_cons, Tendsto, Filter.map_prod]; exact le_rfl +#align list.tendsto_cons List.tendsto_cons + +theorem Filter.Tendsto.cons {α : Type _} {f : α → β} {g : α → List β} {a : Filter α} {b : β} + {l : List β} (hf : Tendsto f a (𝓝 b)) (hg : Tendsto g a (𝓝 l)) : + Tendsto (fun a => List.cons (f a) (g a)) a (𝓝 (b::l)) := + List.tendsto_cons.comp (Tendsto.prod_mk hf hg) +#align filter.tendsto.cons Filter.Tendsto.cons + +namespace List + +theorem tendsto_cons_iff {β : Type _} {f : List α → β} {b : Filter β} {a : α} {l : List α} : + Tendsto f (𝓝 (a::l)) b ↔ Tendsto (fun p : α × List α => f (p.1::p.2)) (𝓝 a ×ᶠ 𝓝 l) b := by + have : 𝓝 (a::l) = (𝓝 a ×ᶠ 𝓝 l).map fun p : α × List α => p.1::p.2 := + by + simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm, + (Filter.seq_eq_filter_seq _ _).symm] + simp [-Filter.map_def, (· ∘ ·), functor_norm] + rw [this, Filter.tendsto_map'_iff] ; dsimp; rfl +#align list.tendsto_cons_iff List.tendsto_cons_iff + +theorem continuous_cons : Continuous fun x : α × List α => (x.1::x.2 : List α) := + continuous_iff_continuousAt.mpr fun ⟨_x, _y⟩ => continuousAt_fst.cons continuousAt_snd +#align list.continuous_cons List.continuous_cons + +theorem tendsto_nhds {β : Type _} {f : List α → β} {r : List α → Filter β} + (h_nil : Tendsto f (pure []) (r [])) + (h_cons : + ∀ l a, + Tendsto f (𝓝 l) (r l) → + Tendsto (fun p : α × List α => f (p.1::p.2)) (𝓝 a ×ᶠ 𝓝 l) (r (a::l))) : + ∀ l, Tendsto f (𝓝 l) (r l) + | [] => by rwa [nhds_nil] + | a::l => by + rw [tendsto_cons_iff]; exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l) + +#align list.tendsto_nhds List.tendsto_nhds + +theorem continuousAt_length : ∀ l : List α, ContinuousAt List.length l := by + simp only [ContinuousAt, nhds_discrete] + refine' tendsto_nhds _ _ + · exact tendsto_pure_pure _ _ + · intro l a ih + dsimp only [List.length] + refine' Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) _ + refine' Tendsto.comp ih tendsto_snd +#align list.continuous_at_length List.continuousAt_length + +theorem tendsto_insert_nth' {a : α} : + ∀ {n : ℕ} {l : List α}, + Tendsto (fun p : α × List α => insertNth n p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insertNth n a l)) + | 0, l => tendsto_cons + | n + 1, [] => by simp + | n + 1, a'::l => + by + have : + 𝓝 a ×ᶠ 𝓝 (a'::l) = (𝓝 a ×ᶠ (𝓝 a' ×ᶠ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := + by + simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq] + simp [-Filter.map_def, (· ∘ ·), functor_norm] + rw [this, tendsto_map'_iff] + exact + (tendsto_fst.comp tendsto_snd).cons + ((@tendsto_insert_nth' _ n l).comp <| tendsto_fst.prod_mk <| tendsto_snd.comp tendsto_snd) +#align list.tendsto_insert_nth' List.tendsto_insert_nth' + +theorem tendsto_insertNth {β} {n : ℕ} {a : α} {l : List α} {f : β → α} {g : β → List α} + {b : Filter β} (hf : Tendsto f b (𝓝 a)) (hg : Tendsto g b (𝓝 l)) : + Tendsto (fun b : β => insertNth n (f b) (g b)) b (𝓝 (insertNth n a l)) := + tendsto_insert_nth'.comp (Tendsto.prod_mk hf hg) +#align list.tendsto_insert_nth List.tendsto_insertNth + +theorem continuous_insertNth {n : ℕ} : Continuous fun p : α × List α => insertNth n p.1 p.2 := + continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by + rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insert_nth' +#align list.continuous_insert_nth List.continuous_insertNth + +theorem tendsto_removeNth : + ∀ {n : ℕ} {l : List α}, Tendsto (fun l => removeNth l n) (𝓝 l) (𝓝 (removeNth l n)) + | _, [] => by rw [nhds_nil]; exact tendsto_pure_nhds _ _ + | 0, a::l => by rw [tendsto_cons_iff]; exact tendsto_snd + | n + 1, a::l => by + rw [tendsto_cons_iff] + dsimp [removeNth] + exact tendsto_fst.cons ((@tendsto_removeNth n l).comp tendsto_snd) +#align list.tendsto_remove_nth List.tendsto_removeNth + +theorem continuous_removeNth {n : ℕ} : Continuous fun l : List α => removeNth l n := + continuous_iff_continuousAt.mpr fun _a => tendsto_removeNth +#align list.continuous_remove_nth List.continuous_removeNth + +@[to_additive] +theorem tendsto_prod [Monoid α] [ContinuousMul α] {l : List α} : + Tendsto List.prod (𝓝 l) (𝓝 l.prod) := by + induction' l with x l ih + · simp (config := { contextual := true }) [nhds_nil, mem_of_mem_nhds, tendsto_pure_left] + simp_rw [tendsto_cons_iff, prod_cons] + have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod) + rw [ContinuousAt, nhds_prod_eq] at this + exact this.comp (tendsto_id.prod_map ih) +#align list.tendsto_prod List.tendsto_prod +#align list.tendsto_sum List.tendsto_sum + +@[to_additive] +theorem continuous_prod [Monoid α] [ContinuousMul α] : Continuous (prod : List α → α) := + continuous_iff_continuousAt.mpr fun _l => tendsto_prod +#align list.continuous_prod List.continuous_prod +#align list.continuous_sum List.continuous_sum + +end List + +namespace Vector + +open List + +instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance + +theorem tendsto_cons {n : ℕ} {a : α} {l : Vector α n} : + Tendsto (fun p : α × Vector α n => p.1 ::ᵥ p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a ::ᵥ l)) := by + rw [tendsto_subtype_rng, cons_val] + exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd) +#align vector.tendsto_cons Vector.tendsto_cons + +theorem tendsto_insertNth {n : ℕ} {i : Fin (n + 1)} {a : α} : + ∀ {l : Vector α n}, + Tendsto (fun p : α × Vector α n => insertNth p.1 i p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insertNth a i l)) + | ⟨l, hl⟩ => by + rw [insertNth, tendsto_subtype_rng] + simp [insertNth_val] + exact List.tendsto_insertNth tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _) +#align vector.tendsto_insert_nth Vector.tendsto_insertNth + +theorem continuous_insert_nth' {n : ℕ} {i : Fin (n + 1)} : + Continuous fun p : α × Vector α n => insertNth p.1 i p.2 := + continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by + rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertNth +#align vector.continuous_insert_nth' Vector.continuous_insert_nth' + +theorem continuous_insertNth {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → Vector α n} + (hf : Continuous f) (hg : Continuous g) : Continuous fun b => insertNth (f b) i (g b) := + continuous_insert_nth'.comp (hf.prod_mk hg : _) +#align vector.continuous_insert_nth Vector.continuous_insertNth + +theorem continuousAt_removeNth {n : ℕ} {i : Fin (n + 1)} : + ∀ {l : Vector α (n + 1)}, ContinuousAt (removeNth i) l + | ⟨l, hl⟩ =>-- ∀{l:vector α (n+1)}, tendsto (remove_nth i) (𝓝 l) (𝓝 (remove_nth i l)) + --| ⟨l, hl⟩ := + by + rw [ContinuousAt, removeNth, tendsto_subtype_rng] + simp only [Vector.removeNth_val] + exact Tendsto.comp List.tendsto_removeNth continuousAt_subtype_val +#align vector.continuous_at_remove_nth Vector.continuousAt_removeNth + +theorem continuous_removeNth {n : ℕ} {i : Fin (n + 1)} : + Continuous (removeNth i : Vector α (n + 1) → Vector α n) := + continuous_iff_continuousAt.mpr fun ⟨_a, _l⟩ => continuousAt_removeNth +#align vector.continuous_remove_nth Vector.continuous_removeNth + +end Vector From cf6e83b80892661661214dc9c2696eac869b5f84 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 16 Feb 2023 06:14:09 +0000 Subject: [PATCH 06/14] feat: port CategoryTheory.Endomorphism (#2310) Co-authored-by: Johan Commelin --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Endomorphism.lean | 202 +++++++++++++++++++++++ 2 files changed, 203 insertions(+) create mode 100644 Mathlib/CategoryTheory/Endomorphism.lean diff --git a/Mathlib.lean b/Mathlib.lean index a9593729920c6..ff9d9f147f44f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -226,6 +226,7 @@ import Mathlib.CategoryTheory.Category.Preorder import Mathlib.CategoryTheory.Category.RelCat import Mathlib.CategoryTheory.Comma import Mathlib.CategoryTheory.ConcreteCategory.Bundled +import Mathlib.CategoryTheory.Endomorphism import Mathlib.CategoryTheory.EpiMono import Mathlib.CategoryTheory.EqToHom import Mathlib.CategoryTheory.Equivalence diff --git a/Mathlib/CategoryTheory/Endomorphism.lean b/Mathlib/CategoryTheory/Endomorphism.lean new file mode 100644 index 0000000000000..e5101f04e1d5c --- /dev/null +++ b/Mathlib/CategoryTheory/Endomorphism.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2019 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov, Scott Morrison, Simon Hudon + +! This file was ported from Lean 3 source module category_theory.endomorphism +! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Algebra.Hom.Equiv.Basic +import Mathlib.CategoryTheory.Groupoid +import Mathlib.CategoryTheory.Opposites +import Mathlib.GroupTheory.GroupAction.Defs + +/-! +# Endomorphisms + +Definition and basic properties of endomorphisms and automorphisms of an object in a category. + +For each `X : C`, we provide `CategoryTheory.End X := X ⟶ X` with a monoid structure, +and `CategoryTheory.Aut X := X ≅ X ` with a group structure. +-/ + + +universe v v' u u' + +namespace CategoryTheory + +/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with +`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`. -/ +def End {C : Type u} [CategoryStruct.{v} C] (X : C) := X ⟶ X +#align category_theory.End CategoryTheory.End + +namespace End + +section Struct + +variable {C : Type u} [CategoryStruct.{v} C] (X : C) + +protected instance one : One (End X) := ⟨𝟙 X⟩ +#align category_theory.End.has_one CategoryTheory.End.one + +protected instance inhabited : Inhabited (End X) := ⟨𝟙 X⟩ +#align category_theory.End.inhabited CategoryTheory.End.inhabited + +/-- Multiplication of endomorphisms agrees with `Function.comp`, not with +`CategoryTheory.CategoryStruct.comp`. -/ +protected instance mul : Mul (End X) := ⟨fun x y => y ≫ x⟩ +#align category_theory.End.has_mul CategoryTheory.End.mul + +variable {X} + +/-- Assist the typechecker by expressing a morphism `X ⟶ X` as a term of `CategoryTheory.End X`. -/ +def of (f : X ⟶ X) : End X := f +#align category_theory.End.of CategoryTheory.End.of + +/-- Assist the typechecker by expressing an endomorphism `f : CategoryTheory.End X` as a term of +`X ⟶ X`. -/ +def asHom (f : End X) : X ⟶ X := f +#align category_theory.End.as_hom CategoryTheory.End.asHom + +@[simp] -- porting note: todo: use `of`/`asHom`? +theorem one_def : (1 : End X) = 𝟙 X := rfl +#align category_theory.End.one_def CategoryTheory.End.one_def + +@[simp] -- porting note: todo: use `of`/`asHom`? +theorem mul_def (xs ys : End X) : xs * ys = ys ≫ xs := rfl +#align category_theory.End.mul_def CategoryTheory.End.mul_def + +end Struct + +/-- Endomorphisms of an object form a monoid -/ +instance monoid {C : Type u} [Category.{v} C] {X : C} : Monoid (End X) where + mul_one := Category.id_comp + one_mul := Category.comp_id + mul_assoc := fun x y z => (Category.assoc z y x).symm +#align category_theory.End.monoid CategoryTheory.End.monoid + +section MulAction + +variable {C : Type u} [Category.{v} C] + +open Opposite + +instance mulActionRight {X Y : C} : MulAction (End Y) (X ⟶ Y) where + smul r f := f ≫ r + one_smul := Category.comp_id + mul_smul _ _ _ := Eq.symm <| Category.assoc _ _ _ +#align category_theory.End.mul_action_right CategoryTheory.End.mulActionRight + +instance mulActionLeft {X : Cᵒᵖ} {Y : C} : MulAction (End X) (unop X ⟶ Y) where + smul r f := r.unop ≫ f + one_smul := Category.id_comp + mul_smul _ _ _ := Category.assoc _ _ _ +#align category_theory.End.mul_action_left CategoryTheory.End.mulActionLeft + +theorem smul_right {X Y : C} {r : End Y} {f : X ⟶ Y} : r • f = f ≫ r := + rfl +#align category_theory.End.smul_right CategoryTheory.End.smul_right + +theorem smul_left {X : Cᵒᵖ} {Y : C} {r : End X} {f : unop X ⟶ Y} : r • f = r.unop ≫ f := + rfl +#align category_theory.End.smul_left CategoryTheory.End.smul_left + +end MulAction + +/-- In a groupoid, endomorphisms form a group -/ +instance group {C : Type u} [Groupoid.{v} C] (X : C) : Group (End X) where + mul_left_inv := Groupoid.comp_inv + inv := Groupoid.inv +#align category_theory.End.group CategoryTheory.End.group + +end End + +theorem isUnit_iff_isIso {C : Type u} [Category.{v} C] {X : C} (f : End X) : + IsUnit (f : End X) ↔ IsIso f := + ⟨fun h => { out := ⟨h.unit.inv, ⟨h.unit.inv_val, h.unit.val_inv⟩⟩ }, fun h => + ⟨⟨f, inv f, by simp, by simp⟩, rfl⟩⟩ +#align category_theory.is_unit_iff_is_iso CategoryTheory.isUnit_iff_isIso + +variable {C : Type u} [Category.{v} C] (X : C) + +/-- Automorphisms of an object in a category. + +The order of arguments in multiplication agrees with +`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`. +-/ +def Aut (X : C) := X ≅ X +set_option linter.uppercaseLean3 false in +#align category_theory.Aut CategoryTheory.Aut + +namespace Aut + +protected instance inhabited : Inhabited (Aut X) := ⟨Iso.refl X⟩ +set_option linter.uppercaseLean3 false in +#align category_theory.Aut.inhabited CategoryTheory.Aut.inhabited + +instance : Group (Aut X) where + one := Iso.refl X + inv := Iso.symm + mul x y := Iso.trans y x + mul_assoc _ _ _ := (Iso.trans_assoc _ _ _).symm + one_mul := Iso.trans_refl + mul_one := Iso.refl_trans + mul_left_inv := Iso.self_symm_id + +theorem Aut_mul_def (f g : Aut X) : f * g = g.trans f := rfl +set_option linter.uppercaseLean3 false in +#align category_theory.Aut.Aut_mul_def CategoryTheory.Aut.Aut_mul_def + +theorem Aut_inv_def (f : Aut X) : f⁻¹ = f.symm := rfl +set_option linter.uppercaseLean3 false in +#align category_theory.Aut.Aut_inv_def CategoryTheory.Aut.Aut_inv_def + +/-- Units in the monoid of endomorphisms of an object +are (multiplicatively) equivalent to automorphisms of that object. +-/ +def unitsEndEquivAut : (End X)ˣ ≃* Aut X where + toFun f := ⟨f.1, f.2, f.4, f.3⟩ + invFun f := ⟨f.1, f.2, f.4, f.3⟩ + left_inv := fun ⟨f₁, f₂, f₃, f₄⟩ => rfl + right_inv := fun ⟨f₁, f₂, f₃, f₄⟩ => rfl + map_mul' f g := by cases f; cases g; rfl +set_option linter.uppercaseLean3 false in +#align category_theory.Aut.units_End_equiv_Aut CategoryTheory.Aut.unitsEndEquivAut + +/-- Isomorphisms induce isomorphisms of the automorphism group -/ +def autMulEquivOfIso {X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y where + toFun x := ⟨h.inv ≫ x.hom ≫ h.hom, h.inv ≫ x.inv ≫ h.hom, _, _⟩ + invFun y := ⟨h.hom ≫ y.hom ≫ h.inv, h.hom ≫ y.inv ≫ h.inv, _, _⟩ + left_inv _ := by aesop_cat + right_inv _ := by aesop_cat + map_mul' := by simp [Aut_mul_def] +set_option linter.uppercaseLean3 false in +#align category_theory.Aut.Aut_mul_equiv_of_iso CategoryTheory.Aut.autMulEquivOfIso + +end Aut + +namespace Functor + +variable {D : Type u'} [Category.{v'} D] (f : C ⥤ D) + +/-- `f.map` as a monoid hom between endomorphism monoids. -/ +@[simps] +def mapEnd : End X →* End (f.obj X) where + toFun := f.map + map_mul' x y := f.map_comp y x + map_one' := f.map_id X +#align category_theory.functor.map_End CategoryTheory.Functor.mapEnd + +/-- `f.mapIso` as a group hom between automorphism groups. -/ +def mapAut : Aut X →* Aut (f.obj X) where + toFun := f.mapIso + map_mul' x y := f.mapIso_trans y x + map_one' := f.mapIso_refl X +set_option linter.uppercaseLean3 false in +#align category_theory.functor.map_Aut CategoryTheory.Functor.mapAut + +end Functor + +end CategoryTheory From 907422526a8411facde348d7ff9c70a6461f851a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 16 Feb 2023 06:27:16 +0000 Subject: [PATCH 07/14] Fix: rename `Set.to_finset_set_of` to `Set.toFinset_setOf` (#2309) --- Mathlib/Combinatorics/Composition.lean | 4 ++-- Mathlib/Data/Fintype/Basic.lean | 7 +++---- Mathlib/Data/Set/Finite.lean | 2 +- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/Combinatorics/Composition.lean b/Mathlib/Combinatorics/Composition.lean index cb2dc243cb435..8dcd1e62b007f 100644 --- a/Mathlib/Combinatorics/Composition.lean +++ b/Mathlib/Combinatorics/Composition.lean @@ -815,7 +815,7 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1) left_inv := by intro c ext i - simp only [add_comm, Set.to_finset_set_of, Finset.mem_univ, + simp only [add_comm, Set.toFinset_setOf, Finset.mem_univ, forall_true_left, Finset.mem_filter, true_and, exists_prop] constructor · rintro (rfl | rfl | ⟨j, hj1, hj2⟩) @@ -848,7 +848,7 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1) rw [add_comm] apply (Nat.succ_pred_eq_of_pos _).symm exact (zero_le i.val).trans_lt (i.2.trans_le (Nat.sub_le n 1)) - simp only [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.to_finset_set_of, + simp only [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf, Finset.mem_univ, forall_true_left, Finset.mem_filter, add_eq_zero_iff, and_false, add_left_inj, false_or, true_and] erw [Set.mem_setOf_eq] diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean index 889cd0a2b9142..3544164b29ea5 100644 --- a/Mathlib/Data/Fintype/Basic.lean +++ b/Mathlib/Data/Fintype/Basic.lean @@ -765,12 +765,11 @@ theorem toFinset_eq_univ [Fintype α] [Fintype s] : s.toFinset = Finset.univ ↔ #align set.to_finset_eq_univ Set.toFinset_eq_univ @[simp] -theorem to_finset_set_of [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { x | p x }] : - { x | p x }.toFinset = Finset.univ.filter p := - by +theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { x | p x }] : + { x | p x }.toFinset = Finset.univ.filter p := by ext simp -#align set.to_finset_set_of Set.to_finset_set_of +#align set.to_finset_set_of Set.toFinset_setOf --@[simp] Porting note: removing simp, simp can prove it theorem toFinset_ssubset_univ [Fintype α] {s : Set α} [Fintype s] : diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index 888b1b99297c2..2df06867da52c 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/Mathlib/Data/Set/Finite.lean @@ -1200,7 +1200,7 @@ theorem Finite.card_toFinset {s : Set α} [Fintype s] (h : s.Finite) : theorem card_ne_eq [Fintype α] (a : α) [Fintype { x : α | x ≠ a }] : Fintype.card { x : α | x ≠ a } = Fintype.card α - 1 := by haveI := Classical.decEq α - rw [← toFinset_card, to_finset_set_of, Finset.filter_ne', + rw [← toFinset_card, toFinset_setOf, Finset.filter_ne', Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ] #align set.card_ne_eq Set.card_ne_eq From 3d04ae464dfe344d13c2d8c6d48cafd5986142b5 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 16 Feb 2023 08:40:23 +0000 Subject: [PATCH 08/14] fix: rename `functor_unit_iso_comp` to `functor_unitIso_comp` (#2314) --- Mathlib/CategoryTheory/Equivalence.lean | 16 ++++++++-------- Mathlib/CategoryTheory/Opposites.lean | 4 ++-- Mathlib/CategoryTheory/Products/Basic.lean | 4 ++-- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean index 7d11ce912cb5c..dac17d3e0b1bc 100644 --- a/Mathlib/CategoryTheory/Equivalence.lean +++ b/Mathlib/CategoryTheory/Equivalence.lean @@ -89,7 +89,7 @@ structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Categ /-- The composition `inverse ⋙ functor` is also isomorphic to the identity -/ counitIso : inverse ⋙ functor ≅ 𝟭 D /-- The natural isomorphism compose to the identity -/ - functor_unit_iso_comp : + functor_unitIso_comp : ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X) := by aesop_cat #align category_theory.equivalence CategoryTheory.Equivalence @@ -150,7 +150,7 @@ theorem Equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) : @[simp] theorem functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) := - e.functor_unit_iso_comp X + e.functor_unitIso_comp X #align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp @[simp] @@ -311,7 +311,7 @@ def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`, -- but we choose to avoid using that here, for the sake of good structure projection `simp` -- lemmas. - functor_unit_iso_comp X := by + functor_unitIso_comp X := by dsimp rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counitInv_app_functor, fun_inv_map, Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp] @@ -490,14 +490,14 @@ class IsEquivalence (F : C ⥤ D) where mk' :: /-- Composition `inverse ⋙ F` is isomorphic to the identity. =-/ counitIso : inverse ⋙ F ≅ 𝟭 D /-- We natural isomorphisms are inverse -/ - functor_unit_iso_comp : + functor_unitIso_comp : ∀ X : C, F.map ((unitIso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫ counitIso.hom.app (F.obj X) = 𝟙 (F.obj X) := by aesop_cat #align category_theory.is_equivalence CategoryTheory.IsEquivalence -attribute [reassoc (attr := simp)] IsEquivalence.functor_unit_iso_comp +attribute [reassoc (attr := simp)] IsEquivalence.functor_unitIso_comp namespace IsEquivalence @@ -524,7 +524,7 @@ namespace Functor /-- Interpret a functor that is an equivalence as an equivalence. -/ def asEquivalence (F : C ⥤ D) [IsEquivalence F] : C ≌ D := ⟨F, IsEquivalence.inverse F, IsEquivalence.unitIso, IsEquivalence.counitIso, - IsEquivalence.functor_unit_iso_comp⟩ + IsEquivalence.functor_unitIso_comp⟩ #align category_theory.functor.as_equivalence CategoryTheory.Functor.asEquivalence instance isEquivalenceRefl : IsEquivalence (𝟭 C) := @@ -630,7 +630,7 @@ def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G inverse := hF.inverse unitIso := hF.unitIso ≪≫ NatIso.hcomp e (Iso.refl hF.inverse) counitIso := NatIso.hcomp (Iso.refl hF.inverse) e.symm ≪≫ hF.counitIso - functor_unit_iso_comp X := by + functor_unitIso_comp X := by dsimp [NatIso.hcomp] erw [id_comp, F.map_id, comp_id] apply (cancel_epi (e.hom.app X)).mp @@ -638,7 +638,7 @@ def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G slice_lhs 2 3 => rw [← NatTrans.vcomp_app', e.hom_inv_id] simp only [NatTrans.id_app, id_comp, comp_id, F.map_comp, assoc] erw [hF.counitIso.hom.naturality] - slice_lhs 1 2 => rw [functor_unit_iso_comp] + slice_lhs 1 2 => rw [functor_unitIso_comp] simp only [Functor.id_map, id_comp] #align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 422085e229b47..98da5ee9a89a6 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/Mathlib/CategoryTheory/Opposites.lean @@ -543,7 +543,7 @@ def op (e : C ≌ D) : Cᵒᵖ ≌ Dᵒᵖ where inverse := e.inverse.op unitIso := (NatIso.op e.unitIso).symm counitIso := (NatIso.op e.counitIso).symm - functor_unit_iso_comp X := by + functor_unitIso_comp X := by apply Quiver.Hom.unop_inj dsimp simp @@ -557,7 +557,7 @@ def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D where inverse := e.inverse.unop unitIso := (NatIso.unop e.unitIso).symm counitIso := (NatIso.unop e.counitIso).symm - functor_unit_iso_comp X := by + functor_unitIso_comp X := by apply Quiver.Hom.op_inj dsimp simp diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean index 12b62a96bc88d..75175657559b1 100644 --- a/Mathlib/CategoryTheory/Products/Basic.lean +++ b/Mathlib/CategoryTheory/Products/Basic.lean @@ -353,7 +353,7 @@ def functorProdFunctorEquivCounitIso : (by aesop_cat) #align category_theory.functor_prod_functor_equiv_counit_iso CategoryTheory.functorProdFunctorEquivCounitIso -/- Porting note: unlike with Lean 3, we needed to provide `functor_unit_iso_comp` because +/- Porting note: unlike with Lean 3, we needed to provide `functor_unitIso_comp` because Lean 4 could not see through `functorProdFunctorEquivUnitIso` (or the co-unit version) to run the auto tactic `by aesop_cat` -/ @@ -364,7 +364,7 @@ def functorProdFunctorEquiv : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C := inverse := functorProdToProdFunctor A B C, unitIso := functorProdFunctorEquivUnitIso A B C, counitIso := functorProdFunctorEquivCounitIso A B C, - functor_unit_iso_comp := by + functor_unitIso_comp := by simp only [functorProdFunctorEquivUnitIso] aesop_cat } From a43298126c5cdd2d8e1fb3c53b46c0f1d1a6daba Mon Sep 17 00:00:00 2001 From: qawbecrdtey Date: Thu, 16 Feb 2023 08:49:15 +0000 Subject: [PATCH 09/14] feat: port CategoryTheory.Balanced (#2313) --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Balanced.lean | 62 ++++++++++++++++++++++++++++ 2 files changed, 63 insertions(+) create mode 100644 Mathlib/CategoryTheory/Balanced.lean diff --git a/Mathlib.lean b/Mathlib.lean index ff9d9f147f44f..788e885ffb27b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -218,6 +218,7 @@ import Mathlib.Algebra.Support import Mathlib.Algebra.Tropical.Basic import Mathlib.Algebra.Tropical.BigOperators import Mathlib.Algebra.Tropical.Lattice +import Mathlib.CategoryTheory.Balanced import Mathlib.CategoryTheory.Bicategory.Basic import Mathlib.CategoryTheory.Bicategory.Strict import Mathlib.CategoryTheory.Category.Basic diff --git a/Mathlib/CategoryTheory/Balanced.lean b/Mathlib/CategoryTheory/Balanced.lean new file mode 100644 index 0000000000000..d6bb98a0c0541 --- /dev/null +++ b/Mathlib/CategoryTheory/Balanced.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2022 Markus Himmel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel + +! This file was ported from Lean 3 source module category_theory.balanced +! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.EpiMono + +/-! +# Balanced categories + +A category is called balanced if any morphism that is both monic and epic is an isomorphism. + +Balanced categories arise frequently. For example, categories in which every monomorphism +(or epimorphism) is strong are balanced. Examples of this are abelian categories and toposes, such +as the category of types. + +-/ + + +universe v u + +namespace CategoryTheory + +variable {C : Type u} [Category.{v} C] + +section + +variable (C) + +/-- A category is called balanced if any morphism that is both monic and epic is an isomorphism. -/ +class Balanced : Prop where + isIso_of_mono_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f], IsIso f +#align category_theory.balanced CategoryTheory.Balanced + +end + +theorem isIso_of_mono_of_epi [Balanced C] {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f] : IsIso f := + Balanced.isIso_of_mono_of_epi _ +#align category_theory.is_iso_of_mono_of_epi CategoryTheory.isIso_of_mono_of_epi + +theorem isIso_iff_mono_and_epi [Balanced C] {X Y : C} (f : X ⟶ Y) : IsIso f ↔ Mono f ∧ Epi f := + ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => isIso_of_mono_of_epi _⟩ +#align category_theory.is_iso_iff_mono_and_epi CategoryTheory.isIso_iff_mono_and_epi + +section + +attribute [local instance] isIso_of_mono_of_epi + +theorem balanced_opposite [Balanced C] : Balanced Cᵒᵖ := + { isIso_of_mono_of_epi := fun f fmono fepi => by + rw [← Quiver.Hom.op_unop f] + exact isIso_of_op _ } +#align category_theory.balanced_opposite CategoryTheory.balanced_opposite + +end + +end CategoryTheory From 1c14085aa2b18959cea8ca84fe73cd264d996a7c Mon Sep 17 00:00:00 2001 From: qawbecrdtey Date: Thu, 16 Feb 2023 08:49:16 +0000 Subject: [PATCH 10/14] feat: port Computability.DFA (#2317) --- Mathlib.lean | 1 + Mathlib/Computability/DFA.lean | 176 +++++++++++++++++++++++++++++++++ 2 files changed, 177 insertions(+) create mode 100644 Mathlib/Computability/DFA.lean diff --git a/Mathlib.lean b/Mathlib.lean index 788e885ffb27b..2ed934b727fee 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -282,6 +282,7 @@ import Mathlib.Combinatorics.SetFamily.Shadow import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise import Mathlib.Combinatorics.Young.SemistandardTableau import Mathlib.Combinatorics.Young.YoungDiagram +import Mathlib.Computability.DFA import Mathlib.Computability.Language import Mathlib.Computability.TuringMachine import Mathlib.Control.Applicative diff --git a/Mathlib/Computability/DFA.lean b/Mathlib/Computability/DFA.lean new file mode 100644 index 0000000000000..be1b063224eac --- /dev/null +++ b/Mathlib/Computability/DFA.lean @@ -0,0 +1,176 @@ +/- +Copyright (c) 2020 Fox Thomson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fox Thomson + +! This file was ported from Lean 3 source module computability.DFA +! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Data.Fintype.Card +import Mathlib.Computability.Language +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.WLOG + +/-! +# Deterministic Finite Automata + +This file contains the definition of a Deterministic Finite Automaton (DFA), a state machine which +determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set +in linear time. +Note that this definition allows for Automaton with infinite states, a `Fintype` instance must be +supplied for true DFA's. +-/ + + +open Computability + +universe u v + +-- Porting note: Required as `DFA` is used in mathlib3 +set_option linter.uppercaseLean3 false + +/-- A DFA is a set of states (`σ`), a transition function from state to state labelled by the + alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`). -/ +structure DFA (α : Type u) (σ : Type v) where + /-- A transition function from state to state labelled by the alphabet. -/ + step : σ → α → σ + /-- Starting state. -/ + start : σ + /-- Set of acceptance states. -/ + accept : Set σ +#align DFA DFA + +namespace DFA + +variable {α : Type u} {σ : Type v} (M : DFA α σ) + +instance [Inhabited σ] : Inhabited (DFA α σ) := + ⟨DFA.mk (fun _ _ => default) default ∅⟩ + +/-- `M.evalFrom s x` evaluates `M` with input `x` starting from the state `s`. -/ +def evalFrom (start : σ) : List α → σ := + List.foldl M.step start +#align DFA.eval_from DFA.evalFrom + +@[simp] +theorem evalFrom_nil (s : σ) : M.evalFrom s [] = s := + rfl +#align DFA.eval_from_nil DFA.evalFrom_nil + +@[simp] +theorem evalFrom_singleton (s : σ) (a : α) : M.evalFrom s [a] = M.step s a := + rfl +#align DFA.eval_from_singleton DFA.evalFrom_singleton + +@[simp] +theorem evalFrom_append_singleton (s : σ) (x : List α) (a : α) : + M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a := by + simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil] +#align DFA.eval_from_append_singleton DFA.evalFrom_append_singleton + +/-- `M.eval x` evaluates `M` with input `x` starting from the state `M.start`. -/ +def eval : List α → σ := + M.evalFrom M.start +#align DFA.eval DFA.eval + +@[simp] +theorem eval_nil : M.eval [] = M.start := + rfl +#align DFA.eval_nil DFA.eval_nil + +@[simp] +theorem eval_singleton (a : α) : M.eval [a] = M.step M.start a := + rfl +#align DFA.eval_singleton DFA.eval_singleton + +@[simp] +theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a := + evalFrom_append_singleton _ _ _ _ +#align DFA.eval_append_singleton DFA.eval_append_singleton + +theorem evalFrom_of_append (start : σ) (x y : List α) : + M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y := + x.foldl_append _ _ y +#align DFA.eval_from_of_append DFA.evalFrom_of_append + +/-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/ +def accepts : Language α := fun x => M.eval x ∈ M.accept +#align DFA.accepts DFA.accepts + +theorem mem_accepts (x : List α) : x ∈ M.accepts ↔ M.evalFrom M.start x ∈ M.accept := by rfl +#align DFA.mem_accepts DFA.mem_accepts + +theorem evalFrom_split [Fintype σ] {x : List α} {s t : σ} (hlen : Fintype.card σ ≤ x.length) + (hx : M.evalFrom s x = t) : + ∃ q a b c, + x = a ++ b ++ c ∧ + a.length + b.length ≤ Fintype.card σ ∧ + b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t := by + obtain ⟨n, m, hneq, heq⟩ := + Fintype.exists_ne_map_eq_of_card_lt + (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by norm_num) + wlog hle : (n : ℕ) ≤ m + · exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle) + have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m + dsimp at heq + refine' + ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by + rfl, _⟩ + · rw [List.take_append_drop, List.take_append_drop] + · simp only [List.length_drop, List.length_take] + rw [min_eq_left (hm.trans hlen), min_eq_left hle, add_tsub_cancel_of_le hle] + exact hm + · intro h + have hlen' := congr_arg List.length h + simp only [List.length_drop, List.length, List.length_take] at hlen' + rw [min_eq_left, tsub_eq_zero_iff_le] at hlen' + · apply hneq + apply le_antisymm + assumption' + exact hm.trans hlen + have hq : + M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) = + M.evalFrom s ((x.take m).take n) := + by + rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← + List.take_take, min_eq_left hle, List.take_append_drop] + use hq + rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc, + List.take_append_drop, List.take_append_drop] +#align DFA.eval_from_split DFA.evalFrom_split + +theorem evalFrom_of_pow {x y : List α} {s : σ} (hx : M.evalFrom s x = s) + (hy : y ∈ ({x} : Language α)∗) : M.evalFrom s y = s := by + rw [Language.mem_kstar] at hy + rcases hy with ⟨S, rfl, hS⟩ + induction' S with a S ih + · rfl + · have ha := hS a (List.mem_cons_self _ _) + rw [Set.mem_singleton_iff] at ha + rw [List.join, evalFrom_of_append, ha, hx] + apply ih + intro z hz + exact hS z (List.mem_cons_of_mem a hz) +#align DFA.eval_from_of_pow DFA.evalFrom_of_pow + +theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts) + (hlen : Fintype.card σ ≤ List.length x) : + ∃ a b c, + x = a ++ b ++ c ∧ + a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts := by + obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split hlen rfl + use a, b, c, hx, hlen, hnil + intro y hy + rw [Language.mem_mul] at hy + rcases hy with ⟨ab, c', hab, hc', rfl⟩ + rw [Language.mem_mul] at hab + rcases hab with ⟨a', b', ha', hb', rfl⟩ + rw [Set.mem_singleton_iff] at ha' hc' + substs ha' hc' + have h := M.evalFrom_of_pow hb hb' + rwa [mem_accepts, evalFrom_of_append, evalFrom_of_append, h, hc] +#align DFA.pumping_lemma DFA.pumping_lemma + +end DFA From b9f402c02de2fa446584888e95ae7599a2ce163e Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 16 Feb 2023 08:59:31 +0000 Subject: [PATCH 11/14] feat: port SetTheory.Ordinal.Arithmetic (#2271) Co-authored-by: qawbecrdtey Co-authored-by: Eric Wieser Co-authored-by: Komyyy Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com> --- Mathlib.lean | 1 + Mathlib/SetTheory/Ordinal/Arithmetic.lean | 3019 +++++++++++++++++++++ 2 files changed, 3020 insertions(+) create mode 100644 Mathlib/SetTheory/Ordinal/Arithmetic.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2ed934b727fee..77fdddc8da43a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -960,6 +960,7 @@ import Mathlib.SetTheory.Cardinal.Basic import Mathlib.SetTheory.Cardinal.Finite import Mathlib.SetTheory.Cardinal.SchroederBernstein import Mathlib.SetTheory.Lists +import Mathlib.SetTheory.Ordinal.Arithmetic import Mathlib.SetTheory.Ordinal.Basic import Mathlib.Tactic.Abel import Mathlib.Tactic.Alias diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean new file mode 100644 index 0000000000000..37a51b6e3b94f --- /dev/null +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -0,0 +1,3019 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Floris van Doorn, Violeta Hernández Palacios + +! This file was ported from Lean 3 source module set_theory.ordinal.arithmetic +! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.SetTheory.Ordinal.Basic +import Mathlib.Tactic.ByContra + +/-! +# Ordinal arithmetic + +Ordinals have an addition (corresponding to disjoint union) that turns them into an additive +monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns +them into a monoid. One can also define correspondingly a subtraction, a division, a successor +function, a power function and a logarithm function. + +We also define limit ordinals and prove the basic induction principle on ordinals separating +successor ordinals and limit ordinals, in `limitRecOn`. + +## Main definitions and results + +* `o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that + every element of `o₁` is smaller than every element of `o₂`. +* `o₁ - o₂` is the unique ordinal `o` such that `o₂ + o = o₁`, when `o₂ ≤ o₁`. +* `o₁ * o₂` is the lexicographic order on `o₂ × o₁`. +* `o₁ / o₂` is the ordinal `o` such that `o₁ = o₂ * o + o'` with `o' < o₂`. We also define the + divisibility predicate, and a modulo operation. +* `Order.succ o = o + 1` is the successor of `o`. +* `pred o` if the predecessor of `o`. If `o` is not a successor, we set `pred o = o`. + +We also define the power function and the logarithm function on ordinals, and discuss the properties +of casts of natural numbers of and of `ω` with respect to these operations. + +Some properties of the operations are also used to discuss general tools on ordinals: + +* `IsLimit o`: an ordinal is a limit ordinal if it is neither `0` nor a successor. +* `limitRecOn` is the main induction principle of ordinals: if one can prove a property by + induction at successor ordinals and at limit ordinals, then it holds for all ordinals. +* `IsNormal`: a function `f : Ordinal → Ordinal` satisfies `IsNormal` if it is strictly increasing + and order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for + `a < o`. +* `enumOrd`: enumerates an unbounded set of ordinals by the ordinals themselves. +* `sup`, `lsub`: the supremum / least strict upper bound of an indexed family of ordinals in + `Type u`, as an ordinal in `Type u`. +* `bsup`, `blsub`: the supremum / least strict upper bound of a set of ordinals indexed by ordinals + less than a given ordinal `o`. + +Various other basic arithmetic results are given in `Principal.lean` instead. +-/ + + +noncomputable section + +open Function Cardinal Set Equiv Order + +open Classical Cardinal Ordinal + +universe u v w + +namespace Ordinal + +variable {α : Type _} {β : Type _} {γ : Type _} {r : α → α → Prop} {s : β → β → Prop} + {t : γ → γ → Prop} + +/-! ### Further properties of addition on ordinals -/ + +@[simp] +theorem lift_add (a b : Ordinal.{v}) : lift.{u} (a + b) = lift.{u} a + lift.{u} b := + Quotient.inductionOn₂ a b fun ⟨_α, _r, _⟩ ⟨_β, _s, _⟩ => + Quotient.sound + ⟨(RelIso.preimage Equiv.ulift _).trans + (RelIso.sumLexCongr (RelIso.preimage Equiv.ulift _) (RelIso.preimage Equiv.ulift _)).symm⟩ +#align ordinal.lift_add Ordinal.lift_add + +@[simp] +theorem lift_succ (a : Ordinal.{v}) : lift.{u} (succ a) = succ (lift.{u} a) := by + rw [← add_one_eq_succ, lift_add, lift_one] + rfl +#align ordinal.lift_succ Ordinal.lift_succ + +instance add_contravariantClass_le : ContravariantClass Ordinal.{u} Ordinal.{u} (· + ·) (· ≤ ·) := + ⟨fun a b c => + inductionOn a fun α r hr => + inductionOn b fun β₁ s₁ hs₁ => + inductionOn c fun β₂ s₂ hs₂ ⟨f⟩ => + ⟨have fl : ∀ a, f (Sum.inl a) = Sum.inl a := fun a => by + simpa only [InitialSeg.trans_apply, InitialSeg.leAdd_apply] using + @InitialSeg.eq _ _ _ _ _ + ((InitialSeg.leAdd r s₁).trans f) (InitialSeg.leAdd r s₂) a + have : ∀ b, { b' // f (Sum.inr b) = Sum.inr b' } := by + intro b; cases e : f (Sum.inr b) + · rw [← fl] at e + have := f.inj' e + contradiction + · exact ⟨_, rfl⟩ + let g (b) := (this b).1 + have fr : ∀ b, f (Sum.inr b) = Sum.inr (g b) := fun b => (this b).2 + ⟨⟨⟨g, fun x y h => by + injection f.inj' (by rw [fr, fr, h] : f (Sum.inr x) = f (Sum.inr y))⟩, + @fun a b => by + -- Porting note: + -- `relEmbedding.coe_fn_to_embedding` & `initial_seg.coe_fn_to_rel_embedding` + -- → `InitialSeg.coe_coe_fn` + simpa only [Sum.lex_inr_inr, fr, InitialSeg.coe_coe_fn, Embedding.coeFn_mk] using + @RelEmbedding.map_rel_iff _ _ _ _ f.toRelEmbedding (Sum.inr a) (Sum.inr b)⟩, + fun a b H => by + rcases f.init' (by rw [fr] <;> exact Sum.lex_inr_inr.2 H) with ⟨a' | a', h⟩ + · rw [fl] at h + cases h + · rw [fr] at h + exact ⟨a', Sum.inr.inj h⟩⟩⟩⟩ +#align ordinal.add_contravariant_class_le Ordinal.add_contravariantClass_le + +theorem add_left_cancel (a) {b c : Ordinal} : a + b = a + c ↔ b = c := by + simp only [le_antisymm_iff, add_le_add_iff_left] +#align ordinal.add_left_cancel Ordinal.add_left_cancel + +private theorem add_lt_add_iff_left' (a) {b c : Ordinal} : a + b < a + c ↔ b < c := by + rw [← not_le, ← not_le, add_le_add_iff_left] + +instance add_covariantClass_lt : CovariantClass Ordinal.{u} Ordinal.{u} (· + ·) (· < ·) := + ⟨fun a _b _c => (add_lt_add_iff_left' a).2⟩ +#align ordinal.add_covariant_class_lt Ordinal.add_covariantClass_lt + +instance add_contravariantClass_lt : ContravariantClass Ordinal.{u} Ordinal.{u} (· + ·) (· < ·) := + ⟨fun a _b _c => (add_lt_add_iff_left' a).1⟩ +#align ordinal.add_contravariant_class_lt Ordinal.add_contravariantClass_lt + +instance add_swap_contravariantClass_lt : + ContravariantClass Ordinal.{u} Ordinal.{u} (swap (· + ·)) (· < ·) := + ⟨fun _a _b _c => lt_imp_lt_of_le_imp_le fun h => add_le_add_right h _⟩ +#align ordinal.add_swap_contravariant_class_lt Ordinal.add_swap_contravariantClass_lt + +theorem add_le_add_iff_right {a b : Ordinal} : ∀ n : ℕ, a + n ≤ b + n ↔ a ≤ b + | 0 => by simp + | n + 1 => by + simp only [nat_cast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right] +#align ordinal.add_le_add_iff_right Ordinal.add_le_add_iff_right + +theorem add_right_cancel {a b : Ordinal} (n : ℕ) : a + n = b + n ↔ a = b := by + simp only [le_antisymm_iff, add_le_add_iff_right] +#align ordinal.add_right_cancel Ordinal.add_right_cancel + +theorem add_eq_zero_iff {a b : Ordinal} : a + b = 0 ↔ a = 0 ∧ b = 0 := + inductionOn a fun α r _ => + inductionOn b fun β s _ => by + simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty] + exact isEmpty_sum +#align ordinal.add_eq_zero_iff Ordinal.add_eq_zero_iff + +theorem left_eq_zero_of_add_eq_zero {a b : Ordinal} (h : a + b = 0) : a = 0 := + (add_eq_zero_iff.1 h).1 +#align ordinal.left_eq_zero_of_add_eq_zero Ordinal.left_eq_zero_of_add_eq_zero + +theorem right_eq_zero_of_add_eq_zero {a b : Ordinal} (h : a + b = 0) : b = 0 := + (add_eq_zero_iff.1 h).2 +#align ordinal.right_eq_zero_of_add_eq_zero Ordinal.right_eq_zero_of_add_eq_zero + +/-! ### The predecessor of an ordinal -/ + + +/-- The ordinal predecessor of `o` is `o'` if `o = succ o'`, + and `o` otherwise. -/ +def pred (o : Ordinal) : Ordinal := + if h : ∃ a, o = succ a then Classical.choose h else o +#align ordinal.pred Ordinal.pred + +@[simp] +theorem pred_succ (o) : pred (succ o) = o := by + have h : ∃ a, succ o = succ a := ⟨_, rfl⟩; + simpa only [pred, dif_pos h] using (succ_injective <| Classical.choose_spec h).symm +#align ordinal.pred_succ Ordinal.pred_succ + +theorem pred_le_self (o) : pred o ≤ o := + if h : ∃ a, o = succ a then by + let ⟨a, e⟩ := h + rw [e, pred_succ]; exact le_succ a + else by rw [pred, dif_neg h] +#align ordinal.pred_le_self Ordinal.pred_le_self + +theorem pred_eq_iff_not_succ {o} : pred o = o ↔ ¬∃ a, o = succ a := + ⟨fun e ⟨a, e'⟩ => by rw [e', pred_succ] at e; exact (lt_succ a).ne e, fun h => dif_neg h⟩ +#align ordinal.pred_eq_iff_not_succ Ordinal.pred_eq_iff_not_succ + +theorem pred_eq_iff_not_succ' {o} : pred o = o ↔ ∀ a, o ≠ succ a := by + simpa using pred_eq_iff_not_succ +#align ordinal.pred_eq_iff_not_succ' Ordinal.pred_eq_iff_not_succ' + +theorem pred_lt_iff_is_succ {o} : pred o < o ↔ ∃ a, o = succ a := + Iff.trans (by simp only [le_antisymm_iff, pred_le_self, true_and_iff, not_le]) + (iff_not_comm.1 pred_eq_iff_not_succ).symm +#align ordinal.pred_lt_iff_is_succ Ordinal.pred_lt_iff_is_succ + +@[simp] +theorem pred_zero : pred 0 = 0 := + pred_eq_iff_not_succ'.2 fun a => (succ_ne_zero a).symm +#align ordinal.pred_zero Ordinal.pred_zero + +theorem succ_pred_iff_is_succ {o} : succ (pred o) = o ↔ ∃ a, o = succ a := + ⟨fun e => ⟨_, e.symm⟩, fun ⟨a, e⟩ => by simp only [e, pred_succ]⟩ +#align ordinal.succ_pred_iff_is_succ Ordinal.succ_pred_iff_is_succ + +theorem succ_lt_of_not_succ {o b : Ordinal} (h : ¬∃ a, o = succ a) : succ b < o ↔ b < o := + ⟨(lt_succ b).trans, fun l => lt_of_le_of_ne (succ_le_of_lt l) fun e => h ⟨_, e.symm⟩⟩ +#align ordinal.succ_lt_of_not_succ Ordinal.succ_lt_of_not_succ + +theorem lt_pred {a b} : a < pred b ↔ succ a < b := + if h : ∃ a, b = succ a then by + let ⟨c, e⟩ := h + rw [e, pred_succ, succ_lt_succ_iff] + else by simp only [pred, dif_neg h, succ_lt_of_not_succ h] +#align ordinal.lt_pred Ordinal.lt_pred + +theorem pred_le {a b} : pred a ≤ b ↔ a ≤ succ b := + le_iff_le_iff_lt_iff_lt.2 lt_pred +#align ordinal.pred_le Ordinal.pred_le + +@[simp] +theorem lift_is_succ {o : Ordinal.{v}} : (∃ a, lift.{u} o = succ a) ↔ ∃ a, o = succ a := + ⟨fun ⟨a, h⟩ => + let ⟨b, e⟩ := lift_down <| show a ≤ lift.{u} o from le_of_lt <| h.symm ▸ lt_succ a + ⟨b, lift_inj.1 <| by rw [h, ← e, lift_succ]⟩, + fun ⟨a, h⟩ => ⟨lift.{u} a, by simp only [h, lift_succ]⟩⟩ +#align ordinal.lift_is_succ Ordinal.lift_is_succ + +@[simp] +theorem lift_pred (o : Ordinal.{v}) : lift.{u} (pred o) = pred (lift.{u} o) := + if h : ∃ a, o = succ a then by cases' h with a e; simp only [e, pred_succ, lift_succ] + else by rw [pred_eq_iff_not_succ.2 h, pred_eq_iff_not_succ.2 (mt lift_is_succ.1 h)] +#align ordinal.lift_pred Ordinal.lift_pred + +/-! ### Limit ordinals -/ + + +/-- A limit ordinal is an ordinal which is not zero and not a successor. -/ +def IsLimit (o : Ordinal) : Prop := + o ≠ 0 ∧ ∀ a < o, succ a < o +#align ordinal.is_limit Ordinal.IsLimit + +theorem IsLimit.succ_lt {o a : Ordinal} (h : IsLimit o) : a < o → succ a < o := + h.2 a +#align ordinal.is_limit.succ_lt Ordinal.IsLimit.succ_lt + +theorem not_zero_isLimit : ¬IsLimit 0 + | ⟨h, _⟩ => h rfl +#align ordinal.not_zero_is_limit Ordinal.not_zero_isLimit + +theorem not_succ_isLimit (o) : ¬IsLimit (succ o) + | ⟨_, h⟩ => lt_irrefl _ (h _ (lt_succ o)) +#align ordinal.not_succ_is_limit Ordinal.not_succ_isLimit + +theorem not_succ_of_isLimit {o} (h : IsLimit o) : ¬∃ a, o = succ a + | ⟨a, e⟩ => not_succ_isLimit a (e ▸ h) +#align ordinal.not_succ_of_is_limit Ordinal.not_succ_of_isLimit + +theorem succ_lt_of_isLimit {o a : Ordinal} (h : IsLimit o) : succ a < o ↔ a < o := + ⟨(lt_succ a).trans, h.2 _⟩ +#align ordinal.succ_lt_of_is_limit Ordinal.succ_lt_of_isLimit + +theorem le_succ_of_isLimit {o} (h : IsLimit o) {a} : o ≤ succ a ↔ o ≤ a := + le_iff_le_iff_lt_iff_lt.2 <| succ_lt_of_isLimit h +#align ordinal.le_succ_of_is_limit Ordinal.le_succ_of_isLimit + +theorem limit_le {o} (h : IsLimit o) {a} : o ≤ a ↔ ∀ x < o, x ≤ a := + ⟨fun h _x l => l.le.trans h, fun H => + (le_succ_of_isLimit h).1 <| le_of_not_lt fun hn => not_lt_of_le (H _ hn) (lt_succ a)⟩ +#align ordinal.limit_le Ordinal.limit_le + +theorem lt_limit {o} (h : IsLimit o) {a} : a < o ↔ ∃ x < o, a < x := by + -- Porting note: `bex_def` is required. + simpa only [not_ball, not_le, bex_def] using not_congr (@limit_le _ h a) +#align ordinal.lt_limit Ordinal.lt_limit + +@[simp] +theorem lift_isLimit (o) : IsLimit (lift o) ↔ IsLimit o := + and_congr (not_congr <| by simpa only [lift_zero] using @lift_inj o 0) + ⟨fun H a h => lift_lt.1 <| by simpa only [lift_succ] using H _ (lift_lt.2 h), fun H a h => + by + obtain ⟨a', rfl⟩ := lift_down h.le + rw [← lift_succ, lift_lt] + exact H a' (lift_lt.1 h)⟩ +#align ordinal.lift_is_limit Ordinal.lift_isLimit + +theorem IsLimit.pos {o : Ordinal} (h : IsLimit o) : 0 < o := + lt_of_le_of_ne (Ordinal.zero_le _) h.1.symm +#align ordinal.is_limit.pos Ordinal.IsLimit.pos + +theorem IsLimit.one_lt {o : Ordinal} (h : IsLimit o) : 1 < o := by + simpa only [succ_zero] using h.2 _ h.pos +#align ordinal.is_limit.one_lt Ordinal.IsLimit.one_lt + +theorem IsLimit.nat_lt {o : Ordinal} (h : IsLimit o) : ∀ n : ℕ, (n : Ordinal) < o + | 0 => h.pos + | n + 1 => h.2 _ (IsLimit.nat_lt h n) +#align ordinal.is_limit.nat_lt Ordinal.IsLimit.nat_lt + +theorem zero_or_succ_or_limit (o : Ordinal) : o = 0 ∨ (∃ a, o = succ a) ∨ IsLimit o := + if o0 : o = 0 then Or.inl o0 + else + if h : ∃ a, o = succ a then Or.inr (Or.inl h) + else Or.inr <| Or.inr ⟨o0, fun _a => (succ_lt_of_not_succ h).2⟩ +#align ordinal.zero_or_succ_or_limit Ordinal.zero_or_succ_or_limit + +/-- Main induction principle of ordinals: if one can prove a property by + induction at successor ordinals and at limit ordinals, then it holds for all ordinals. -/ +@[elab_as_elim] +def limitRecOn {C : Ordinal → Sort _} (o : Ordinal) (H₁ : C 0) (H₂ : ∀ o, C o → C (succ o)) + (H₃ : ∀ o, IsLimit o → (∀ o' < o, C o') → C o) : C o := + lt_wf.fix + (fun o IH => + if o0 : o = 0 then by rw [o0]; exact H₁ + else + if h : ∃ a, o = succ a then by + rw [← succ_pred_iff_is_succ.2 h]; exact H₂ _ (IH _ <| pred_lt_iff_is_succ.2 h) + else H₃ _ ⟨o0, fun a => (succ_lt_of_not_succ h).2⟩ IH) + o +#align ordinal.limit_rec_on Ordinal.limitRecOn + +@[simp] +theorem limitRecOn_zero {C} (H₁ H₂ H₃) : @limitRecOn C 0 H₁ H₂ H₃ = H₁ := by + rw [limitRecOn, lt_wf.fix_eq, dif_pos rfl]; rfl +#align ordinal.limit_rec_on_zero Ordinal.limitRecOn_zero + +@[simp] +theorem limitRecOn_succ {C} (o H₁ H₂ H₃) : + @limitRecOn C (succ o) H₁ H₂ H₃ = H₂ o (@limitRecOn C o H₁ H₂ H₃) := by + have h : ∃ a, succ o = succ a := ⟨_, rfl⟩ + rw [limitRecOn, lt_wf.fix_eq, dif_neg (succ_ne_zero o), dif_pos h] + generalize limitRecOn.proof_2 (succ o) h = h₂ + generalize limitRecOn.proof_3 (succ o) h = h₃ + revert h₂ h₃; generalize e : pred (succ o) = o'; intros + rw [pred_succ] at e; subst o'; rfl +#align ordinal.limit_rec_on_succ Ordinal.limitRecOn_succ + +@[simp] +theorem limitRecOn_limit {C} (o H₁ H₂ H₃ h) : + @limitRecOn C o H₁ H₂ H₃ = H₃ o h fun x _h => @limitRecOn C x H₁ H₂ H₃ := by + rw [limitRecOn, lt_wf.fix_eq, dif_neg h.1, dif_neg (not_succ_of_isLimit h)]; rfl +#align ordinal.limit_rec_on_limit Ordinal.limitRecOn_limit + +instance orderTopOutSucc (o : Ordinal) : OrderTop (succ o).out.α := + @OrderTop.mk _ _ (Top.mk _) le_enum_succ +#align ordinal.order_top_out_succ Ordinal.orderTopOutSucc + +theorem enum_succ_eq_top {o : Ordinal} : + enum (· < ·) o + (by + rw [type_lt] + exact lt_succ o) = + (⊤ : (succ o).out.α) := + rfl +#align ordinal.enum_succ_eq_top Ordinal.enum_succ_eq_top + +theorem has_succ_of_type_succ_lt {α} {r : α → α → Prop} [wo : IsWellOrder α r] + (h : ∀ a < type r, succ a < type r) (x : α) : ∃ y, r x y := by + use enum r (succ (typein r x)) (h _ (typein_lt_type r x)) + convert (enum_lt_enum (typein_lt_type r x) + (h _ (typein_lt_type r x))).mpr (lt_succ _); rw [enum_typein] +#align ordinal.has_succ_of_type_succ_lt Ordinal.has_succ_of_type_succ_lt + +theorem out_no_max_of_succ_lt {o : Ordinal} (ho : ∀ a < o, succ a < o) : NoMaxOrder o.out.α := + ⟨has_succ_of_type_succ_lt (by rwa [type_lt])⟩ +#align ordinal.out_no_max_of_succ_lt Ordinal.out_no_max_of_succ_lt + +theorem bounded_singleton {r : α → α → Prop} [IsWellOrder α r] (hr : (type r).IsLimit) (x) : + Bounded r {x} := by + refine' ⟨enum r (succ (typein r x)) (hr.2 _ (typein_lt_type r x)), _⟩ + intro b hb + rw [mem_singleton_iff.1 hb] + nth_rw 1 [← enum_typein r x] + rw [@enum_lt_enum _ r] + apply lt_succ +#align ordinal.bounded_singleton Ordinal.bounded_singleton + +-- Porting note: `· < ·` requires a type ascription for an `IsWellOrder` instance. +theorem type_subrel_lt (o : Ordinal.{u}) : + type (Subrel ((· < ·) : Ordinal → Ordinal → Prop) { o' : Ordinal | o' < o }) + = Ordinal.lift.{u + 1} o := by + refine' Quotient.inductionOn o _ + rintro ⟨α, r, wo⟩; skip; apply Quotient.sound + -- Porting note: `symm; refine' [term]` → `refine' [term].symm` + constructor; refine' ((RelIso.preimage Equiv.ulift r).trans (enumIso r).symm).symm +#align ordinal.type_subrel_lt Ordinal.type_subrel_lt + +theorem mk_initialSeg (o : Ordinal.{u}) : + (#{ o' : Ordinal | o' < o }) = Cardinal.lift.{u + 1} o.card := by + rw [lift_card, ← type_subrel_lt, card_type] +#align ordinal.mk_initial_seg Ordinal.mk_initialSeg + +/-! ### Normal ordinal functions -/ + + +/-- A normal ordinal function is a strictly increasing function which is + order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for + `a < o`. -/ +def IsNormal (f : Ordinal → Ordinal) : Prop := + (∀ o, f o < f (succ o)) ∧ ∀ o, IsLimit o → ∀ a, f o ≤ a ↔ ∀ b < o, f b ≤ a +#align ordinal.is_normal Ordinal.IsNormal + +theorem IsNormal.limit_le {f} (H : IsNormal f) : + ∀ {o}, IsLimit o → ∀ {a}, f o ≤ a ↔ ∀ b < o, f b ≤ a := + @H.2 +#align ordinal.is_normal.limit_le Ordinal.IsNormal.limit_le + +theorem IsNormal.limit_lt {f} (H : IsNormal f) {o} (h : IsLimit o) {a} : + a < f o ↔ ∃ b < o, a < f b := + not_iff_not.1 <| by simpa only [exists_prop, not_exists, not_and, not_lt] using H.2 _ h a +#align ordinal.is_normal.limit_lt Ordinal.IsNormal.limit_lt + +theorem IsNormal.strictMono {f} (H : IsNormal f) : StrictMono f := fun a b => + limitRecOn b (Not.elim (not_lt_of_le <| Ordinal.zero_le _)) + (fun _b IH h => + (lt_or_eq_of_le (le_of_lt_succ h)).elim (fun h => (IH h).trans (H.1 _)) fun e => e ▸ H.1 _) + fun _b l _IH h => lt_of_lt_of_le (H.1 a) ((H.2 _ l _).1 le_rfl _ (l.2 _ h)) +#align ordinal.is_normal.strict_mono Ordinal.IsNormal.strictMono + +theorem IsNormal.monotone {f} (H : IsNormal f) : Monotone f := + H.strictMono.monotone +#align ordinal.is_normal.monotone Ordinal.IsNormal.monotone + +theorem isNormal_iff_strictMono_limit (f : Ordinal → Ordinal) : + IsNormal f ↔ StrictMono f ∧ ∀ o, IsLimit o → ∀ a, (∀ b < o, f b ≤ a) → f o ≤ a := + ⟨fun hf => ⟨hf.strictMono, fun a ha c => (hf.2 a ha c).2⟩, fun ⟨hs, hl⟩ => + ⟨fun a => hs (lt_succ a), fun a ha c => + ⟨fun hac _b hba => ((hs hba).trans_le hac).le, hl a ha c⟩⟩⟩ +#align ordinal.is_normal_iff_strict_mono_limit Ordinal.isNormal_iff_strictMono_limit + +theorem IsNormal.lt_iff {f} (H : IsNormal f) {a b} : f a < f b ↔ a < b := + StrictMono.lt_iff_lt <| H.strictMono +#align ordinal.is_normal.lt_iff Ordinal.IsNormal.lt_iff + +theorem IsNormal.le_iff {f} (H : IsNormal f) {a b} : f a ≤ f b ↔ a ≤ b := + le_iff_le_iff_lt_iff_lt.2 H.lt_iff +#align ordinal.is_normal.le_iff Ordinal.IsNormal.le_iff + +theorem IsNormal.inj {f} (H : IsNormal f) {a b} : f a = f b ↔ a = b := by + simp only [le_antisymm_iff, H.le_iff] +#align ordinal.is_normal.inj Ordinal.IsNormal.inj + +theorem IsNormal.self_le {f} (H : IsNormal f) (a) : a ≤ f a := + lt_wf.self_le_of_strictMono H.strictMono a +#align ordinal.is_normal.self_le Ordinal.IsNormal.self_le + +theorem IsNormal.le_set {f o} (H : IsNormal f) (p : Set Ordinal) (p0 : p.Nonempty) (b) + (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o := + ⟨fun h a pa => (H.le_iff.2 ((H₂ _).1 le_rfl _ pa)).trans h, fun h => by + -- Porting note: `refine'` didn't work well so `induction` is used + induction b using limitRecOn with + | H₁ => + cases' p0 with x px + have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px) + rw [this] at px + exact h _ px + | H₂ S _ => + rcases not_ball.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩ + exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁) + | H₃ S L _ => + refine' (H.2 _ L _).2 fun a h' => _ + rcases not_ball.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩ + exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)⟩ +#align ordinal.is_normal.le_set Ordinal.IsNormal.le_set + +theorem IsNormal.le_set' {f o} (H : IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal) (b) + (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, g a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o := by + simpa [H₂] using H.le_set (g '' p) (p0.image g) b +#align ordinal.is_normal.le_set' Ordinal.IsNormal.le_set' + +theorem IsNormal.refl : IsNormal id := + ⟨lt_succ, fun _o l _a => Ordinal.limit_le l⟩ +#align ordinal.is_normal.refl Ordinal.IsNormal.refl + +theorem IsNormal.trans {f g} (H₁ : IsNormal f) (H₂ : IsNormal g) : IsNormal (f ∘ g) := + ⟨fun _x => H₁.lt_iff.2 (H₂.1 _), fun o l _a => + H₁.le_set' (· < o) ⟨0, l.pos⟩ g _ fun _c => H₂.2 _ l _⟩ +#align ordinal.is_normal.trans Ordinal.IsNormal.trans + +theorem IsNormal.isLimit {f} (H : IsNormal f) {o} (l : IsLimit o) : IsLimit (f o) := + ⟨ne_of_gt <| (Ordinal.zero_le _).trans_lt <| H.lt_iff.2 l.pos, fun _ h => + let ⟨_b, h₁, h₂⟩ := (H.limit_lt l).1 h + (succ_le_of_lt h₂).trans_lt (H.lt_iff.2 h₁)⟩ +#align ordinal.is_normal.is_limit Ordinal.IsNormal.isLimit + +theorem IsNormal.le_iff_eq {f} (H : IsNormal f) {a} : f a ≤ a ↔ f a = a := + (H.self_le a).le_iff_eq +#align ordinal.is_normal.le_iff_eq Ordinal.IsNormal.le_iff_eq + +theorem add_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c := + ⟨fun h b' l => (add_le_add_left l.le _).trans h, fun H => + le_of_not_lt <| by + -- Porting note: `induction` tactics are required because of the parser bug. + induction a using inductionOn with + | H α r => + induction b using inductionOn with + | H β s => + intro l + suffices ∀ x : β, Sum.Lex r s (Sum.inr x) (enum _ _ l) by + -- Porting note: `revert` & `intro` is required because `cases'` doesn't replace + -- `enum _ _ l` in `this`. + revert this; cases' enum _ _ l with x x <;> intro this + · cases this (enum s 0 h.pos) + · exact irrefl _ (this _) + intro x + rw [← typein_lt_typein (Sum.Lex r s), typein_enum] + have := H _ (h.2 _ (typein_lt_type s x)) + rw [add_succ, succ_le_iff] at this + refine' + (RelEmbedding.ofMonotone (fun a => _) fun a b => _).ordinal_type_le.trans_lt this + · rcases a with ⟨a | b, h⟩ + · exact Sum.inl a + · exact Sum.inr ⟨b, by cases h; assumption⟩ + · rcases a with ⟨a | a, h₁⟩ <;> rcases b with ⟨b | b, h₂⟩ <;> cases h₁ <;> cases h₂ <;> + rintro ⟨⟩ <;> constructor <;> assumption⟩ +#align ordinal.add_le_of_limit Ordinal.add_le_of_limit + +theorem add_isNormal (a : Ordinal) : IsNormal ((· + ·) a) := + ⟨fun b => (add_lt_add_iff_left a).2 (lt_succ b), fun _b l _c => add_le_of_limit l⟩ +#align ordinal.add_is_normal Ordinal.add_isNormal + +theorem add_isLimit (a) {b} : IsLimit b → IsLimit (a + b) := + (add_isNormal a).isLimit +#align ordinal.add_is_limit Ordinal.add_isLimit + +alias add_isLimit ← IsLimit.add +#align ordinal.is_limit.add Ordinal.IsLimit.add + +/-! ### Subtraction on ordinals-/ + + +/-- The set in the definition of subtraction is nonempty. -/ +theorem sub_nonempty {a b : Ordinal} : { o | a ≤ b + o }.Nonempty := + ⟨a, le_add_left _ _⟩ +#align ordinal.sub_nonempty Ordinal.sub_nonempty + +/-- `a - b` is the unique ordinal satisfying `b + (a - b) = a` when `b ≤ a`. -/ +instance : Sub Ordinal := + ⟨fun a b => infₛ { o | a ≤ b + o }⟩ + +theorem le_add_sub (a b : Ordinal) : a ≤ b + (a - b) := + cinfₛ_mem sub_nonempty +#align ordinal.le_add_sub Ordinal.le_add_sub + +theorem sub_le {a b c : Ordinal} : a - b ≤ c ↔ a ≤ b + c := + ⟨fun h => (le_add_sub a b).trans (add_le_add_left h _), fun h => cinfₛ_le' h⟩ +#align ordinal.sub_le Ordinal.sub_le + +theorem lt_sub {a b c : Ordinal} : a < b - c ↔ c + a < b := + lt_iff_lt_of_le_iff_le sub_le +#align ordinal.lt_sub Ordinal.lt_sub + +theorem add_sub_cancel (a b : Ordinal) : a + b - a = b := + le_antisymm (sub_le.2 <| le_rfl) ((add_le_add_iff_left a).1 <| le_add_sub _ _) +#align ordinal.add_sub_cancel Ordinal.add_sub_cancel + +theorem sub_eq_of_add_eq {a b c : Ordinal} (h : a + b = c) : c - a = b := + h ▸ add_sub_cancel _ _ +#align ordinal.sub_eq_of_add_eq Ordinal.sub_eq_of_add_eq + +theorem sub_le_self (a b : Ordinal) : a - b ≤ a := + sub_le.2 <| le_add_left _ _ +#align ordinal.sub_le_self Ordinal.sub_le_self + +protected theorem add_sub_cancel_of_le {a b : Ordinal} (h : b ≤ a) : b + (a - b) = a := + (le_add_sub a b).antisymm' + (by + rcases zero_or_succ_or_limit (a - b) with (e | ⟨c, e⟩ | l) + · simp only [e, add_zero, h] + · rw [e, add_succ, succ_le_iff, ← lt_sub, e] + exact lt_succ c + · exact (add_le_of_limit l).2 fun c l => (lt_sub.1 l).le) +#align ordinal.add_sub_cancel_of_le Ordinal.add_sub_cancel_of_le + +theorem le_sub_of_le {a b c : Ordinal} (h : b ≤ a) : c ≤ a - b ↔ b + c ≤ a := by + rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h] +#align ordinal.le_sub_of_le Ordinal.le_sub_of_le + +theorem sub_lt_of_le {a b c : Ordinal} (h : b ≤ a) : a - b < c ↔ a < b + c := + lt_iff_lt_of_le_iff_le (le_sub_of_le h) +#align ordinal.sub_lt_of_le Ordinal.sub_lt_of_le + +instance : ExistsAddOfLE Ordinal := + ⟨fun h => ⟨_, (Ordinal.add_sub_cancel_of_le h).symm⟩⟩ + +@[simp] +theorem sub_zero (a : Ordinal) : a - 0 = a := by simpa only [zero_add] using add_sub_cancel 0 a +#align ordinal.sub_zero Ordinal.sub_zero + +@[simp] +theorem zero_sub (a : Ordinal) : 0 - a = 0 := by rw [← Ordinal.le_zero]; apply sub_le_self +#align ordinal.zero_sub Ordinal.zero_sub + +@[simp] +theorem sub_self (a : Ordinal) : a - a = 0 := by simpa only [add_zero] using add_sub_cancel a 0 +#align ordinal.sub_self Ordinal.sub_self + +protected theorem sub_eq_zero_iff_le {a b : Ordinal} : a - b = 0 ↔ a ≤ b := + ⟨fun h => by simpa only [h, add_zero] using le_add_sub a b, fun h => by + rwa [← Ordinal.le_zero, sub_le, add_zero]⟩ +#align ordinal.sub_eq_zero_iff_le Ordinal.sub_eq_zero_iff_le + +theorem sub_sub (a b c : Ordinal) : a - b - c = a - (b + c) := + eq_of_forall_ge_iff fun d => by rw [sub_le, sub_le, sub_le, add_assoc] +#align ordinal.sub_sub Ordinal.sub_sub + +theorem add_sub_add_cancel (a b c : Ordinal) : a + b - (a + c) = b - c := by + rw [← sub_sub, add_sub_cancel] +#align ordinal.add_sub_add_cancel Ordinal.add_sub_add_cancel + +theorem sub_isLimit {a b} (l : IsLimit a) (h : b < a) : IsLimit (a - b) := + ⟨ne_of_gt <| lt_sub.2 <| by rwa [add_zero], fun c h => by + rw [lt_sub, add_succ]; exact l.2 _ (lt_sub.1 h)⟩ +#align ordinal.sub_is_limit Ordinal.sub_isLimit + +-- @[simp] -- Porting note: simp can prove this +theorem one_add_omega : 1 + ω = ω := by + refine' le_antisymm _ (le_add_left _ _) + rw [omega, ← lift_one.{_, 0}, ← lift_add, lift_le, ← type_unit, ← type_sum_lex] + refine' ⟨RelEmbedding.collapse (RelEmbedding.ofMonotone _ _)⟩ + · apply Sum.rec + exact fun _ => 0 + exact Nat.succ + · intro a b + cases a <;> cases b <;> intro H <;> cases' H with _ _ H _ _ H <;> + [exact H.elim, exact Nat.succ_pos _, exact Nat.succ_lt_succ H] +#align ordinal.one_add_omega Ordinal.one_add_omega + +@[simp] +theorem one_add_of_omega_le {o} (h : ω ≤ o) : 1 + o = o := by + rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, one_add_omega] +#align ordinal.one_add_of_omega_le Ordinal.one_add_of_omega_le + +/-! ### Multiplication of ordinals-/ + + +/-- The multiplication of ordinals `o₁` and `o₂` is the (well founded) lexicographic order on +`o₂ × o₁`. -/ +instance monoid : Monoid Ordinal.{u} + where + mul a b := + Quotient.liftOn₂ a b + (fun ⟨α, r, wo⟩ ⟨β, s, wo'⟩ => ⟦⟨β × α, Prod.Lex s r, inferInstance⟩⟧ : + WellOrder → WellOrder → Ordinal) + fun ⟨α₁, r₁, o₁⟩ ⟨α₂, r₂, o₂⟩ ⟨β₁, s₁, p₁⟩ ⟨β₂, s₂, p₂⟩ ⟨f⟩ ⟨g⟩ => + Quot.sound ⟨RelIso.prodLexCongr g f⟩ + one := 1 + mul_assoc a b c := + Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ => + Eq.symm <| + Quotient.sound + ⟨⟨prodAssoc _ _ _, @fun a b => by + rcases a with ⟨⟨a₁, a₂⟩, a₃⟩ + rcases b with ⟨⟨b₁, b₂⟩, b₃⟩ + simp [Prod.lex_def, and_or_left, or_assoc, and_assoc]⟩⟩ + mul_one a := + inductionOn a fun α r _ => + Quotient.sound + ⟨⟨punitProd _, @fun a b => by + rcases a with ⟨⟨⟨⟩⟩, a⟩; rcases b with ⟨⟨⟨⟩⟩, b⟩ + simp only [Prod.lex_def, EmptyRelation, false_or_iff] + simp only [eq_self_iff_true, true_and_iff] + rfl⟩⟩ + one_mul a := + inductionOn a fun α r _ => + Quotient.sound + ⟨⟨prodPUnit _, @fun a b => by + rcases a with ⟨a, ⟨⟨⟩⟩⟩; rcases b with ⟨b, ⟨⟨⟩⟩⟩ + simp only [Prod.lex_def, EmptyRelation, and_false_iff, or_false_iff] + rfl⟩⟩ + +@[simp] +theorem type_prod_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] + [IsWellOrder β s] : type (Prod.Lex s r) = type r * type s := + rfl +#align ordinal.type_prod_lex Ordinal.type_prod_lex + +private theorem mul_eq_zero' {a b : Ordinal} : a * b = 0 ↔ a = 0 ∨ b = 0 := + inductionOn a fun α _ _ => + inductionOn b fun β _ _ => + by + simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty] + rw [or_comm] + exact isEmpty_prod + +instance : MonoidWithZero Ordinal := + { Ordinal.monoid with + zero := 0 + mul_zero := fun _a => mul_eq_zero'.2 <| Or.inr rfl + zero_mul := fun _a => mul_eq_zero'.2 <| Or.inl rfl } + +instance : NoZeroDivisors Ordinal := + ⟨fun {_ _} => mul_eq_zero'.1⟩ + +@[simp] +theorem lift_mul (a b : Ordinal.{v}) : lift.{u} (a * b) = lift.{u} a * lift.{u} b := + Quotient.inductionOn₂ a b fun ⟨_α, _r, _⟩ ⟨_β, _s, _⟩ => + Quotient.sound + ⟨(RelIso.preimage Equiv.ulift _).trans + (RelIso.prodLexCongr (RelIso.preimage Equiv.ulift _) + (RelIso.preimage Equiv.ulift _)).symm⟩ +#align ordinal.lift_mul Ordinal.lift_mul + +@[simp] +theorem card_mul (a b) : card (a * b) = card a * card b := + Quotient.inductionOn₂ a b fun ⟨α, _r, _⟩ ⟨β, _s, _⟩ => mul_comm (#β) (#α) +#align ordinal.card_mul Ordinal.card_mul + +instance : LeftDistribClass Ordinal.{u} := + ⟨fun a b c => + Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ => + Quotient.sound + ⟨⟨sumProdDistrib _ _ _, by + rintro ⟨a₁ | a₁, a₂⟩ ⟨b₁ | b₁, b₂⟩ <;> + simp only [Prod.lex_def, Sum.lex_inl_inl, Sum.Lex.sep, Sum.lex_inr_inl, + Sum.lex_inr_inr, sumProdDistrib_apply_left, sumProdDistrib_apply_right] <;> + -- Porting note: `Sum.inr.inj_iff` is required. + simp only [Sum.inl.inj_iff, Sum.inr.inj_iff, + true_or_iff, false_and_iff, false_or_iff]⟩⟩⟩ + +theorem mul_succ (a b : Ordinal) : a * succ b = a * b + a := + mul_add_one a b +#align ordinal.mul_succ Ordinal.mul_succ + +instance mul_covariantClass_le : CovariantClass Ordinal.{u} Ordinal.{u} (· * ·) (· ≤ ·) := + ⟨fun c a b => + Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩ => by + refine' + (RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, a.2)) fun a b h => _).ordinal_type_le + cases' h with a₁ b₁ a₂ b₂ h' a b₁ b₂ h' + · exact Prod.Lex.left _ _ (f.toRelEmbedding.map_rel_iff.2 h') + · exact Prod.Lex.right _ h'⟩ +#align ordinal.mul_covariant_class_le Ordinal.mul_covariantClass_le + +instance mul_swap_covariantClass_le : + CovariantClass Ordinal.{u} Ordinal.{u} (swap (· * ·)) (· ≤ ·) := + ⟨fun c a b => + Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩ => by + refine' + (RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => _).ordinal_type_le + cases' h with a₁ b₁ a₂ b₂ h' a b₁ b₂ h' + · exact Prod.Lex.left _ _ h' + · exact Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')⟩ +#align ordinal.mul_swap_covariant_class_le Ordinal.mul_swap_covariantClass_le + +theorem le_mul_left (a : Ordinal) {b : Ordinal} (hb : 0 < b) : a ≤ a * b := by + convert mul_le_mul_left' (one_le_iff_pos.2 hb) a + rw [mul_one a] +#align ordinal.le_mul_left Ordinal.le_mul_left + +theorem le_mul_right (a : Ordinal) {b : Ordinal} (hb : 0 < b) : a ≤ b * a := by + convert mul_le_mul_right' (one_le_iff_pos.2 hb) a + rw [one_mul a] +#align ordinal.le_mul_right Ordinal.le_mul_right + +private theorem mul_le_of_limit_aux {α β r s} [IsWellOrder α r] [IsWellOrder β s] {c} + (h : IsLimit (type s)) (H : ∀ b' < type s, type r * b' ≤ c) (l : c < type r * type s) : + False := by + suffices ∀ a b, Prod.Lex s r (b, a) (enum _ _ l) by + cases' enum _ _ l with b a + exact irrefl _ (this _ _) + intro a b + rw [← typein_lt_typein (Prod.Lex s r), typein_enum] + have := H _ (h.2 _ (typein_lt_type s b)) + rw [mul_succ] at this + have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this + refine' (RelEmbedding.ofMonotone (fun a => _) fun a b => _).ordinal_type_le.trans_lt this + · rcases a with ⟨⟨b', a'⟩, h⟩ + by_cases e : b = b' + · refine' Sum.inr ⟨a', _⟩ + subst e + cases' h with _ _ _ _ h _ _ _ h + · exact (irrefl _ h).elim + · exact h + · refine' Sum.inl (⟨b', _⟩, a') + cases' h with _ _ _ _ h _ _ _ h + · exact h + · exact (e rfl).elim + · rcases a with ⟨⟨b₁, a₁⟩, h₁⟩ + rcases b with ⟨⟨b₂, a₂⟩, h₂⟩ + intro h + by_cases e₁ : b = b₁ <;> by_cases e₂ : b = b₂ + · substs b₁ b₂ + simpa only [subrel_val, Prod.lex_def, @irrefl _ s _ b, true_and_iff, false_or_iff, + eq_self_iff_true, dif_pos, Sum.lex_inr_inr] using h + · subst b₁ + simp only [subrel_val, Prod.lex_def, e₂, Prod.lex_def, dif_pos, subrel_val, eq_self_iff_true, + or_false_iff, dif_neg, not_false_iff, Sum.lex_inr_inl, false_and_iff] at h ⊢ + cases' h₂ with _ _ _ _ h₂_h h₂_h <;> [exact asymm h h₂_h, exact e₂ rfl] + -- Porting note: `cc` hadn't ported yet. + · simp [e₂, dif_neg e₁, show b₂ ≠ b₁ from e₂ ▸ e₁] + · simpa only [dif_neg e₁, dif_neg e₂, Prod.lex_def, subrel_val, Subtype.mk_eq_mk, + Sum.lex_inl_inl] using h + +theorem mul_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c := + ⟨fun h b' l => (mul_le_mul_left' l.le _).trans h, fun H => + -- Porting note: `induction` tactics are required because of the parser bug. + le_of_not_lt <| by + induction a using inductionOn with + | H α r => + induction b using inductionOn with + | H β s => + exact mul_le_of_limit_aux h H⟩ +#align ordinal.mul_le_of_limit Ordinal.mul_le_of_limit + +theorem mul_isNormal {a : Ordinal} (h : 0 < a) : IsNormal ((· * ·) a) := + -- Porting note: `dsimp only` is required for beta reduction. + ⟨fun b => by + dsimp only + rw [mul_succ] + simpa only [add_zero] using (add_lt_add_iff_left (a * b)).2 h, + fun b l c => mul_le_of_limit l⟩ +#align ordinal.mul_is_normal Ordinal.mul_isNormal + +theorem lt_mul_of_limit {a b c : Ordinal} (h : IsLimit c) : a < b * c ↔ ∃ c' < c, a < b * c' := by + -- Porting note: `bex_def` is required. + simpa only [not_ball, not_le, bex_def] using not_congr (@mul_le_of_limit b c a h) +#align ordinal.lt_mul_of_limit Ordinal.lt_mul_of_limit + +theorem mul_lt_mul_iff_left {a b c : Ordinal} (a0 : 0 < a) : a * b < a * c ↔ b < c := + (mul_isNormal a0).lt_iff +#align ordinal.mul_lt_mul_iff_left Ordinal.mul_lt_mul_iff_left + +theorem mul_le_mul_iff_left {a b c : Ordinal} (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c := + (mul_isNormal a0).le_iff +#align ordinal.mul_le_mul_iff_left Ordinal.mul_le_mul_iff_left + +theorem mul_lt_mul_of_pos_left {a b c : Ordinal} (h : a < b) (c0 : 0 < c) : c * a < c * b := + (mul_lt_mul_iff_left c0).2 h +#align ordinal.mul_lt_mul_of_pos_left Ordinal.mul_lt_mul_of_pos_left + +theorem mul_pos {a b : Ordinal} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by + simpa only [mul_zero] using mul_lt_mul_of_pos_left h₂ h₁ +#align ordinal.mul_pos Ordinal.mul_pos + +theorem mul_ne_zero {a b : Ordinal} : a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by + simpa only [Ordinal.pos_iff_ne_zero] using mul_pos +#align ordinal.mul_ne_zero Ordinal.mul_ne_zero + +theorem le_of_mul_le_mul_left {a b c : Ordinal} (h : c * a ≤ c * b) (h0 : 0 < c) : a ≤ b := + le_imp_le_of_lt_imp_lt (fun h' => mul_lt_mul_of_pos_left h' h0) h +#align ordinal.le_of_mul_le_mul_left Ordinal.le_of_mul_le_mul_left + +theorem mul_right_inj {a b c : Ordinal} (a0 : 0 < a) : a * b = a * c ↔ b = c := + (mul_isNormal a0).inj +#align ordinal.mul_right_inj Ordinal.mul_right_inj + +theorem mul_isLimit {a b : Ordinal} (a0 : 0 < a) : IsLimit b → IsLimit (a * b) := + (mul_isNormal a0).isLimit +#align ordinal.mul_is_limit Ordinal.mul_isLimit + +theorem mul_isLimit_left {a b : Ordinal} (l : IsLimit a) (b0 : 0 < b) : IsLimit (a * b) := by + rcases zero_or_succ_or_limit b with (rfl | ⟨b, rfl⟩ | lb) + · exact b0.false.elim + · rw [mul_succ] + exact add_isLimit _ l + · exact mul_isLimit l.pos lb +#align ordinal.mul_is_limit_left Ordinal.mul_isLimit_left + +theorem smul_eq_mul : ∀ (n : ℕ) (a : Ordinal), n • a = a * n + | 0, a => by rw [zero_smul, Nat.cast_zero, mul_zero] + | n + 1, a => by rw [succ_nsmul', Nat.cast_add, mul_add, Nat.cast_one, mul_one, smul_eq_mul n] +#align ordinal.smul_eq_mul Ordinal.smul_eq_mul + +/-! ### Division on ordinals -/ + + +/-- The set in the definition of division is nonempty. -/ +theorem div_nonempty {a b : Ordinal} (h : b ≠ 0) : { o | a < b * succ o }.Nonempty := + ⟨a, (succ_le_iff (a := a) (b := b * succ a)).1 <| by + simpa only [succ_zero, one_mul] using + mul_le_mul_right' (succ_le_of_lt (Ordinal.pos_iff_ne_zero.2 h)) (succ a)⟩ +#align ordinal.div_nonempty Ordinal.div_nonempty + +/-- `a / b` is the unique ordinal `o` satisfying `a = b * o + o'` with `o' < b`. -/ +instance : Div Ordinal := + ⟨fun a b => if _h : b = 0 then 0 else infₛ { o | a < b * succ o }⟩ + +@[simp] +theorem div_zero (a : Ordinal) : a / 0 = 0 := + dif_pos rfl +#align ordinal.div_zero Ordinal.div_zero + +theorem div_def (a) {b : Ordinal} (h : b ≠ 0) : a / b = infₛ { o | a < b * succ o } := + dif_neg h +#align ordinal.div_def Ordinal.div_def + +theorem lt_mul_succ_div (a) {b : Ordinal} (h : b ≠ 0) : a < b * succ (a / b) := by + rw [div_def a h]; exact cinfₛ_mem (div_nonempty h) +#align ordinal.lt_mul_succ_div Ordinal.lt_mul_succ_div + +theorem lt_mul_div_add (a) {b : Ordinal} (h : b ≠ 0) : a < b * (a / b) + b := by + simpa only [mul_succ] using lt_mul_succ_div a h +#align ordinal.lt_mul_div_add Ordinal.lt_mul_div_add + +theorem div_le {a b c : Ordinal} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * succ c := + ⟨fun h => (lt_mul_succ_div a b0).trans_le (mul_le_mul_left' (succ_le_succ_iff.2 h) _), fun h => by + rw [div_def a b0]; exact cinfₛ_le' h⟩ +#align ordinal.div_le Ordinal.div_le + +theorem lt_div {a b c : Ordinal} (h : c ≠ 0) : a < b / c ↔ c * succ a ≤ b := by + rw [← not_le, div_le h, not_lt] +#align ordinal.lt_div Ordinal.lt_div + +theorem div_pos {b c : Ordinal} (h : c ≠ 0) : 0 < b / c ↔ c ≤ b := by simp [lt_div h] +#align ordinal.div_pos Ordinal.div_pos + +theorem le_div {a b c : Ordinal} (c0 : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b := by + apply limitRecOn a + · simp only [mul_zero, Ordinal.zero_le] + · intros + rw [succ_le_iff, lt_div c0] + · + simp (config := { contextual := true }) only [mul_le_of_limit, limit_le, iff_self_iff, + forall_true_iff] +#align ordinal.le_div Ordinal.le_div + +theorem div_lt {a b c : Ordinal} (b0 : b ≠ 0) : a / b < c ↔ a < b * c := + lt_iff_lt_of_le_iff_le <| le_div b0 +#align ordinal.div_lt Ordinal.div_lt + +theorem div_le_of_le_mul {a b c : Ordinal} (h : a ≤ b * c) : a / b ≤ c := + if b0 : b = 0 then by simp only [b0, div_zero, Ordinal.zero_le] + else + (div_le b0).2 <| h.trans_lt <| mul_lt_mul_of_pos_left (lt_succ c) (Ordinal.pos_iff_ne_zero.2 b0) +#align ordinal.div_le_of_le_mul Ordinal.div_le_of_le_mul + +theorem mul_lt_of_lt_div {a b c : Ordinal} : a < b / c → c * a < b := + lt_imp_lt_of_le_imp_le div_le_of_le_mul +#align ordinal.mul_lt_of_lt_div Ordinal.mul_lt_of_lt_div + +@[simp] +theorem zero_div (a : Ordinal) : 0 / a = 0 := + Ordinal.le_zero.1 <| div_le_of_le_mul <| Ordinal.zero_le _ +#align ordinal.zero_div Ordinal.zero_div + +theorem mul_div_le (a b : Ordinal) : b * (a / b) ≤ a := + if b0 : b = 0 then by simp only [b0, zero_mul, Ordinal.zero_le] else (le_div b0).1 le_rfl +#align ordinal.mul_div_le Ordinal.mul_div_le + +theorem mul_add_div (a) {b : Ordinal} (b0 : b ≠ 0) (c) : (b * a + c) / b = a + c / b := by + apply le_antisymm + · apply (div_le b0).2 + rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left] + apply lt_mul_div_add _ b0 + · rw [le_div b0, mul_add, add_le_add_iff_left] + apply mul_div_le +#align ordinal.mul_add_div Ordinal.mul_add_div + +theorem div_eq_zero_of_lt {a b : Ordinal} (h : a < b) : a / b = 0 := by + rw [← Ordinal.le_zero, div_le <| Ordinal.pos_iff_ne_zero.1 <| (Ordinal.zero_le _).trans_lt h] + simpa only [succ_zero, mul_one] using h +#align ordinal.div_eq_zero_of_lt Ordinal.div_eq_zero_of_lt + +@[simp] +theorem mul_div_cancel (a) {b : Ordinal} (b0 : b ≠ 0) : b * a / b = a := by + simpa only [add_zero, zero_div] using mul_add_div a b0 0 +#align ordinal.mul_div_cancel Ordinal.mul_div_cancel + +@[simp] +theorem div_one (a : Ordinal) : a / 1 = a := by + simpa only [one_mul] using mul_div_cancel a Ordinal.one_ne_zero +#align ordinal.div_one Ordinal.div_one + +@[simp] +theorem div_self {a : Ordinal} (h : a ≠ 0) : a / a = 1 := by + simpa only [mul_one] using mul_div_cancel 1 h +#align ordinal.div_self Ordinal.div_self + +theorem mul_sub (a b c : Ordinal) : a * (b - c) = a * b - a * c := + if a0 : a = 0 then by simp only [a0, zero_mul, sub_self] + else + eq_of_forall_ge_iff fun d => by rw [sub_le, ← le_div a0, sub_le, ← le_div a0, mul_add_div _ a0] +#align ordinal.mul_sub Ordinal.mul_sub + +theorem isLimit_add_iff {a b} : IsLimit (a + b) ↔ IsLimit b ∨ b = 0 ∧ IsLimit a := by + constructor <;> intro h + · by_cases h' : b = 0 + · rw [h', add_zero] at h + right + exact ⟨h', h⟩ + left + rw [← add_sub_cancel a b] + apply sub_isLimit h + suffices : a + 0 < a + b + simpa only [add_zero] using this + rwa [add_lt_add_iff_left, Ordinal.pos_iff_ne_zero] + rcases h with (h | ⟨rfl, h⟩); exact add_isLimit a h; simpa only [add_zero] +#align ordinal.is_limit_add_iff Ordinal.isLimit_add_iff + +theorem dvd_add_iff : ∀ {a b c : Ordinal}, a ∣ b → (a ∣ b + c ↔ a ∣ c) + | a, _, c, ⟨b, rfl⟩ => + ⟨fun ⟨d, e⟩ => ⟨d - b, by rw [mul_sub, ← e, add_sub_cancel]⟩, fun ⟨d, e⟩ => + by + rw [e, ← mul_add] + apply dvd_mul_right⟩ +#align ordinal.dvd_add_iff Ordinal.dvd_add_iff + +theorem div_mul_cancel : ∀ {a b : Ordinal}, a ≠ 0 → a ∣ b → a * (b / a) = b + | a, _, a0, ⟨b, rfl⟩ => by rw [mul_div_cancel _ a0] +#align ordinal.div_mul_cancel Ordinal.div_mul_cancel + +theorem le_of_dvd : ∀ {a b : Ordinal}, b ≠ 0 → a ∣ b → a ≤ b + -- Porting note: `⟨b, rfl⟩ => by` → `⟨b, e⟩ => by subst e` + | a, _, b0, ⟨b, e⟩ => by + subst e + -- Porting note: `Ne` is required. + simpa only [mul_one] using + mul_le_mul_left' + (one_le_iff_ne_zero.2 fun h : b = 0 => by simp only [h, mul_zero, Ne] at b0) a +#align ordinal.le_of_dvd Ordinal.le_of_dvd + +theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b := + if a0 : a = 0 then by subst a; exact (eq_zero_of_zero_dvd h₁).symm + else + if b0 : b = 0 then by subst b; exact eq_zero_of_zero_dvd h₂ + else (le_of_dvd b0 h₁).antisymm (le_of_dvd a0 h₂) +#align ordinal.dvd_antisymm Ordinal.dvd_antisymm + +instance : IsAntisymm Ordinal (· ∣ ·) := + ⟨@dvd_antisymm⟩ + +/-- `a % b` is the unique ordinal `o'` satisfying + `a = b * o + o'` with `o' < b`. -/ +instance : Mod Ordinal := + ⟨fun a b => a - b * (a / b)⟩ + +theorem mod_def (a b : Ordinal) : a % b = a - b * (a / b) := + rfl +#align ordinal.mod_def Ordinal.mod_def + +@[simp] +theorem mod_zero (a : Ordinal) : a % 0 = a := by simp only [mod_def, div_zero, zero_mul, sub_zero] +#align ordinal.mod_zero Ordinal.mod_zero + +theorem mod_eq_of_lt {a b : Ordinal} (h : a < b) : a % b = a := by + simp only [mod_def, div_eq_zero_of_lt h, mul_zero, sub_zero] +#align ordinal.mod_eq_of_lt Ordinal.mod_eq_of_lt + +@[simp] +theorem zero_mod (b : Ordinal) : 0 % b = 0 := by simp only [mod_def, zero_div, mul_zero, sub_self] +#align ordinal.zero_mod Ordinal.zero_mod + +theorem div_add_mod (a b : Ordinal) : b * (a / b) + a % b = a := + Ordinal.add_sub_cancel_of_le <| mul_div_le _ _ +#align ordinal.div_add_mod Ordinal.div_add_mod + +theorem mod_lt (a) {b : Ordinal} (h : b ≠ 0) : a % b < b := + (add_lt_add_iff_left (b * (a / b))).1 <| by rw [div_add_mod]; exact lt_mul_div_add a h +#align ordinal.mod_lt Ordinal.mod_lt + +@[simp] +theorem mod_self (a : Ordinal) : a % a = 0 := + if a0 : a = 0 then by simp only [a0, zero_mod] + else by simp only [mod_def, div_self a0, mul_one, sub_self] +#align ordinal.mod_self Ordinal.mod_self + +@[simp] +theorem mod_one (a : Ordinal) : a % 1 = 0 := by simp only [mod_def, div_one, one_mul, sub_self] +#align ordinal.mod_one Ordinal.mod_one + +theorem dvd_of_mod_eq_zero {a b : Ordinal} (H : a % b = 0) : b ∣ a := + ⟨a / b, by simpa [H] using (div_add_mod a b).symm⟩ +#align ordinal.dvd_of_mod_eq_zero Ordinal.dvd_of_mod_eq_zero + +theorem mod_eq_zero_of_dvd {a b : Ordinal} (H : b ∣ a) : a % b = 0 := by + rcases H with ⟨c, rfl⟩ + rcases eq_or_ne b 0 with (rfl | hb) + · simp + · simp [mod_def, hb] +#align ordinal.mod_eq_zero_of_dvd Ordinal.mod_eq_zero_of_dvd + +theorem dvd_iff_mod_eq_zero {a b : Ordinal} : b ∣ a ↔ a % b = 0 := + ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ +#align ordinal.dvd_iff_mod_eq_zero Ordinal.dvd_iff_mod_eq_zero + +/-! ### Families of ordinals + +There are two kinds of indexed families that naturally arise when dealing with ordinals: those +indexed by some type in the appropriate universe, and those indexed by ordinals less than another. +The following API allows one to convert from one kind of family to the other. + +In many cases, this makes it easy to prove claims about one kind of family via the corresponding +claim on the other. -/ + + +/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a specified +well-ordering. -/ +def bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : + ∀ a < type r, α := fun a ha => f (enum r a ha) +#align ordinal.bfamily_of_family' Ordinal.bfamilyOfFamily' + +/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a well-ordering +given by the axiom of choice. -/ +def bfamilyOfFamily {ι : Type u} : (ι → α) → ∀ a < type (@WellOrderingRel ι), α := + bfamilyOfFamily' WellOrderingRel +#align ordinal.bfamily_of_family Ordinal.bfamilyOfFamily + +/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by an `Type u` using a specified +well-ordering. -/ +def familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) + (f : ∀ a < o, α) : ι → α := fun i => + f (typein r i) + (by + rw [← ho] + exact typein_lt_type r i) +#align ordinal.family_of_bfamily' Ordinal.familyOfBFamily' + +/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by a `Type u` using a well-ordering +given by the axiom of choice. -/ +def familyOfBFamily (o : Ordinal) (f : ∀ a < o, α) : o.out.α → α := + familyOfBFamily' (· < ·) (type_lt o) f +#align ordinal.family_of_bfamily Ordinal.familyOfBFamily + +@[simp] +theorem bfamilyOfFamily'_typein {ι} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i) : + bfamilyOfFamily' r f (typein r i) (typein_lt_type r i) = f i := by + simp only [bfamilyOfFamily', enum_typein] +#align ordinal.bfamily_of_family'_typein Ordinal.bfamilyOfFamily'_typein + +@[simp] +theorem bfamilyOfFamily_typein {ι} (f : ι → α) (i) : + bfamilyOfFamily f (typein _ i) (typein_lt_type _ i) = f i := + bfamilyOfFamily'_typein _ f i +#align ordinal.bfamily_of_family_typein Ordinal.bfamilyOfFamily_typein + +@[simp, nolint simpNF] -- Porting note: simp cannot prove this +theorem familyOfBFamily'_enum {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} + (ho : type r = o) (f : ∀ a < o, α) (i hi) : + familyOfBFamily' r ho f (enum r i (by rwa [ho])) = f i hi := by + simp only [familyOfBFamily', typein_enum] +#align ordinal.family_of_bfamily'_enum Ordinal.familyOfBFamily'_enum + +@[simp, nolint simpNF] -- Porting note: simp cannot prove this +theorem familyOfBFamily_enum (o : Ordinal) (f : ∀ a < o, α) (i hi) : + familyOfBFamily o f + (enum (· < ·) i + (by + convert hi + exact type_lt _)) = + f i hi := + familyOfBFamily'_enum _ (type_lt o) f _ _ +#align ordinal.family_of_bfamily_enum Ordinal.familyOfBFamily_enum + +/-- The range of a family indexed by ordinals. -/ +def brange (o : Ordinal) (f : ∀ a < o, α) : Set α := + { a | ∃ i hi, f i hi = a } +#align ordinal.brange Ordinal.brange + +theorem mem_brange {o : Ordinal} {f : ∀ a < o, α} {a} : a ∈ brange o f ↔ ∃ i hi, f i hi = a := + Iff.rfl +#align ordinal.mem_brange Ordinal.mem_brange + +theorem mem_brange_self {o} (f : ∀ a < o, α) (i hi) : f i hi ∈ brange o f := + ⟨i, hi, rfl⟩ +#align ordinal.mem_brange_self Ordinal.mem_brange_self + +@[simp] +theorem range_familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} + (ho : type r = o) (f : ∀ a < o, α) : range (familyOfBFamily' r ho f) = brange o f := by + refine' Set.ext fun a => ⟨_, _⟩ + · rintro ⟨b, rfl⟩ + apply mem_brange_self + · rintro ⟨i, hi, rfl⟩ + exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩ +#align ordinal.range_family_of_bfamily' Ordinal.range_familyOfBFamily' + +@[simp] +theorem range_familyOfBFamily {o} (f : ∀ a < o, α) : range (familyOfBFamily o f) = brange o f := + range_familyOfBFamily' _ _ f +#align ordinal.range_family_of_bfamily Ordinal.range_familyOfBFamily + +@[simp] +theorem brange_bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : + brange _ (bfamilyOfFamily' r f) = range f := by + refine' Set.ext fun a => ⟨_, _⟩ + · rintro ⟨i, hi, rfl⟩ + apply mem_range_self + · rintro ⟨b, rfl⟩ + exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩ +#align ordinal.brange_bfamily_of_family' Ordinal.brange_bfamilyOfFamily' + +@[simp] +theorem brange_bfamilyOfFamily {ι : Type u} (f : ι → α) : brange _ (bfamilyOfFamily f) = range f := + brange_bfamilyOfFamily' _ _ +#align ordinal.brange_bfamily_of_family Ordinal.brange_bfamilyOfFamily + +@[simp] +theorem brange_const {o : Ordinal} (ho : o ≠ 0) {c : α} : (brange o fun _ _ => c) = {c} := by + rw [← range_familyOfBFamily] + exact @Set.range_const _ o.out.α (out_nonempty_iff_ne_zero.2 ho) c +#align ordinal.brange_const Ordinal.brange_const + +theorem comp_bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) + (g : α → β) : (fun i hi => g (bfamilyOfFamily' r f i hi)) = bfamilyOfFamily' r (g ∘ f) := + rfl +#align ordinal.comp_bfamily_of_family' Ordinal.comp_bfamilyOfFamily' + +theorem comp_bfamilyOfFamily {ι : Type u} (f : ι → α) (g : α → β) : + (fun i hi => g (bfamilyOfFamily f i hi)) = bfamilyOfFamily (g ∘ f) := + rfl +#align ordinal.comp_bfamily_of_family Ordinal.comp_bfamilyOfFamily + +theorem comp_familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} + (ho : type r = o) (f : ∀ a < o, α) (g : α → β) : + g ∘ familyOfBFamily' r ho f = familyOfBFamily' r ho fun i hi => g (f i hi) := + rfl +#align ordinal.comp_family_of_bfamily' Ordinal.comp_familyOfBFamily' + +theorem comp_familyOfBFamily {o} (f : ∀ a < o, α) (g : α → β) : + g ∘ familyOfBFamily o f = familyOfBFamily o fun i hi => g (f i hi) := + rfl +#align ordinal.comp_family_of_bfamily Ordinal.comp_familyOfBFamily + +/-! ### Supremum of a family of ordinals -/ + +-- Porting note: Universes should be specified in `sup`s. + +/-- The supremum of a family of ordinals -/ +def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} := + supᵢ f +#align ordinal.sup Ordinal.sup + +@[simp] +theorem supₛ_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : supₛ (Set.range f) = sup.{_, v} f := + rfl +#align ordinal.Sup_eq_sup Ordinal.supₛ_eq_sup + +/-- The range of an indexed ordinal function, whose outputs live in a higher universe than the + inputs, is always bounded above. See `Ordinal.lsub` for an explicit bound. -/ +theorem bddAbove_range {ι : Type u} (f : ι → Ordinal.{max u v}) : BddAbove (Set.range f) := + ⟨(supᵢ (succ ∘ card ∘ f)).ord, by + rintro a ⟨i, rfl⟩ + exact le_of_lt (Cardinal.lt_ord.2 ((lt_succ _).trans_le + (le_csupᵢ (Cardinal.bddAbove_range.{_, v} _) _)))⟩ +#align ordinal.bdd_above_range Ordinal.bddAbove_range + +theorem le_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : ∀ i, f i ≤ sup.{_, v} f := fun i => + le_csupₛ (bddAbove_range.{_, v} f) (mem_range_self i) +#align ordinal.le_sup Ordinal.le_sup + +theorem sup_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : sup.{_, v} f ≤ a ↔ ∀ i, f i ≤ a := + (csupₛ_le_iff' (bddAbove_range.{_, v} f)).trans (by simp) +#align ordinal.sup_le_iff Ordinal.sup_le_iff + +theorem sup_le {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : (∀ i, f i ≤ a) → sup.{_, v} f ≤ a := + sup_le_iff.2 +#align ordinal.sup_le Ordinal.sup_le + +theorem lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : a < sup.{_, v} f ↔ ∃ i, a < f i := by + simpa only [not_forall, not_le] using not_congr (@sup_le_iff.{_, v} _ f a) +#align ordinal.lt_sup Ordinal.lt_sup + +theorem ne_sup_iff_lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} : + (∀ i, f i ≠ sup.{_, v} f) ↔ ∀ i, f i < sup.{_, v} f := + ⟨fun hf _ => lt_of_le_of_ne (le_sup _ _) (hf _), fun hf _ => ne_of_lt (hf _)⟩ +#align ordinal.ne_sup_iff_lt_sup Ordinal.ne_sup_iff_lt_sup + +theorem sup_not_succ_of_ne_sup {ι : Type u} {f : ι → Ordinal.{max u v}} + (hf : ∀ i, f i ≠ sup.{_, v} f) {a} (hao : a < sup.{_, v} f) : succ a < sup.{_, v} f := by + by_contra' hoa + exact + hao.not_le (sup_le fun i => le_of_lt_succ <| (lt_of_le_of_ne (le_sup _ _) (hf i)).trans_le hoa) +#align ordinal.sup_not_succ_of_ne_sup Ordinal.sup_not_succ_of_ne_sup + +@[simp] +theorem sup_eq_zero_iff {ι : Type u} {f : ι → Ordinal.{max u v}} : + sup.{_, v} f = 0 ↔ ∀ i, f i = 0 := by + refine' + ⟨fun h i => _, fun h => + le_antisymm (sup_le fun i => Ordinal.le_zero.2 (h i)) (Ordinal.zero_le _)⟩ + rw [← Ordinal.le_zero, ← h] + exact le_sup f i +#align ordinal.sup_eq_zero_iff Ordinal.sup_eq_zero_iff + +theorem IsNormal.sup {f : Ordinal.{max u v} → Ordinal.{max u w}} (H : IsNormal f) {ι : Type u} + (g : ι → Ordinal.{max u v}) [Nonempty ι] : f (sup.{_, v} g) = sup.{_, w} (f ∘ g) := + eq_of_forall_ge_iff fun a => by + rw [sup_le_iff]; simp only [comp]; rw [H.le_set' Set.univ Set.univ_nonempty g] <;> + simp [sup_le_iff] +#align ordinal.is_normal.sup Ordinal.IsNormal.sup + +@[simp] +theorem sup_empty {ι} [IsEmpty ι] (f : ι → Ordinal) : sup f = 0 := + csupᵢ_of_empty f +#align ordinal.sup_empty Ordinal.sup_empty + +@[simp] +theorem sup_const {ι} [_hι : Nonempty ι] (o : Ordinal) : (sup fun _ : ι => o) = o := + csupᵢ_const +#align ordinal.sup_const Ordinal.sup_const + +@[simp] +theorem sup_unique {ι} [Unique ι] (f : ι → Ordinal) : sup f = f default := + csupᵢ_unique +#align ordinal.sup_unique Ordinal.sup_unique + +theorem sup_le_of_range_subset {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} + (h : Set.range f ⊆ Set.range g) : sup.{u, max v w} f ≤ sup.{v, max u w} g := + sup_le fun i => + match h (mem_range_self i) with + | ⟨_j, hj⟩ => hj ▸ le_sup _ _ +#align ordinal.sup_le_of_range_subset Ordinal.sup_le_of_range_subset + +theorem sup_eq_of_range_eq {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} + (h : Set.range f = Set.range g) : sup.{u, max v w} f = sup.{v, max u w} g := + (sup_le_of_range_subset.{u, v, w} h.le).antisymm (sup_le_of_range_subset.{v, u, w} h.ge) +#align ordinal.sup_eq_of_range_eq Ordinal.sup_eq_of_range_eq + +@[simp] +theorem sup_sum {α : Type u} {β : Type v} (f : Sum α β → Ordinal) : + sup.{max u v, w} f = + max (sup.{u, max v w} fun a => f (Sum.inl a)) (sup.{v, max u w} fun b => f (Sum.inr b)) := by + apply (sup_le_iff.2 _).antisymm (max_le_iff.2 ⟨_, _⟩) + · rintro (i | i) + · exact le_max_of_le_left (le_sup _ i) + · exact le_max_of_le_right (le_sup _ i) + all_goals + apply sup_le_of_range_subset.{_, max u v, w} + rintro i ⟨a, rfl⟩ + apply mem_range_self +#align ordinal.sup_sum Ordinal.sup_sum + +theorem unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) + (h : type r ≤ sup.{u, u} (typein r ∘ f)) : Unbounded r (range f) := + (not_bounded_iff _).1 fun ⟨x, hx⟩ => + not_lt_of_le h <| + lt_of_le_of_lt + (sup_le fun y => le_of_lt <| (typein_lt_typein r).2 <| hx _ <| mem_range_self y) + (typein_lt_type r x) +#align ordinal.unbounded_range_of_sup_ge Ordinal.unbounded_range_of_sup_ge + +theorem le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u} s) (a) (ha : a ∈ s) : + a ≤ sup.{u, u} fun x => ((@equivShrink s hs).symm x).val := by + convert le_sup.{u, u} (fun x => ((@equivShrink s hs).symm x).val) ((@equivShrink s hs) ⟨a, ha⟩) + rw [symm_apply_apply] +#align ordinal.le_sup_shrink_equiv Ordinal.le_sup_shrink_equiv + +instance small_Iio (o : Ordinal.{u}) : Small.{u} (Set.Iio o) := + let f : o.out.α → Set.Iio o := + fun x => ⟨typein ((· < ·) : o.out.α → o.out.α → Prop) x, typein_lt_self x⟩ + let hf : Surjective f := fun b => + ⟨enum (· < ·) b.val + (by + rw [type_lt] + exact b.prop), + Subtype.ext (typein_enum _ _)⟩ + small_of_surjective hf +#align ordinal.small_Iio Ordinal.small_Iio + +instance small_Iic (o : Ordinal.{u}) : Small.{u} (Set.Iic o) := by + rw [← Iio_succ] + infer_instance +#align ordinal.small_Iic Ordinal.small_Iic + +theorem bddAbove_iff_small {s : Set Ordinal.{u}} : BddAbove s ↔ Small.{u} s := + ⟨fun ⟨a, h⟩ => small_subset <| show s ⊆ Iic a from fun _x hx => h hx, fun h => + ⟨sup.{u, u} fun x => ((@equivShrink s h).symm x).val, le_sup_shrink_equiv h⟩⟩ +#align ordinal.bdd_above_iff_small Ordinal.bddAbove_iff_small + +theorem bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u} s] : BddAbove s := + bddAbove_iff_small.2 h +#align ordinal.bdd_above_of_small Ordinal.bddAbove_of_small + +theorem sup_eq_supₛ {s : Set Ordinal.{u}} (hs : Small.{u} s) : + (sup.{u, u} fun x => (@equivShrink s hs).symm x) = supₛ s := + let hs' := bddAbove_iff_small.2 hs + ((csupₛ_le_iff' hs').2 (le_sup_shrink_equiv hs)).antisymm' + (sup_le fun _x => le_csupₛ hs' (Subtype.mem _)) +#align ordinal.sup_eq_Sup Ordinal.sup_eq_supₛ + +theorem supₛ_ord {s : Set Cardinal.{u}} (hs : BddAbove s) : (supₛ s).ord = supₛ (ord '' s) := + eq_of_forall_ge_iff fun a => by + rw [csupₛ_le_iff' + (bddAbove_iff_small.2 (@small_image _ _ _ s (Cardinal.bddAbove_iff_small.1 hs))), + ord_le, csupₛ_le_iff' hs] + simp [ord_le] +#align ordinal.Sup_ord Ordinal.supₛ_ord + +theorem supᵢ_ord {ι} {f : ι → Cardinal} (hf : BddAbove (range f)) : + (supᵢ f).ord = ⨆ i, (f i).ord := by + unfold supᵢ + convert supₛ_ord hf + -- Porting note: `change` is required. + conv_lhs => change range (ord ∘ f) + rw [range_comp] +#align ordinal.supr_ord Ordinal.supᵢ_ord + +private theorem sup_le_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) + [IsWellOrder ι r] [IsWellOrder ι' r'] {o} (ho : type r = o) (ho' : type r' = o) + (f : ∀ a < o, Ordinal.{max u v}) : + sup.{_, v} (familyOfBFamily' r ho f) ≤ sup.{_, v} (familyOfBFamily' r' ho' f) := + sup_le fun i => by + cases' + typein_surj r' + (by + rw [ho', ← ho] + exact typein_lt_type r i) with + j hj + simp_rw [familyOfBFamily', ← hj] + apply le_sup + +theorem sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] + [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) + (f : ∀ a < o, Ordinal.{max u v}) : + sup.{_, v} (familyOfBFamily' r ho f) = sup.{_, v} (familyOfBFamily' r' ho' f) := + sup_eq_of_range_eq.{u, u, v} (by simp) +#align ordinal.sup_eq_sup Ordinal.sup_eq_sup + +/-- The supremum of a family of ordinals indexed by the set of ordinals less than some + `o : Ordinal.{u}`. This is a special case of `sup` over the family provided by + `familyOfBFamily`. -/ +def bsup (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) : Ordinal.{max u v} := + sup.{_, v} (familyOfBFamily o f) +#align ordinal.bsup Ordinal.bsup + +@[simp] +theorem sup_eq_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + sup.{_, v} (familyOfBFamily o f) = bsup.{_, v} o f := + rfl +#align ordinal.sup_eq_bsup Ordinal.sup_eq_bsup + +@[simp] +theorem sup_eq_bsup' {o : Ordinal.{u}} {ι} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) + (f : ∀ a < o, Ordinal.{max u v}) : sup.{_, v} (familyOfBFamily' r ho f) = bsup.{_, v} o f := + sup_eq_sup r _ ho _ f +#align ordinal.sup_eq_bsup' Ordinal.sup_eq_bsup' + +@[simp, nolint simpNF] -- Porting note: simp cannot prove this +theorem supₛ_eq_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + supₛ (brange o f) = bsup.{_, v} o f := by + congr + rw [range_familyOfBFamily] +#align ordinal.Sup_eq_bsup Ordinal.supₛ_eq_bsup + +@[simp] +theorem bsup_eq_sup' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) : + bsup.{_, v} _ (bfamilyOfFamily' r f) = sup.{_, v} f := by + simp only [← sup_eq_bsup' r, enum_typein, familyOfBFamily', bfamilyOfFamily'] +#align ordinal.bsup_eq_sup' Ordinal.bsup_eq_sup' + +theorem bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] + (f : ι → Ordinal.{max u v}) : + bsup.{_, v} _ (bfamilyOfFamily' r f) = bsup.{_, v} _ (bfamilyOfFamily' r' f) := by + rw [bsup_eq_sup', bsup_eq_sup'] +#align ordinal.bsup_eq_bsup Ordinal.bsup_eq_bsup + +@[simp] +theorem bsup_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : + bsup.{_, v} _ (bfamilyOfFamily f) = sup.{_, v} f := + bsup_eq_sup' _ f +#align ordinal.bsup_eq_sup Ordinal.bsup_eq_sup + +@[congr] +theorem bsup_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) : + bsup.{_, v} o₁ f = bsup.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm) := by + subst ho + -- Porting note: `congr` is required. + congr +#align ordinal.bsup_congr Ordinal.bsup_congr + +theorem bsup_le_iff {o f a} : bsup.{u, v} o f ≤ a ↔ ∀ i h, f i h ≤ a := + sup_le_iff.trans + ⟨fun h i hi => by + rw [← familyOfBFamily_enum o f] + exact h _, fun h i => h _ _⟩ +#align ordinal.bsup_le_iff Ordinal.bsup_le_iff + +theorem bsup_le {o : Ordinal} {f : ∀ b < o, Ordinal} {a} : + (∀ i h, f i h ≤ a) → bsup.{u, v} o f ≤ a := + bsup_le_iff.2 +#align ordinal.bsup_le Ordinal.bsup_le + +theorem le_bsup {o} (f : ∀ a < o, Ordinal) (i h) : f i h ≤ bsup o f := + bsup_le_iff.1 le_rfl _ _ +#align ordinal.le_bsup Ordinal.le_bsup + +theorem lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {a} : + a < bsup.{_, v} o f ↔ ∃ i hi, a < f i hi := by + simpa only [not_forall, not_le] using not_congr (@bsup_le_iff.{_, v} _ f a) +#align ordinal.lt_bsup Ordinal.lt_bsup + +theorem IsNormal.bsup {f : Ordinal.{max u v} → Ordinal.{max u w}} (H : IsNormal f) + {o : Ordinal.{u}} : + ∀ (g : ∀ a < o, Ordinal), o ≠ 0 → f (bsup.{_, v} o g) = bsup.{_, w} o fun a h => f (g a h) := + inductionOn o fun α r _ g h => by + haveI := type_ne_zero_iff_nonempty.1 h + rw [← sup_eq_bsup' r, IsNormal.sup.{_, v, w} H, ← sup_eq_bsup' r] <;> rfl +#align ordinal.is_normal.bsup Ordinal.IsNormal.bsup + +theorem lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} : + (∀ i h, f i h ≠ bsup.{_, v} o f) ↔ ∀ i h, f i h < bsup.{_, v} o f := + ⟨fun hf _ _ => lt_of_le_of_ne (le_bsup _ _ _) (hf _ _), fun hf _ _ => ne_of_lt (hf _ _)⟩ +#align ordinal.lt_bsup_of_ne_bsup Ordinal.lt_bsup_of_ne_bsup + +theorem bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} + (hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ bsup.{_, v} o f) (a) : + a < bsup.{_, v} o f → succ a < bsup.{_, v} o f := by + rw [← sup_eq_bsup] at * + exact sup_not_succ_of_ne_sup fun i => hf _ +#align ordinal.bsup_not_succ_of_ne_bsup Ordinal.bsup_not_succ_of_ne_bsup + +@[simp] +theorem bsup_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : bsup o f = 0 ↔ ∀ i hi, f i hi = 0 := by + refine' + ⟨fun h i hi => _, fun h => + le_antisymm (bsup_le fun i hi => Ordinal.le_zero.2 (h i hi)) (Ordinal.zero_le _)⟩ + rw [← Ordinal.le_zero, ← h] + exact le_bsup f i hi +#align ordinal.bsup_eq_zero_iff Ordinal.bsup_eq_zero_iff + +theorem lt_bsup_of_limit {o : Ordinal} {f : ∀ a < o, Ordinal} + (hf : ∀ {a a'} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') + (ho : ∀ a < o, succ a < o) (i h) : f i h < bsup o f := + (hf _ _ <| lt_succ i).trans_le (le_bsup f (succ i) <| ho _ h) +#align ordinal.lt_bsup_of_limit Ordinal.lt_bsup_of_limit + +theorem bsup_succ_of_mono {o : Ordinal} {f : ∀ a < succ o, Ordinal} + (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) : bsup _ f = f o (lt_succ o) := + le_antisymm (bsup_le fun _i hi => hf _ _ <| le_of_lt_succ hi) (le_bsup _ _ _) +#align ordinal.bsup_succ_of_mono Ordinal.bsup_succ_of_mono + +@[simp] +theorem bsup_zero (f : ∀ a < (0 : Ordinal), Ordinal) : bsup 0 f = 0 := + bsup_eq_zero_iff.2 fun i hi => (Ordinal.not_lt_zero i hi).elim +#align ordinal.bsup_zero Ordinal.bsup_zero + +theorem bsup_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) : + (bsup.{_, v} o fun _ _ => a) = a := + le_antisymm (bsup_le fun _ _ => le_rfl) (le_bsup _ 0 (Ordinal.pos_iff_ne_zero.2 ho)) +#align ordinal.bsup_const Ordinal.bsup_const + +@[simp] +theorem bsup_one (f : ∀ a < (1 : Ordinal), Ordinal) : bsup 1 f = f 0 zero_lt_one := by + simp_rw [← sup_eq_bsup, sup_unique, familyOfBFamily, familyOfBFamily', typein_one_out] +#align ordinal.bsup_one Ordinal.bsup_one + +theorem bsup_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} + (h : brange o f ⊆ brange o' g) : bsup.{u, max v w} o f ≤ bsup.{v, max u w} o' g := + bsup_le fun i hi => by + obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩ + rw [← hj'] + apply le_bsup +#align ordinal.bsup_le_of_brange_subset Ordinal.bsup_le_of_brange_subset + +theorem bsup_eq_of_brange_eq {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} + (h : brange o f = brange o' g) : bsup.{u, max v w} o f = bsup.{v, max u w} o' g := + (bsup_le_of_brange_subset.{u, v, w} h.le).antisymm (bsup_le_of_brange_subset.{v, u, w} h.ge) +#align ordinal.bsup_eq_of_brange_eq Ordinal.bsup_eq_of_brange_eq + +/-- The least strict upper bound of a family of ordinals. -/ +def lsub {ι} (f : ι → Ordinal) : Ordinal := + sup (succ ∘ f) +#align ordinal.lsub Ordinal.lsub + +@[simp] +theorem sup_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : + sup.{_, v} (succ ∘ f) = lsub.{_, v} f := + rfl +#align ordinal.sup_eq_lsub Ordinal.sup_eq_lsub + +theorem lsub_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : + lsub.{_, v} f ≤ a ↔ ∀ i, f i < a := by + convert sup_le_iff.{_, v} (f := succ ∘ f) (a := a) + -- Porting note: `eq_iff_iff` & `(· ∘ ·)` are required. + simp only [eq_iff_iff, (· ∘ ·), succ_le_iff] +#align ordinal.lsub_le_iff Ordinal.lsub_le_iff + +theorem lsub_le {ι} {f : ι → Ordinal} {a} : (∀ i, f i < a) → lsub f ≤ a := + lsub_le_iff.2 +#align ordinal.lsub_le Ordinal.lsub_le + +theorem lt_lsub {ι} (f : ι → Ordinal) (i) : f i < lsub f := + succ_le_iff.1 (le_sup _ i) +#align ordinal.lt_lsub Ordinal.lt_lsub + +theorem lt_lsub_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : + a < lsub.{_, v} f ↔ ∃ i, a ≤ f i := by + simpa only [not_forall, not_lt, not_le] using not_congr (@lsub_le_iff.{_, v} _ f a) +#align ordinal.lt_lsub_iff Ordinal.lt_lsub_iff + +theorem sup_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : sup.{_, v} f ≤ lsub.{_, v} f := + sup_le fun i => (lt_lsub f i).le +#align ordinal.sup_le_lsub Ordinal.sup_le_lsub + +theorem lsub_le_sup_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : + lsub.{_, v} f ≤ succ (sup.{_, v} f) := + lsub_le fun i => lt_succ_iff.2 (le_sup f i) +#align ordinal.lsub_le_sup_succ Ordinal.lsub_le_sup_succ + +theorem sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : + sup.{_, v} f = lsub.{_, v} f ∨ succ (sup.{_, v} f) = lsub.{_, v} f := by + cases' eq_or_lt_of_le (sup_le_lsub.{_, v} f) with h h + · exact Or.inl h + · exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_sup_succ f)) +#align ordinal.sup_eq_lsub_or_sup_succ_eq_lsub Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub + +theorem sup_succ_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : + succ (sup.{_, v} f) ≤ lsub.{_, v} f ↔ ∃ i, f i = sup.{_, v} f := by + refine' ⟨fun h => _, _⟩ + · by_contra' hf + exact (succ_le_iff.1 h).ne ((sup_le_lsub f).antisymm (lsub_le (ne_sup_iff_lt_sup.1 hf))) + rintro ⟨_, hf⟩ + rw [succ_le_iff, ← hf] + exact lt_lsub _ _ +#align ordinal.sup_succ_le_lsub Ordinal.sup_succ_le_lsub + +theorem sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : + succ (sup.{_, v} f) = lsub.{_, v} f ↔ ∃ i, f i = sup.{_, v} f := + (lsub_le_sup_succ f).le_iff_eq.symm.trans (sup_succ_le_lsub f) +#align ordinal.sup_succ_eq_lsub Ordinal.sup_succ_eq_lsub + +theorem sup_eq_lsub_iff_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : + sup.{_, v} f = lsub.{_, v} f ↔ ∀ a < lsub.{_, v} f, succ a < lsub.{_, v} f := by + refine' ⟨fun h => _, fun hf => le_antisymm (sup_le_lsub f) (lsub_le fun i => _)⟩ + · rw [← h] + exact fun a => sup_not_succ_of_ne_sup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne + by_contra' hle + have heq := (sup_succ_eq_lsub f).2 ⟨i, le_antisymm (le_sup _ _) hle⟩ + have := + hf _ + (by + rw [← heq] + exact lt_succ (sup f)) + rw [heq] at this + exact this.false +#align ordinal.sup_eq_lsub_iff_succ Ordinal.sup_eq_lsub_iff_succ + +theorem sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : + sup.{_, v} f = lsub.{_, v} f ↔ ∀ i, f i < sup.{_, v} f := + ⟨fun h i => by + rw [h] + apply lt_lsub, fun h => le_antisymm (sup_le_lsub f) (lsub_le h)⟩ +#align ordinal.sup_eq_lsub_iff_lt_sup Ordinal.sup_eq_lsub_iff_lt_sup + +@[simp] +theorem lsub_empty {ι} [h : IsEmpty ι] (f : ι → Ordinal) : lsub f = 0 := by + rw [← Ordinal.le_zero, lsub_le_iff] + exact h.elim +#align ordinal.lsub_empty Ordinal.lsub_empty + +theorem lsub_pos {ι : Type u} [h : Nonempty ι] (f : ι → Ordinal.{max u v}) : 0 < lsub.{_, v} f := + h.elim fun i => (Ordinal.zero_le _).trans_lt (lt_lsub f i) +#align ordinal.lsub_pos Ordinal.lsub_pos + +@[simp] +theorem lsub_eq_zero_iff {ι : Type u} (f : ι → Ordinal.{max u v}) : + lsub.{_, v} f = 0 ↔ IsEmpty ι := by + refine' ⟨fun h => ⟨fun i => _⟩, fun h => @lsub_empty _ h _⟩ + have := @lsub_pos.{_, v} _ ⟨i⟩ f + rw [h] at this + exact this.false +#align ordinal.lsub_eq_zero_iff Ordinal.lsub_eq_zero_iff + +@[simp] +theorem lsub_const {ι} [Nonempty ι] (o : Ordinal) : (lsub fun _ : ι => o) = succ o := + sup_const (succ o) +#align ordinal.lsub_const Ordinal.lsub_const + +@[simp] +theorem lsub_unique {ι} [Unique ι] (f : ι → Ordinal) : lsub f = succ (f default) := + sup_unique _ +#align ordinal.lsub_unique Ordinal.lsub_unique + +theorem lsub_le_of_range_subset {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} + (h : Set.range f ⊆ Set.range g) : lsub.{u, max v w} f ≤ lsub.{v, max u w} g := + sup_le_of_range_subset.{u, v, w} (by convert Set.image_subset succ h <;> apply Set.range_comp) +#align ordinal.lsub_le_of_range_subset Ordinal.lsub_le_of_range_subset + +theorem lsub_eq_of_range_eq {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} + (h : Set.range f = Set.range g) : lsub.{u, max v w} f = lsub.{v, max u w} g := + (lsub_le_of_range_subset.{u, v, w} h.le).antisymm (lsub_le_of_range_subset.{v, u, w} h.ge) +#align ordinal.lsub_eq_of_range_eq Ordinal.lsub_eq_of_range_eq + +@[simp] +theorem lsub_sum {α : Type u} {β : Type v} (f : Sum α β → Ordinal) : + lsub.{max u v, w} f = + max (lsub.{u, max v w} fun a => f (Sum.inl a)) (lsub.{v, max u w} fun b => f (Sum.inr b)) := + sup_sum _ +#align ordinal.lsub_sum Ordinal.lsub_sum + +theorem lsub_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : + lsub.{_, v} f ∉ Set.range f := fun ⟨i, h⟩ => + h.not_lt (lt_lsub f i) +#align ordinal.lsub_not_mem_range Ordinal.lsub_not_mem_range + +theorem nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v}) : Set.range fᶜ.Nonempty := + ⟨_, lsub_not_mem_range.{_, v} f⟩ +#align ordinal.nonempty_compl_range Ordinal.nonempty_compl_range + +@[simp] +theorem lsub_typein (o : Ordinal) : lsub.{u, u} (typein ((· < ·) : o.out.α → o.out.α → Prop)) = o := + (lsub_le.{u, u} typein_lt_self).antisymm + (by + by_contra' h + -- Porting note: `nth_rw` → `conv_rhs` & `rw` + conv_rhs at h => rw [← type_lt o] + simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) _ h)) +#align ordinal.lsub_typein Ordinal.lsub_typein + +theorem sup_typein_limit {o : Ordinal} (ho : ∀ a, a < o → succ a < o) : + sup.{u, u} (typein ((· < ·) : o.out.α → o.out.α → Prop)) = o := by + -- Portinh note: `rwa` → `rw` & `assumption` + rw [(sup_eq_lsub_iff_succ.{u, u} (typein (· < ·))).2] <;> rw [lsub_typein o]; assumption +#align ordinal.sup_typein_limit Ordinal.sup_typein_limit + +@[simp] +theorem sup_typein_succ {o : Ordinal} : + sup.{u, u} (typein ((· < ·) : (succ o).out.α → (succ o).out.α → Prop)) = o := by + cases' + sup_eq_lsub_or_sup_succ_eq_lsub.{u, u} + (typein ((· < ·) : (succ o).out.α → (succ o).out.α → Prop)) with + h h + · rw [sup_eq_lsub_iff_succ] at h + simp only [lsub_typein] at h + exact (h o (lt_succ o)).false.elim + rw [← succ_eq_succ_iff, h] + apply lsub_typein +#align ordinal.sup_typein_succ Ordinal.sup_typein_succ + +/-- The least strict upper bound of a family of ordinals indexed by the set of ordinals less than + some `o : Ordinal.{u}`. + + This is to `lsub` as `bsup` is to `sup`. -/ +def blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) : Ordinal.{max u v} := + bsup.{_, v} o fun a ha => succ (f a ha) +#align ordinal.blsub Ordinal.blsub + +@[simp] +theorem bsup_eq_blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) : + (bsup.{_, v} o fun a ha => succ (f a ha)) = blsub.{_, v} o f := + rfl +#align ordinal.bsup_eq_blsub Ordinal.bsup_eq_blsub + +theorem lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) + (f : ∀ a < o, Ordinal.{max u v}) : lsub.{_, v} (familyOfBFamily' r ho f) = blsub.{_, v} o f := + sup_eq_bsup'.{_, v} r ho fun a ha => succ (f a ha) +#align ordinal.lsub_eq_blsub' Ordinal.lsub_eq_blsub' + +theorem lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] + [IsWellOrder ι' r'] {o} (ho : type r = o) (ho' : type r' = o) + (f : ∀ a < o, Ordinal.{max u v}) : + lsub.{_, v} (familyOfBFamily' r ho f) = lsub.{_, v} (familyOfBFamily' r' ho' f) := by + rw [lsub_eq_blsub', lsub_eq_blsub'] +#align ordinal.lsub_eq_lsub Ordinal.lsub_eq_lsub + +@[simp] +theorem lsub_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + lsub.{_, v} (familyOfBFamily o f) = blsub.{_, v} o f := + lsub_eq_blsub' _ _ _ +#align ordinal.lsub_eq_blsub Ordinal.lsub_eq_blsub + +@[simp] +theorem blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] + (f : ι → Ordinal.{max u v}) : blsub.{_, v} _ (bfamilyOfFamily' r f) = lsub.{_, v} f := + bsup_eq_sup'.{_, v} r (succ ∘ f) +#align ordinal.blsub_eq_lsub' Ordinal.blsub_eq_lsub' + +theorem blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] + (f : ι → Ordinal.{max u v}) : + blsub.{_, v} _ (bfamilyOfFamily' r f) = blsub.{_, v} _ (bfamilyOfFamily' r' f) := by + rw [blsub_eq_lsub', blsub_eq_lsub'] +#align ordinal.blsub_eq_blsub Ordinal.blsub_eq_blsub + +@[simp] +theorem blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : + blsub.{_, v} _ (bfamilyOfFamily f) = lsub.{_, v} f := + blsub_eq_lsub' _ _ +#align ordinal.blsub_eq_lsub Ordinal.blsub_eq_lsub + +@[congr] +theorem blsub_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) : + blsub.{_, v} o₁ f = blsub.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm) := by + subst ho + -- Porting note: `congr` is required. + congr +#align ordinal.blsub_congr Ordinal.blsub_congr + +theorem blsub_le_iff {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} {a} : + blsub.{_, v} o f ≤ a ↔ ∀ i h, f i h < a := by + convert bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) + simp [succ_le_iff] +#align ordinal.blsub_le_iff Ordinal.blsub_le_iff + +theorem blsub_le {o : Ordinal} {f : ∀ b < o, Ordinal} {a} : (∀ i h, f i h < a) → blsub o f ≤ a := + blsub_le_iff.2 +#align ordinal.blsub_le Ordinal.blsub_le + +theorem lt_blsub {o} (f : ∀ a < o, Ordinal) (i h) : f i h < blsub o f := + blsub_le_iff.1 le_rfl _ _ +#align ordinal.lt_blsub Ordinal.lt_blsub + +theorem lt_blsub_iff {o : Ordinal.{u}} {f : ∀ b < o, Ordinal.{max u v}} {a} : + a < blsub.{_, v} o f ↔ ∃ i hi, a ≤ f i hi := by + simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a) +#align ordinal.lt_blsub_iff Ordinal.lt_blsub_iff + +theorem bsup_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + bsup.{_, v} o f ≤ blsub.{_, v} o f := + bsup_le fun i h => (lt_blsub f i h).le +#align ordinal.bsup_le_blsub Ordinal.bsup_le_blsub + +theorem blsub_le_bsup_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + blsub.{_, v} o f ≤ succ (bsup.{_, v} o f) := + blsub_le fun i h => lt_succ_iff.2 (le_bsup f i h) +#align ordinal.blsub_le_bsup_succ Ordinal.blsub_le_bsup_succ + +theorem bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + bsup.{_, v} o f = blsub.{_, v} o f ∨ succ (bsup.{_, v} o f) = blsub.{_, v} o f := by + rw [← sup_eq_bsup, ← lsub_eq_blsub] + exact sup_eq_lsub_or_sup_succ_eq_lsub _ +#align ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub + +theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + succ (bsup.{_, v} o f) ≤ blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f := by + refine' ⟨fun h => _, _⟩ + · by_contra' hf + exact + ne_of_lt (succ_le_iff.1 h) + (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf))) + rintro ⟨_, _, hf⟩ + rw [succ_le_iff, ← hf] + exact lt_blsub _ _ _ +#align ordinal.bsup_succ_le_blsub Ordinal.bsup_succ_le_blsub + +theorem bsup_succ_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + succ (bsup.{_, v} o f) = blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f := + (blsub_le_bsup_succ f).le_iff_eq.symm.trans (bsup_succ_le_blsub f) +#align ordinal.bsup_succ_eq_blsub Ordinal.bsup_succ_eq_blsub + +theorem bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ a < blsub.{_, v} o f, succ a < blsub.{_, v} o f := by + rw [← sup_eq_bsup, ← lsub_eq_blsub] + apply sup_eq_lsub_iff_succ +#align ordinal.bsup_eq_blsub_iff_succ Ordinal.bsup_eq_blsub_iff_succ + +theorem bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ i hi, f i hi < bsup.{_, v} o f := + ⟨fun h i => by + rw [h] + apply lt_blsub, fun h => le_antisymm (bsup_le_blsub f) (blsub_le h)⟩ +#align ordinal.bsup_eq_blsub_iff_lt_bsup Ordinal.bsup_eq_blsub_iff_lt_bsup + +theorem bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : IsLimit o) + {f : ∀ a < o, Ordinal.{max u v}} (hf : ∀ a ha, f a ha < f (succ a) (ho.2 a ha)) : + bsup.{_, v} o f = blsub.{_, v} o f := by + rw [bsup_eq_blsub_iff_lt_bsup] + exact fun i hi => (hf i hi).trans_le (le_bsup f _ _) +#align ordinal.bsup_eq_blsub_of_lt_succ_limit Ordinal.bsup_eq_blsub_of_lt_succ_limit + +theorem blsub_succ_of_mono {o : Ordinal.{u}} {f : ∀ a < succ o, Ordinal.{max u v}} + (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) : blsub.{_, v} _ f = succ (f o (lt_succ o)) := + bsup_succ_of_mono fun {_ _} hi hj h => succ_le_succ (hf hi hj h) +#align ordinal.blsub_succ_of_mono Ordinal.blsub_succ_of_mono + +@[simp] +theorem blsub_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : blsub o f = 0 ↔ o = 0 := by + rw [← lsub_eq_blsub, lsub_eq_zero_iff] + exact out_empty_iff_eq_zero +#align ordinal.blsub_eq_zero_iff Ordinal.blsub_eq_zero_iff + +-- Porting note: `rwa` → `rw` +@[simp] +theorem blsub_zero (f : ∀ a < (0 : Ordinal), Ordinal) : blsub 0 f = 0 := by rw [blsub_eq_zero_iff] +#align ordinal.blsub_zero Ordinal.blsub_zero + +theorem blsub_pos {o : Ordinal} (ho : 0 < o) (f : ∀ a < o, Ordinal) : 0 < blsub o f := + (Ordinal.zero_le _).trans_lt (lt_blsub f 0 ho) +#align ordinal.blsub_pos Ordinal.blsub_pos + +theorem blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] + (f : ∀ a < type r, Ordinal.{max u v}) : + blsub.{_, v} (type r) f = lsub.{_, v} fun a => f (typein r a) (typein_lt_type _ _) := + eq_of_forall_ge_iff fun o => by + rw [blsub_le_iff, lsub_le_iff]; + exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r i h)⟩ +#align ordinal.blsub_type Ordinal.blsub_type + +theorem blsub_const {o : Ordinal} (ho : o ≠ 0) (a : Ordinal) : + (blsub.{u, v} o fun _ _ => a) = succ a := + bsup_const.{u, v} ho (succ a) +#align ordinal.blsub_const Ordinal.blsub_const + +@[simp] +theorem blsub_one (f : ∀ a < (1 : Ordinal), Ordinal) : blsub 1 f = succ (f 0 zero_lt_one) := + bsup_one _ +#align ordinal.blsub_one Ordinal.blsub_one + +@[simp] +theorem blsub_id : ∀ o, (blsub.{u, u} o fun x _ => x) = o := + lsub_typein +#align ordinal.blsub_id Ordinal.blsub_id + +theorem bsup_id_limit {o : Ordinal} : (∀ a < o, succ a < o) → (bsup.{u, u} o fun x _ => x) = o := + sup_typein_limit +#align ordinal.bsup_id_limit Ordinal.bsup_id_limit + +@[simp] +theorem bsup_id_succ (o) : (bsup.{u, u} (succ o) fun x _ => x) = o := + sup_typein_succ +#align ordinal.bsup_id_succ Ordinal.bsup_id_succ + +theorem blsub_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} + (h : brange o f ⊆ brange o' g) : blsub.{u, max v w} o f ≤ blsub.{v, max u w} o' g := + bsup_le_of_brange_subset.{u, v, w} fun a ⟨b, hb, hb'⟩ => + by + obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩ + simp_rw [← hc'] at hb' + exact ⟨c, hc, hb'⟩ +#align ordinal.blsub_le_of_brange_subset Ordinal.blsub_le_of_brange_subset + +theorem blsub_eq_of_brange_eq {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} + (h : { o | ∃ i hi, f i hi = o } = { o | ∃ i hi, g i hi = o }) : + blsub.{u, max v w} o f = blsub.{v, max u w} o' g := + (blsub_le_of_brange_subset.{u, v, w} h.le).antisymm (blsub_le_of_brange_subset.{v, u, w} h.ge) +#align ordinal.blsub_eq_of_brange_eq Ordinal.blsub_eq_of_brange_eq + +theorem bsup_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}} + (hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}} + (hg : blsub.{_, u} o' g = o) : + (bsup.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = bsup.{_, w} o f := by + apply le_antisymm <;> refine' bsup_le fun i hi => _ + · apply le_bsup + · rw [← hg, lt_blsub_iff] at hi + rcases hi with ⟨j, hj, hj'⟩ + exact (hf _ _ hj').trans (le_bsup _ _ _) +#align ordinal.bsup_comp Ordinal.bsup_comp + +theorem blsub_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}} + (hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}} + (hg : blsub.{_, u} o' g = o) : + (blsub.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = blsub.{_, w} o f := + @bsup_comp.{u, v, w} o _ (fun a ha => succ (f a ha)) + (fun {_ _} _ _ h => succ_le_succ_iff.2 (hf _ _ h)) g hg +#align ordinal.blsub_comp Ordinal.blsub_comp + +theorem IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} + (h : IsLimit o) : (Ordinal.bsup.{_, v} o fun x _ => f x) = f o := by + rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.1, bsup_id_limit h.2] +#align ordinal.is_normal.bsup_eq Ordinal.IsNormal.bsup_eq + +theorem IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} + (h : IsLimit o) : (blsub.{_, v} o fun x _ => f x) = f o := by + rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h] + exact fun a _ => H.1 a +#align ordinal.is_normal.blsub_eq Ordinal.IsNormal.blsub_eq + +theorem isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} : + IsNormal f ↔ (∀ a, f a < f (succ a)) ∧ ∀ o, IsLimit o → (bsup.{_, v} o fun x _ => f x) = f o := + ⟨fun h => ⟨h.1, @IsNormal.bsup_eq f h⟩, fun ⟨h₁, h₂⟩ => + ⟨h₁, fun o ho a => by + rw [← h₂ o ho] + exact bsup_le_iff⟩⟩ +#align ordinal.is_normal_iff_lt_succ_and_bsup_eq Ordinal.isNormal_iff_lt_succ_and_bsup_eq + +theorem isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} : + IsNormal f ↔ (∀ a, f a < f (succ a)) ∧ + ∀ o, IsLimit o → (blsub.{_, v} o fun x _ => f x) = f o := by + rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff] + intro h + constructor <;> intro H o ho <;> have := H o ho <;> + rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at * +#align ordinal.is_normal_iff_lt_succ_and_blsub_eq Ordinal.isNormal_iff_lt_succ_and_blsub_eq + +theorem IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) + (hg : IsNormal g) : f = g ↔ f 0 = g 0 ∧ ∀ a, f a = g a → f (succ a) = g (succ a) := + ⟨fun h => by simp [h], fun ⟨h₁, h₂⟩ => + funext fun a => by + apply a.limitRecOn + assumption' + intro o ho H + rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho] + congr + ext (b hb) + exact H b hb⟩ +#align ordinal.is_normal.eq_iff_zero_and_succ Ordinal.IsNormal.eq_iff_zero_and_succ + +/-! ### Minimum excluded ordinals -/ + + +/-- The minimum excluded ordinal in a family of ordinals. -/ +def mex {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal := + infₛ (Set.range fᶜ) +#align ordinal.mex Ordinal.mex + +theorem mex_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : mex.{_, v} f ∉ Set.range f := + cinfₛ_mem (nonempty_compl_range.{_, v} f) +#align ordinal.mex_not_mem_range Ordinal.mex_not_mem_range + +theorem le_mex_of_forall {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal} + (H : ∀ b < a, ∃ i, f i = b) : a ≤ mex.{_, v} f := by + by_contra' h + exact mex_not_mem_range f (H _ h) +#align ordinal.le_mex_of_forall Ordinal.le_mex_of_forall + +theorem ne_mex {ι : Type u} (f : ι → Ordinal.{max u v}) : ∀ i, f i ≠ mex.{_, v} f := by + simpa using mex_not_mem_range.{_, v} f +#align ordinal.ne_mex Ordinal.ne_mex + +theorem mex_le_of_ne {ι} {f : ι → Ordinal} {a} (ha : ∀ i, f i ≠ a) : mex f ≤ a := + cinfₛ_le' (by simp [ha]) +#align ordinal.mex_le_of_ne Ordinal.mex_le_of_ne + +theorem exists_of_lt_mex {ι} {f : ι → Ordinal} {a} (ha : a < mex f) : ∃ i, f i = a := by + by_contra' ha' + exact ha.not_le (mex_le_of_ne ha') +#align ordinal.exists_of_lt_mex Ordinal.exists_of_lt_mex + +theorem mex_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : mex.{_, v} f ≤ lsub.{_, v} f := + cinfₛ_le' (lsub_not_mem_range f) +#align ordinal.mex_le_lsub Ordinal.mex_le_lsub + +theorem mex_monotone {α β : Type u} {f : α → Ordinal.{max u v}} {g : β → Ordinal.{max u v}} + (h : Set.range f ⊆ Set.range g) : mex.{_, v} f ≤ mex.{_, v} g := by + refine' mex_le_of_ne fun i hi => _ + cases' h ⟨i, rfl⟩ with j hj + rw [← hj] at hi + exact ne_mex g j hi +#align ordinal.mex_monotone Ordinal.mex_monotone + +theorem mex_lt_ord_succ_mk {ι : Type u} (f : ι → Ordinal.{u}) : + mex.{_, u} f < (succ (#ι)).ord := by + by_contra' h + apply (lt_succ (#ι)).not_le + have H := fun a => exists_of_lt_mex ((typein_lt_self a).trans_le h) + let g : (succ (#ι)).ord.out.α → ι := fun a => Classical.choose (H a) + have hg : Injective g := fun a b h' => by + have Hf : ∀ x, f (g x) = + typein ((· < ·) : (succ (#ι)).ord.out.α → (succ (#ι)).ord.out.α → Prop) x := + fun a => Classical.choose_spec (H a) + apply_fun f at h' + rwa [Hf, Hf, typein_inj] at h' + -- Porting note: `convert` & `rw` → `have` & `rwa` + have hg' := Cardinal.mk_le_of_injective hg + rwa [Cardinal.mk_ord_out (succ (#ι))] at hg' +#align ordinal.mex_lt_ord_succ_mk Ordinal.mex_lt_ord_succ_mk + +/-- The minimum excluded ordinal of a family of ordinals indexed by the set of ordinals less than + some `o : Ordinal.{u}`. This is a special case of `mex` over the family provided by + `familyOfBFamily`. + + This is to `mex` as `bsup` is to `sup`. -/ +def bmex (o : Ordinal) (f : ∀ a < o, Ordinal) : Ordinal := + mex (familyOfBFamily o f) +#align ordinal.bmex Ordinal.bmex + +theorem bmex_not_mem_brange {o : Ordinal} (f : ∀ a < o, Ordinal) : bmex o f ∉ brange o f := by + rw [← range_familyOfBFamily] + apply mex_not_mem_range +#align ordinal.bmex_not_mem_brange Ordinal.bmex_not_mem_brange + +theorem le_bmex_of_forall {o : Ordinal} (f : ∀ a < o, Ordinal) {a : Ordinal} + (H : ∀ b < a, ∃ i hi, f i hi = b) : a ≤ bmex o f := by + by_contra' h + exact bmex_not_mem_brange f (H _ h) +#align ordinal.le_bmex_of_forall Ordinal.le_bmex_of_forall + +theorem ne_bmex {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {i} (hi) : + f i hi ≠ bmex.{_, v} o f := by + convert ne_mex.{_, v} (familyOfBFamily o f) (enum (· < ·) i (by rwa [type_lt])) + -- Porting note: `familyOfBFamily_enum` → `typein_enum` + rw [typein_enum] +#align ordinal.ne_bmex Ordinal.ne_bmex + +theorem bmex_le_of_ne {o : Ordinal} {f : ∀ a < o, Ordinal} {a} (ha : ∀ i hi, f i hi ≠ a) : + bmex o f ≤ a := + mex_le_of_ne fun _i => ha _ _ +#align ordinal.bmex_le_of_ne Ordinal.bmex_le_of_ne + +theorem exists_of_lt_bmex {o : Ordinal} {f : ∀ a < o, Ordinal} {a} (ha : a < bmex o f) : + ∃ i hi, f i hi = a := by + cases' exists_of_lt_mex ha with i hi + exact ⟨_, typein_lt_self i, hi⟩ +#align ordinal.exists_of_lt_bmex Ordinal.exists_of_lt_bmex + +theorem bmex_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : + bmex.{_, v} o f ≤ blsub.{_, v} o f := + mex_le_lsub _ +#align ordinal.bmex_le_blsub Ordinal.bmex_le_blsub + +theorem bmex_monotone {o o' : Ordinal.{u}} + {f : ∀ a < o, Ordinal.{max u v}} {g : ∀ a < o', Ordinal.{max u v}} + (h : brange o f ⊆ brange o' g) : bmex.{_, v} o f ≤ bmex.{_, v} o' g := + mex_monotone (by rwa [range_familyOfBFamily, range_familyOfBFamily]) +#align ordinal.bmex_monotone Ordinal.bmex_monotone + +theorem bmex_lt_ord_succ_card {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{u}) : + bmex.{_, u} o f < (succ o.card).ord := + by + rw [← mk_ordinal_out] + exact mex_lt_ord_succ_mk (familyOfBFamily o f) +#align ordinal.bmex_lt_ord_succ_card Ordinal.bmex_lt_ord_succ_card + +end Ordinal + +/-! ### Results about injectivity and surjectivity -/ + + +theorem not_surjective_of_ordinal {α : Type u} (f : α → Ordinal.{u}) : ¬Surjective f := fun h => + Ordinal.lsub_not_mem_range.{u, u} f (h _) +#align not_surjective_of_ordinal not_surjective_of_ordinal + +theorem not_injective_of_ordinal {α : Type u} (f : Ordinal.{u} → α) : ¬Injective f := fun h => + not_surjective_of_ordinal _ (invFun_surjective h) +#align not_injective_of_ordinal not_injective_of_ordinal + +theorem not_surjective_of_ordinal_of_small {α : Type v} [Small.{u} α] (f : α → Ordinal.{u}) : + ¬Surjective f := fun h => not_surjective_of_ordinal _ (h.comp (equivShrink _).symm.surjective) +#align not_surjective_of_ordinal_of_small not_surjective_of_ordinal_of_small + +theorem not_injective_of_ordinal_of_small {α : Type v} [Small.{u} α] (f : Ordinal.{u} → α) : + ¬Injective f := fun h => not_injective_of_ordinal _ ((equivShrink _).injective.comp h) +#align not_injective_of_ordinal_of_small not_injective_of_ordinal_of_small + +/-- The type of ordinals in universe `u` is not `Small.{u}`. This is the type-theoretic analog of +the Burali-Forti paradox. -/ +theorem not_small_ordinal : ¬Small.{u} Ordinal.{max u v} := fun h => + @not_injective_of_ordinal_of_small _ h _ fun _a _b => Ordinal.lift_inj.{v, u}.1 +#align not_small_ordinal not_small_ordinal + +/-! ### Enumerating unbounded sets of ordinals with ordinals -/ + + +namespace Ordinal + +section + +/-- Enumerator function for an unbounded set of ordinals. -/ +def enumOrd (S : Set Ordinal.{u}) : Ordinal → Ordinal := + lt_wf.fix fun o f => infₛ (S ∩ Set.Ici (blsub.{u, u} o f)) +#align ordinal.enum_ord Ordinal.enumOrd + +variable {S : Set Ordinal.{u}} + +/-- The equation that characterizes `enumOrd` definitionally. This isn't the nicest expression to + work with, so consider using `enumOrd_def` instead. -/ +theorem enumOrd_def' (o) : + enumOrd S o = infₛ (S ∩ Set.Ici (blsub.{u, u} o fun a _ => enumOrd S a)) := + lt_wf.fix_eq _ _ +#align ordinal.enum_ord_def' Ordinal.enumOrd_def' + +/-- The set in `enumOrd_def'` is nonempty. -/ +theorem enumOrd_def'_nonempty (hS : Unbounded (· < ·) S) (a) : (S ∩ Set.Ici a).Nonempty := + let ⟨b, hb, hb'⟩ := hS a + ⟨b, hb, le_of_not_gt hb'⟩ +#align ordinal.enum_ord_def'_nonempty Ordinal.enumOrd_def'_nonempty + +private theorem enumOrd_mem_aux (hS : Unbounded (· < ·) S) (o) : + enumOrd S o ∈ S ∩ Set.Ici (blsub.{u, u} o fun c _ => enumOrd S c) := by + rw [enumOrd_def'] + exact cinfₛ_mem (enumOrd_def'_nonempty hS _) + +theorem enumOrd_mem (hS : Unbounded (· < ·) S) (o) : enumOrd S o ∈ S := + (enumOrd_mem_aux hS o).left +#align ordinal.enum_ord_mem Ordinal.enumOrd_mem + +theorem blsub_le_enumOrd (hS : Unbounded (· < ·) S) (o) : + (blsub.{u, u} o fun c _ => enumOrd S c) ≤ enumOrd S o := + (enumOrd_mem_aux hS o).right +#align ordinal.blsub_le_enum_ord Ordinal.blsub_le_enumOrd + +theorem enumOrd_strictMono (hS : Unbounded (· < ·) S) : StrictMono (enumOrd S) := fun _ _ h => + (lt_blsub.{u, u} _ _ h).trans_le (blsub_le_enumOrd hS _) +#align ordinal.enum_ord_strict_mono Ordinal.enumOrd_strictMono + +/-- A more workable definition for `enumOrd`. -/ +theorem enumOrd_def (o) : enumOrd S o = infₛ (S ∩ { b | ∀ c, c < o → enumOrd S c < b }) := by + rw [enumOrd_def'] + congr ; ext + exact ⟨fun h a hao => (lt_blsub.{u, u} _ _ hao).trans_le h, blsub_le⟩ +#align ordinal.enum_ord_def Ordinal.enumOrd_def + +/-- The set in `enumOrd_def` is nonempty. -/ +theorem enumOrd_def_nonempty (hS : Unbounded (· < ·) S) {o} : + { x | x ∈ S ∧ ∀ c, c < o → enumOrd S c < x }.Nonempty := + ⟨_, enumOrd_mem hS o, fun _ b => enumOrd_strictMono hS b⟩ +#align ordinal.enum_ord_def_nonempty Ordinal.enumOrd_def_nonempty + +@[simp] +theorem enumOrd_range {f : Ordinal → Ordinal} (hf : StrictMono f) : enumOrd (range f) = f := + funext fun o => by + apply Ordinal.induction o + intro a H + rw [enumOrd_def a] + have Hfa : f a ∈ range f ∩ { b | ∀ c, c < a → enumOrd (range f) c < b } := + ⟨mem_range_self a, fun b hb => by + rw [H b hb] + exact hf hb⟩ + refine' (cinfₛ_le' Hfa).antisymm ((le_cinfₛ_iff'' ⟨_, Hfa⟩).2 _) + rintro _ ⟨⟨c, rfl⟩, hc : ∀ b < a, enumOrd (range f) b < f c⟩ + rw [hf.le_iff_le] + contrapose! hc + exact ⟨c, hc, (H c hc).ge⟩ +#align ordinal.enum_ord_range Ordinal.enumOrd_range + +@[simp] +theorem enumOrd_univ : enumOrd Set.univ = id := by + rw [← range_id] + exact enumOrd_range strictMono_id +#align ordinal.enum_ord_univ Ordinal.enumOrd_univ + +@[simp] +theorem enumOrd_zero : enumOrd S 0 = infₛ S := by + rw [enumOrd_def] + simp [Ordinal.not_lt_zero] +#align ordinal.enum_ord_zero Ordinal.enumOrd_zero + +theorem enumOrd_succ_le {a b} (hS : Unbounded (· < ·) S) (ha : a ∈ S) (hb : enumOrd S b < a) : + enumOrd S (succ b) ≤ a := by + rw [enumOrd_def] + exact + cinfₛ_le' ⟨ha, fun c hc => ((enumOrd_strictMono hS).monotone (le_of_lt_succ hc)).trans_lt hb⟩ +#align ordinal.enum_ord_succ_le Ordinal.enumOrd_succ_le + +theorem enumOrd_le_of_subset {S T : Set Ordinal} (hS : Unbounded (· < ·) S) (hST : S ⊆ T) (a) : + enumOrd T a ≤ enumOrd S a := by + apply Ordinal.induction a + intro b H + rw [enumOrd_def] + exact cinfₛ_le' ⟨hST (enumOrd_mem hS b), fun c h => (H c h).trans_lt (enumOrd_strictMono hS h)⟩ +#align ordinal.enum_ord_le_of_subset Ordinal.enumOrd_le_of_subset + +theorem enumOrd_surjective (hS : Unbounded (· < ·) S) : ∀ s ∈ S, ∃ a, enumOrd S a = s := fun s hs => + ⟨supₛ { a | enumOrd S a ≤ s }, by + apply le_antisymm + · rw [enumOrd_def] + refine' cinfₛ_le' ⟨hs, fun a ha => _⟩ + have : enumOrd S 0 ≤ s := by + rw [enumOrd_zero] + exact cinfₛ_le' hs + -- Porting note: `flip` is required to infer a metavariable. + rcases flip exists_lt_of_lt_csupₛ ha ⟨0, this⟩ with ⟨b, hb, hab⟩ + exact (enumOrd_strictMono hS hab).trans_le hb + · by_contra' h + exact + (le_csupₛ ⟨s, fun a => (lt_wf.self_le_of_strictMono (enumOrd_strictMono hS) a).trans⟩ + (enumOrd_succ_le hS hs h)).not_lt + (lt_succ _)⟩ +#align ordinal.enum_ord_surjective Ordinal.enumOrd_surjective + +/-- An order isomorphism between an unbounded set of ordinals and the ordinals. -/ +def enumOrdOrderIso (hS : Unbounded (· < ·) S) : Ordinal ≃o S := + StrictMono.orderIsoOfSurjective (fun o => ⟨_, enumOrd_mem hS o⟩) (enumOrd_strictMono hS) fun s => + let ⟨a, ha⟩ := enumOrd_surjective hS s s.prop + ⟨a, Subtype.eq ha⟩ +#align ordinal.enum_ord_order_iso Ordinal.enumOrdOrderIso + +theorem range_enumOrd (hS : Unbounded (· < ·) S) : range (enumOrd S) = S := by + rw [range_eq_iff] + exact ⟨enumOrd_mem hS, enumOrd_surjective hS⟩ +#align ordinal.range_enum_ord Ordinal.range_enumOrd + +/-- A characterization of `enumOrd`: it is the unique strict monotonic function with range `S`. -/ +theorem eq_enumOrd (f : Ordinal → Ordinal) (hS : Unbounded (· < ·) S) : + StrictMono f ∧ range f = S ↔ f = enumOrd S := by + constructor + · rintro ⟨h₁, h₂⟩ + rwa [← lt_wf.eq_strictMono_iff_eq_range h₁ (enumOrd_strictMono hS), range_enumOrd hS] + · rintro rfl + exact ⟨enumOrd_strictMono hS, range_enumOrd hS⟩ +#align ordinal.eq_enum_ord Ordinal.eq_enumOrd + +end + +/-! ### Ordinal exponential -/ + + +/-- The ordinal exponential, defined by transfinite recursion. -/ +instance : Pow Ordinal Ordinal := + ⟨fun a b => if a = 0 then 1 - b else limitRecOn b 1 (fun _ IH => IH * a) fun b _ => bsup.{u, u} b⟩ + +-- Porting note: Ambiguous notations. +-- local infixr:0 "^" => @Pow.pow Ordinal Ordinal Ordinal.instPowOrdinalOrdinal + +theorem opow_def (a b : Ordinal) : + (a^b) = if a = 0 then 1 - b else limitRecOn b 1 (fun _ IH => IH * a) fun b _ => bsup.{u, u} b := + rfl +#align ordinal.opow_def Ordinal.opow_def + +-- Porting note: `if_pos rfl` → `if_true` +theorem zero_opow' (a : Ordinal) : (0^a) = 1 - a := by simp only [opow_def, if_true] +#align ordinal.zero_opow' Ordinal.zero_opow' + +@[simp] +theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0^a) = 0 := by + rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero] +#align ordinal.zero_opow Ordinal.zero_opow + +@[simp] +theorem opow_zero (a : Ordinal) : (a^0) = 1 := by + by_cases a = 0 <;> [simp only [opow_def, if_pos h, sub_zero], + simp only [opow_def, if_neg h, limitRecOn_zero]] +#align ordinal.opow_zero Ordinal.opow_zero + +@[simp] +theorem opow_succ (a b : Ordinal) : (a^succ b) = (a^b) * a := + if h : a = 0 then by subst a; simp only [zero_opow (succ_ne_zero _), mul_zero] + else by simp only [opow_def, limitRecOn_succ, if_neg h] +#align ordinal.opow_succ Ordinal.opow_succ + +theorem opow_limit {a b : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) : + (a^b) = bsup.{u, u} b fun c _ => a^c := by + simp only [opow_def, if_neg a0]; rw [limitRecOn_limit _ _ _ _ h] +#align ordinal.opow_limit Ordinal.opow_limit + +theorem opow_le_of_limit {a b c : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) : + (a^b) ≤ c ↔ ∀ b' < b, (a^b') ≤ c := by rw [opow_limit a0 h, bsup_le_iff] +#align ordinal.opow_le_of_limit Ordinal.opow_le_of_limit + +theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) : + a < (b^c) ↔ ∃ c' < c, a < (b^c') := by + rw [← not_iff_not, not_exists]; simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and] +#align ordinal.lt_opow_of_limit Ordinal.lt_opow_of_limit + +@[simp] +theorem opow_one (a : Ordinal) : (a^1) = a := by + rw [← succ_zero, opow_succ]; simp only [opow_zero, one_mul] +#align ordinal.opow_one Ordinal.opow_one + +@[simp] +theorem one_opow (a : Ordinal) : (1^a) = 1 := by + apply limitRecOn a + · simp only [opow_zero] + · intro _ ih + simp only [opow_succ, ih, mul_one] + refine' fun b l IH => eq_of_forall_ge_iff fun c => _ + rw [opow_le_of_limit Ordinal.one_ne_zero l] + exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩ +#align ordinal.one_opow Ordinal.one_opow + +theorem opow_pos {a : Ordinal} (b) (a0 : 0 < a) : 0 < (a^b) := by + have h0 : 0 < (a^0) := by simp only [opow_zero, zero_lt_one] + apply limitRecOn b + · exact h0 + · intro b IH + rw [opow_succ] + exact mul_pos IH a0 + · exact fun b l _ => (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩ +#align ordinal.opow_pos Ordinal.opow_pos + +theorem opow_ne_zero {a : Ordinal} (b) (a0 : a ≠ 0) : (a^b) ≠ 0 := + Ordinal.pos_iff_ne_zero.1 <| opow_pos b <| Ordinal.pos_iff_ne_zero.2 a0 +#align ordinal.opow_ne_zero Ordinal.opow_ne_zero + +theorem opow_isNormal {a : Ordinal} (h : 1 < a) : IsNormal ((·^·) a) := + have a0 : 0 < a := zero_lt_one.trans h + ⟨fun b => by simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h, + fun b l c => opow_le_of_limit (ne_of_gt a0) l⟩ +#align ordinal.opow_is_normal Ordinal.opow_isNormal + +theorem opow_lt_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : (a^b) < (a^c) ↔ b < c := + (opow_isNormal a1).lt_iff +#align ordinal.opow_lt_opow_iff_right Ordinal.opow_lt_opow_iff_right + +theorem opow_le_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : (a^b) ≤ (a^c) ↔ b ≤ c := + (opow_isNormal a1).le_iff +#align ordinal.opow_le_opow_iff_right Ordinal.opow_le_opow_iff_right + +theorem opow_right_inj {a b c : Ordinal} (a1 : 1 < a) : (a^b) = (a^c) ↔ b = c := + (opow_isNormal a1).inj +#align ordinal.opow_right_inj Ordinal.opow_right_inj + +theorem opow_isLimit {a b : Ordinal} (a1 : 1 < a) : IsLimit b → IsLimit (a^b) := + (opow_isNormal a1).isLimit +#align ordinal.opow_is_limit Ordinal.opow_isLimit + +theorem opow_isLimit_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a^b) := by + rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l') + · exact absurd e hb + · rw [opow_succ] + exact mul_isLimit (opow_pos _ l.pos) l + · exact opow_isLimit l.one_lt l' +#align ordinal.opow_is_limit_left Ordinal.opow_isLimit_left + +theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : (a^b) ≤ (a^c) := by + cases' lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ h₁ + · exact (opow_le_opow_iff_right h₁).2 h₂ + · subst a + -- Porting note: `le_refl` is required. + simp only [one_opow, le_refl] +#align ordinal.opow_le_opow_right Ordinal.opow_le_opow_right + +theorem opow_le_opow_left {a b : Ordinal} (c) (ab : a ≤ b) : (a^c) ≤ (b^c) := by + by_cases a0 : a = 0 + -- Porting note: `le_refl` is required. + · subst a + by_cases c0 : c = 0 + · subst c + simp only [opow_zero, le_refl] + · simp only [zero_opow c0, Ordinal.zero_le] + · apply limitRecOn c + · simp only [opow_zero, le_refl] + · intro c IH + simpa only [opow_succ] using mul_le_mul' IH ab + · + exact fun c l IH => + (opow_le_of_limit a0 l).2 fun b' h => + (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le) +#align ordinal.opow_le_opow_left Ordinal.opow_le_opow_left + +theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ (a^b) := by + nth_rw 1 [← opow_one a] + cases' le_or_gt a 1 with a1 a1 + · cases' lt_or_eq_of_le a1 with a0 a1 + · rw [lt_one_iff_zero] at a0 + rw [a0, zero_opow Ordinal.one_ne_zero] + exact Ordinal.zero_le _ + rw [a1, one_opow, one_opow] + rwa [opow_le_opow_iff_right a1, one_le_iff_pos] +#align ordinal.left_le_opow Ordinal.left_le_opow + +theorem right_le_opow {a : Ordinal} (b) (a1 : 1 < a) : b ≤ (a^b) := + (opow_isNormal a1).self_le _ +#align ordinal.right_le_opow Ordinal.right_le_opow + +theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : (a^succ c) < (b^succ c) := by + rw [opow_succ, opow_succ] + exact + (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt + (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab))) +#align ordinal.opow_lt_opow_left_of_succ Ordinal.opow_lt_opow_left_of_succ + +theorem opow_add (a b c : Ordinal) : a^(b + c) = (a^b) * (a^c) := by + rcases eq_or_ne a 0 with (rfl | a0) + · rcases eq_or_ne c 0 with (rfl | c0) + · simp + have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne' + simp only [zero_opow c0, zero_opow this, mul_zero] + rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1) + · simp only [one_opow, mul_one] + apply limitRecOn c + · simp + · intro c IH + rw [add_succ, opow_succ, IH, opow_succ, mul_assoc] + · intro c l IH + refine' + eq_of_forall_ge_iff fun d => + (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _ + dsimp only [Function.comp] + simp (config := { contextual := true }) only [IH] + exact + (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans + (opow_isNormal a1)).limit_le + l).symm +#align ordinal.opow_add Ordinal.opow_add + +theorem opow_one_add (a b : Ordinal) : a^(1 + b) = a * (a^b) := by rw [opow_add, opow_one] +#align ordinal.opow_one_add Ordinal.opow_one_add + +theorem opow_dvd_opow (a) {b c : Ordinal} (h : b ≤ c) : (a^b) ∣ (a^c) := by + rw [← Ordinal.add_sub_cancel_of_le h, opow_add] + apply dvd_mul_right +#align ordinal.opow_dvd_opow Ordinal.opow_dvd_opow + +theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : (a^b) ∣ (a^c) ↔ b ≤ c := + ⟨fun h => + le_of_not_lt fun hn => + not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) <| + le_of_dvd (opow_ne_zero _ <| one_le_iff_ne_zero.1 <| a1.le) h, + opow_dvd_opow _⟩ +#align ordinal.opow_dvd_opow_iff Ordinal.opow_dvd_opow_iff + +theorem opow_mul (a b c : Ordinal) : a^(b * c) = ((a^b)^c) := by + by_cases b0 : b = 0; · simp only [b0, zero_mul, opow_zero, one_opow] + by_cases a0 : a = 0 + · subst a + by_cases c0 : c = 0 + · simp only [c0, mul_zero, opow_zero] + simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)] + cases' eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 a1 + · subst a1 + simp only [one_opow] + apply limitRecOn c + · simp only [mul_zero, opow_zero] + · intro c IH + rw [mul_succ, opow_add, IH, opow_succ] + · intro c l IH + refine' + eq_of_forall_ge_iff fun d => + (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le + l).trans + _ + dsimp only [Function.comp] + simp (config := { contextual := true }) only [IH] + exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm +#align ordinal.opow_mul Ordinal.opow_mul + +/-! ### Ordinal logarithm -/ + + +/-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and + `w < b ^ u`. -/ +-- @[pp_nodot] -- Porting note: Unknown attribute. +def log (b : Ordinal) (x : Ordinal) : Ordinal := + if _h : 1 < b then pred (infₛ { o | x < (b^o) }) else 0 +#align ordinal.log Ordinal.log + +/-- The set in the definition of `log` is nonempty. -/ +theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o | x < (b^o) }.Nonempty := + ⟨_, succ_le_iff.1 (right_le_opow _ h)⟩ +#align ordinal.log_nonempty Ordinal.log_nonempty + +theorem log_def {b : Ordinal} (h : 1 < b) (x : Ordinal) : log b x = pred (infₛ { o | x < (b^o) }) := + by simp only [log, dif_pos h] +#align ordinal.log_def Ordinal.log_def + +theorem log_of_not_one_lt_left {b : Ordinal} (h : ¬1 < b) (x : Ordinal) : log b x = 0 := by + simp only [log, dif_neg h] +#align ordinal.log_of_not_one_lt_left Ordinal.log_of_not_one_lt_left + +theorem log_of_left_le_one {b : Ordinal} (h : b ≤ 1) : ∀ x, log b x = 0 := + log_of_not_one_lt_left h.not_lt +#align ordinal.log_of_left_le_one Ordinal.log_of_left_le_one + +@[simp] +theorem log_zero_left : ∀ b, log 0 b = 0 := + log_of_left_le_one zero_le_one +#align ordinal.log_zero_left Ordinal.log_zero_left + +@[simp] +theorem log_zero_right (b : Ordinal) : log b 0 = 0 := + if b1 : 1 < b then by + rw [log_def b1, ← Ordinal.le_zero, pred_le] + apply cinfₛ_le' + dsimp + rw [succ_zero, opow_one] + exact zero_lt_one.trans b1 + else by simp only [log_of_not_one_lt_left b1] +#align ordinal.log_zero_right Ordinal.log_zero_right + +@[simp] +theorem log_one_left : ∀ b, log 1 b = 0 := + log_of_left_le_one le_rfl +#align ordinal.log_one_left Ordinal.log_one_left + +theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : + succ (log b x) = infₛ { o | x < (b^o) } := by + let t := infₛ { o | x < (b^o) } + have : x < (b^t) := cinfₛ_mem (log_nonempty hb) + rcases zero_or_succ_or_limit t with (h | h | h) + · refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim + simpa only [h, opow_zero] using this + · rw [show log b x = pred t from log_def hb x, succ_pred_iff_is_succ.2 h] + · rcases(lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩ + exact h₁.not_le.elim ((le_cinfₛ_iff'' (log_nonempty hb)).1 le_rfl a h₂) +#align ordinal.succ_log_def Ordinal.succ_log_def + +theorem lt_opow_succ_log_self {b : Ordinal} (hb : 1 < b) (x : Ordinal) : x < (b^succ (log b x)) := + by + rcases eq_or_ne x 0 with (rfl | hx) + · apply opow_pos _ (zero_lt_one.trans hb) + · rw [succ_log_def hb hx] + exact cinfₛ_mem (log_nonempty hb) +#align ordinal.lt_opow_succ_log_self Ordinal.lt_opow_succ_log_self + +theorem opow_log_le_self (b) {x : Ordinal} (hx : x ≠ 0) : (b^log b x) ≤ x := by + rcases eq_or_ne b 0 with (rfl | b0) + · rw [zero_opow'] + refine' (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx) + rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl) + · refine' le_of_not_lt fun h => (lt_succ (log b x)).not_le _ + have := @cinfₛ_le' _ _ { o | x < (b^o) } _ h + rwa [← succ_log_def hb hx] at this + · rwa [one_opow, one_le_iff_ne_zero] +#align ordinal.opow_log_le_self Ordinal.opow_log_le_self + +/-- `opow b` and `log b` (almost) form a Galois connection. -/ +theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : (b^c) ≤ x ↔ c ≤ log b x := + ⟨fun h => + le_of_not_lt fun hn => + (lt_opow_succ_log_self hb x).not_le <| + ((opow_le_opow_iff_right hb).2 (succ_le_of_lt hn)).trans h, + fun h => ((opow_le_opow_iff_right hb).2 h).trans (opow_log_le_self b hx)⟩ +#align ordinal.opow_le_iff_le_log Ordinal.opow_le_iff_le_log + +theorem lt_opow_iff_log_lt {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < (b^c) ↔ log b x < c := + lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx) +#align ordinal.lt_opow_iff_log_lt Ordinal.lt_opow_iff_log_lt + +theorem log_pos {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < log b o := by + rwa [← succ_le_iff, succ_zero, ← opow_le_iff_le_log hb ho, opow_one] +#align ordinal.log_pos Ordinal.log_pos + +theorem log_eq_zero {b o : Ordinal} (hbo : o < b) : log b o = 0 := by + rcases eq_or_ne o 0 with (rfl | ho) + · exact log_zero_right b + cases' le_or_lt b 1 with hb hb + · rcases le_one_iff.1 hb with (rfl | rfl) + · exact log_zero_left o + · exact log_one_left o + · rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one] +#align ordinal.log_eq_zero Ordinal.log_eq_zero + +-- @[mono] -- Porting note: Unknown attribute. +theorem log_mono_right (b) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y := + if hx : x = 0 then by simp only [hx, log_zero_right, Ordinal.zero_le] + else + if hb : 1 < b then + (opow_le_iff_le_log hb (lt_of_lt_of_le (Ordinal.pos_iff_ne_zero.2 hx) xy).ne').1 <| + (opow_log_le_self _ hx).trans xy + else by simp only [log_of_not_one_lt_left hb, Ordinal.zero_le] +#align ordinal.log_mono_right Ordinal.log_mono_right + +theorem log_le_self (b x : Ordinal) : log b x ≤ x := + if hx : x = 0 then by simp only [hx, log_zero_right, Ordinal.zero_le] + else + if hb : 1 < b then (right_le_opow _ hb).trans (opow_log_le_self b hx) + else by simp only [log_of_not_one_lt_left hb, Ordinal.zero_le] +#align ordinal.log_le_self Ordinal.log_le_self + +@[simp] +theorem log_one_right (b : Ordinal) : log b 1 = 0 := + if hb : 1 < b then log_eq_zero hb else log_of_not_one_lt_left hb 1 +#align ordinal.log_one_right Ordinal.log_one_right + +theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b^log b o) < o := by + rcases eq_or_ne b 0 with (rfl | hb) + · simpa using Ordinal.pos_iff_ne_zero.2 ho + · exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho) +#align ordinal.mod_opow_log_lt_self Ordinal.mod_opow_log_lt_self + +theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : + log b (o % (b^log b o)) < log b o := by + cases' eq_or_ne (o % (b^log b o)) 0 with h h + · rw [h, log_zero_right] + apply log_pos hb ho hbo + · rw [← succ_le_iff, succ_log_def hb h] + apply cinfₛ_le' + apply mod_lt + rw [← Ordinal.pos_iff_ne_zero] + exact opow_pos _ (zero_lt_one.trans hb) +#align ordinal.log_mod_opow_log_lt_log_self Ordinal.log_mod_opow_log_lt_log_self + +theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u) (hv : v ≠ 0) (w) : 0 < (b^u) * v + w := + (opow_pos u <| Ordinal.pos_iff_ne_zero.2 hb).trans_le <| + (le_mul_left _ <| Ordinal.pos_iff_ne_zero.2 hv).trans <| le_add_right _ _ +#align ordinal.opow_mul_add_pos Ordinal.opow_mul_add_pos + +theorem opow_mul_add_lt_opow_mul_succ {b u w : Ordinal} (v : Ordinal) (hw : w < (b^u)) : + (b^u) * v + w < (b^u) * succ v := by rwa [mul_succ, add_lt_add_iff_left] +#align ordinal.opow_mul_add_lt_opow_mul_succ Ordinal.opow_mul_add_lt_opow_mul_succ + +theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < (b^u)) : + (b^u) * v + w < (b^succ u) := by + convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le (mul_le_mul_left' (succ_le_of_lt hvb) _) + exact opow_succ b u +#align ordinal.opow_mul_add_lt_opow_succ Ordinal.opow_mul_add_lt_opow_succ + +theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b) + (hw : w < (b^u)) : log b ((b^u) * v + w) = u := by + have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne' + by_contra' hne + cases' lt_or_gt_of_ne hne with h h + · rw [← lt_opow_iff_log_lt hb hne'] at h + exact h.not_le ((le_mul_left _ (Ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _)) + · conv at h => change u < log b (b ^ u * v + w) + rw [← succ_le_iff, ← opow_le_iff_le_log hb hne'] at h + exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw) +#align ordinal.log_opow_mul_add Ordinal.log_opow_mul_add + +theorem log_opow {b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b^x) = x := by + convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb)) + rw [add_zero, mul_one] +#align ordinal.log_opow Ordinal.log_opow + +theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b^log b o) < b := by + rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ] + exact lt_opow_succ_log_self hb o +#align ordinal.div_opow_log_lt Ordinal.div_opow_log_lt + +theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y ≠ 0) : + log b x + log b y ≤ log b (x * y) := by + by_cases hb : 1 < b + · rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add] + exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy) + -- Porting note: `le_refl` is required. + simp only [log_of_not_one_lt_left hb, zero_add, le_refl] +#align ordinal.add_log_le_log_mul Ordinal.add_log_le_log_mul + +/-! ### Casting naturals into ordinals, compatibility with operations -/ + + +@[simp] +theorem one_add_nat_cast (m : ℕ) : 1 + (m : Ordinal) = succ m := by + rw [← Nat.cast_one, ← Nat.cast_add, add_comm] + rfl +#align ordinal.one_add_nat_cast Ordinal.one_add_nat_cast + +@[simp, norm_cast] +theorem nat_cast_mul (m : ℕ) : ∀ n : ℕ, ((m * n : ℕ) : Ordinal) = m * n + | 0 => by simp + | n + 1 => by rw [Nat.mul_succ, Nat.cast_add, nat_cast_mul m n, Nat.cast_succ, mul_add_one] +#align ordinal.nat_cast_mul Ordinal.nat_cast_mul + +@[simp, norm_cast] +theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((m ^ n : ℕ) : Ordinal) = (m^n) + | 0 => by simp + | n + 1 => by + rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ] +#align ordinal.nat_cast_opow Ordinal.nat_cast_opow + +@[simp, norm_cast] +theorem nat_cast_le {m n : ℕ} : (m : Ordinal) ≤ n ↔ m ≤ n := by + rw [← Cardinal.ord_nat, ← Cardinal.ord_nat, Cardinal.ord_le_ord, Cardinal.natCast_le] +#align ordinal.nat_cast_le Ordinal.nat_cast_le + +@[simp, norm_cast] +theorem nat_cast_lt {m n : ℕ} : (m : Ordinal) < n ↔ m < n := by + simp only [lt_iff_le_not_le, nat_cast_le] +#align ordinal.nat_cast_lt Ordinal.nat_cast_lt + +@[simp, norm_cast] +theorem nat_cast_inj {m n : ℕ} : (m : Ordinal) = n ↔ m = n := by + simp only [le_antisymm_iff, nat_cast_le] +#align ordinal.nat_cast_inj Ordinal.nat_cast_inj + +@[simp, norm_cast] +theorem nat_cast_eq_zero {n : ℕ} : (n : Ordinal) = 0 ↔ n = 0 := + @nat_cast_inj n 0 +#align ordinal.nat_cast_eq_zero Ordinal.nat_cast_eq_zero + +theorem nat_cast_ne_zero {n : ℕ} : (n : Ordinal) ≠ 0 ↔ n ≠ 0 := + not_congr nat_cast_eq_zero +#align ordinal.nat_cast_ne_zero Ordinal.nat_cast_ne_zero + +@[simp, norm_cast] +theorem nat_cast_pos {n : ℕ} : (0 : Ordinal) < n ↔ 0 < n := + @nat_cast_lt 0 n +#align ordinal.nat_cast_pos Ordinal.nat_cast_pos + +@[simp, norm_cast] +theorem nat_cast_sub (m n : ℕ) : ((m - n : ℕ) : Ordinal) = m - n := by + cases' le_total m n with h h + · rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)] + rfl + · apply (add_left_cancel n).1 + rw [← Nat.cast_add, add_tsub_cancel_of_le h, Ordinal.add_sub_cancel_of_le (nat_cast_le.2 h)] +#align ordinal.nat_cast_sub Ordinal.nat_cast_sub + +@[simp, norm_cast] +theorem nat_cast_div (m n : ℕ) : ((m / n : ℕ) : Ordinal) = m / n := by + rcases eq_or_ne n 0 with (rfl | hn) + · simp + · have hn' := nat_cast_ne_zero.2 hn + apply le_antisymm + · rw [le_div hn', ← nat_cast_mul, nat_cast_le, mul_comm] + apply Nat.div_mul_le_self + · rw [div_le hn', ← add_one_eq_succ, ← Nat.cast_succ, ← nat_cast_mul, nat_cast_lt, mul_comm, ← + Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)] + apply Nat.lt_succ_self +#align ordinal.nat_cast_div Ordinal.nat_cast_div + +@[simp, norm_cast] +theorem nat_cast_mod (m n : ℕ) : ((m % n : ℕ) : Ordinal) = m % n := by + rw [← add_left_cancel, div_add_mod, ← nat_cast_div, ← nat_cast_mul, ← Nat.cast_add, + Nat.div_add_mod] +#align ordinal.nat_cast_mod Ordinal.nat_cast_mod + +@[simp] +theorem lift_nat_cast : ∀ n : ℕ, lift.{u, v} n = n + | 0 => by simp + | n + 1 => by simp [lift_nat_cast n] +#align ordinal.lift_nat_cast Ordinal.lift_nat_cast + +end Ordinal + +/-! ### Properties of `omega` -/ + + +namespace Cardinal + +open Ordinal + +@[simp] +theorem ord_aleph0 : ord.{u} ℵ₀ = ω := + le_antisymm (ord_le.2 <| le_rfl) <| + le_of_forall_lt fun o h => + by + rcases Ordinal.lt_lift_iff.1 h with ⟨o, rfl, h'⟩ + rw [lt_ord, ← lift_card, ← lift_aleph0.{0, u}, lift_lt, ← typein_enum (· < ·) h'] + exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩ +#align cardinal.ord_aleph_0 Cardinal.ord_aleph0 + +@[simp] +theorem add_one_of_aleph0_le {c} (h : ℵ₀ ≤ c) : c + 1 = c := by + rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega_le] + rwa [← ord_aleph0, ord_le_ord] +#align cardinal.add_one_of_aleph_0_le Cardinal.add_one_of_aleph0_le + +end Cardinal + +namespace Ordinal + +theorem lt_add_of_limit {a b c : Ordinal.{u}} (h : IsLimit c) : + a < b + c ↔ ∃ c' < c, a < b + c' := by + -- Porting note: `have` & `dsimp` are required for beta reduction. + have := IsNormal.bsup_eq.{u, u} (add_isNormal b) h + dsimp only at this + -- Porting note: `bex_def` is required. + rw [← this, lt_bsup, bex_def] +#align ordinal.lt_add_of_limit Ordinal.lt_add_of_limit + +theorem lt_omega {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n := by + simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat] +#align ordinal.lt_omega Ordinal.lt_omega + +theorem nat_lt_omega (n : ℕ) : ↑n < ω := + lt_omega.2 ⟨_, rfl⟩ +#align ordinal.nat_lt_omega Ordinal.nat_lt_omega + +theorem omega_pos : 0 < ω := + nat_lt_omega 0 +#align ordinal.omega_pos Ordinal.omega_pos + +theorem omega_ne_zero : ω ≠ 0 := + omega_pos.ne' +#align ordinal.omega_ne_zero Ordinal.omega_ne_zero + +theorem one_lt_omega : 1 < ω := by simpa only [Nat.cast_one] using nat_lt_omega 1 +#align ordinal.one_lt_omega Ordinal.one_lt_omega + +theorem omega_isLimit : IsLimit ω := + ⟨omega_ne_zero, fun o h => by + let ⟨n, e⟩ := lt_omega.1 h + rw [e]; exact nat_lt_omega (n + 1)⟩ +#align ordinal.omega_is_limit Ordinal.omega_isLimit + +theorem omega_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o := + ⟨fun h n => (nat_lt_omega _).le.trans h, fun H => + le_of_forall_lt fun a h => by + let ⟨n, e⟩ := lt_omega.1 h + rw [e, ← succ_le_iff]; exact H (n + 1)⟩ +#align ordinal.omega_le Ordinal.omega_le + +@[simp] +theorem sup_nat_cast : sup Nat.cast = ω := + (sup_le fun n => (nat_lt_omega n).le).antisymm <| omega_le.2 <| le_sup _ +#align ordinal.sup_nat_cast Ordinal.sup_nat_cast + +theorem nat_lt_limit {o} (h : IsLimit o) : ∀ n : ℕ, ↑n < o + | 0 => lt_of_le_of_ne (Ordinal.zero_le o) h.1.symm + | n + 1 => h.2 _ (nat_lt_limit h n) +#align ordinal.nat_lt_limit Ordinal.nat_lt_limit + +theorem omega_le_of_isLimit {o} (h : IsLimit o) : ω ≤ o := + omega_le.2 fun n => le_of_lt <| nat_lt_limit h n +#align ordinal.omega_le_of_is_limit Ordinal.omega_le_of_isLimit + +theorem isLimit_iff_omega_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ a := by + refine' ⟨fun l => ⟨l.1, ⟨a / ω, le_antisymm _ (mul_div_le _ _)⟩⟩, fun h => _⟩ + · refine' (limit_le l).2 fun x hx => le_of_lt _ + rw [← div_lt omega_ne_zero, ← succ_le_iff, le_div omega_ne_zero, mul_succ, + add_le_of_limit omega_isLimit] + intro b hb + rcases lt_omega.1 hb with ⟨n, rfl⟩ + exact + (add_le_add_right (mul_div_le _ _) _).trans + (lt_sub.1 <| nat_lt_limit (sub_isLimit l hx) _).le + · rcases h with ⟨a0, b, rfl⟩ + refine' mul_isLimit_left omega_isLimit (Ordinal.pos_iff_ne_zero.2 <| mt _ a0) + intro e + simp only [e, mul_zero] +#align ordinal.is_limit_iff_omega_dvd Ordinal.isLimit_iff_omega_dvd + +theorem add_mul_limit_aux {a b c : Ordinal} (ba : b + a = a) (l : IsLimit c) + (IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b) : (a + b) * c = a * c := + le_antisymm + ((mul_le_of_limit l).2 fun c' h => by + apply (mul_le_mul_left' (le_succ c') _).trans + rw [IH _ h] + apply (add_le_add_left _ _).trans + · rw [← mul_succ] + exact mul_le_mul_left' (succ_le_of_lt <| l.2 _ h) _ + · rw [← ba] + exact le_add_right _ _) + (mul_le_mul_right' (le_add_right _ _) _) +#align ordinal.add_mul_limit_aux Ordinal.add_mul_limit_aux + +theorem add_mul_succ {a b : Ordinal} (c) (ba : b + a = a) : (a + b) * succ c = a * succ c + b := by + apply limitRecOn c + · simp only [succ_zero, mul_one] + · intro c IH + rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ] + · intro c l IH + -- Porting note: Unused. + -- have := add_mul_limit_aux ba l IH + rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc] +#align ordinal.add_mul_succ Ordinal.add_mul_succ + +theorem add_mul_limit {a b c : Ordinal} (ba : b + a = a) (l : IsLimit c) : (a + b) * c = a * c := + add_mul_limit_aux ba l fun c' _ => add_mul_succ c' ba +#align ordinal.add_mul_limit Ordinal.add_mul_limit + +theorem add_le_of_forall_add_lt {a b c : Ordinal} (hb : 0 < b) (h : ∀ d < b, a + d < c) : + a + b ≤ c := by + have H : a + (c - a) = c := + Ordinal.add_sub_cancel_of_le + (by + rw [← add_zero a] + exact (h _ hb).le) + rw [← H] + apply add_le_add_left _ a + by_contra' hb + exact (h _ hb).ne H +#align ordinal.add_le_of_forall_add_lt Ordinal.add_le_of_forall_add_lt + +theorem IsNormal.apply_omega {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) : + Ordinal.sup.{0, u} (f ∘ Nat.cast) = f ω := by rw [← sup_nat_cast, IsNormal.sup.{0, u, u} hf] +#align ordinal.is_normal.apply_omega Ordinal.IsNormal.apply_omega + +@[simp] +theorem sup_add_nat (o : Ordinal) : (sup fun n : ℕ => o + n) = o + ω := + (add_isNormal o).apply_omega +#align ordinal.sup_add_nat Ordinal.sup_add_nat + +@[simp] +theorem sup_mul_nat (o : Ordinal) : (sup fun n : ℕ => o * n) = o * ω := by + rcases eq_zero_or_pos o with (rfl | ho) + · rw [zero_mul] + exact sup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal) + · exact (mul_isNormal ho).apply_omega +#align ordinal.sup_mul_nat Ordinal.sup_mul_nat + +-- Porting note: Ambiguous notations. +-- local infixr:0 "^" => @Pow.pow Ordinal Ordinal Ordinal.instPowOrdinalOrdinal + +theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o^n) = (o^ω) := by + rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl) + · exact (opow_isNormal ho₁).apply_omega + · rw [one_opow] + refine' le_antisymm (sup_le fun n => by rw [one_opow]) _ + convert le_sup (fun n : ℕ => 1^n) 0 + rw [Nat.cast_zero, opow_zero] +#align ordinal.sup_opow_nat Ordinal.sup_opow_nat + +end Ordinal + +-- Porting note: TODO: Port this meta code. + +-- namespace Tactic + +-- open Ordinal Mathlib.Meta.Positivity + +-- /-- Extension for the `positivity` tactic: `ordinal.opow` takes positive values on positive +-- inputs. -/ +-- @[positivity] +-- unsafe def positivity_opow : expr → tactic strictness +-- | q(@Pow.pow _ _ $(inst) $(a) $(b)) => do +-- let strictness_a ← core a +-- match strictness_a with +-- | positive p => positive <$> mk_app `` opow_pos [b, p] +-- | _ => failed +-- |-- We already know that `0 ≤ x` for all `x : ordinal` +-- _ => +-- failed +-- #align tactic.positivity_opow Tactic.positivity_opow + +-- end Tactic + +variable {α : Type u} {r : α → α → Prop} {a b : α} + +namespace Acc + +/-- The rank of an element `a` accessible under a relation `r` is defined inductively as the +smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that +`r b a`). -/ +noncomputable def rank (h : Acc r a) : Ordinal.{u} := + Acc.recOn h fun a _h ih => Ordinal.sup.{u, u} fun b : { b // r b a } => Order.succ <| ih b b.2 +#align acc.rank Acc.rank + +theorem rank_eq (h : Acc r a) : + h.rank = Ordinal.sup.{u, u} fun b : { b // r b a } => Order.succ (h.inv b.2).rank := by + change (Acc.intro a fun _ => h.inv).rank = _ + rfl +#align acc.rank_eq Acc.rank_eq + +/-- if `r a b` then the rank of `a` is less than the rank of `b`. -/ +theorem rank_lt_of_rel (hb : Acc r b) (h : r a b) : (hb.inv h).rank < hb.rank := + (Order.lt_succ _).trans_le <| by + rw [hb.rank_eq] + refine' le_trans _ (Ordinal.le_sup _ ⟨a, h⟩) + rfl +#align acc.rank_lt_of_rel Acc.rank_lt_of_rel + +end Acc + +namespace WellFounded + +variable (hwf : WellFounded r) + +/-- The rank of an element `a` under a well-founded relation `r` is defined inductively as the +smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that +`r b a`). -/ +noncomputable def rank (a : α) : Ordinal.{u} := + (hwf.apply a).rank +#align well_founded.rank WellFounded.rank + +theorem rank_eq : + hwf.rank a = Ordinal.sup.{u, u} fun b : { b // r b a } => Order.succ <| hwf.rank b := by + rw [rank, Acc.rank_eq] + rfl +#align well_founded.rank_eq WellFounded.rank_eq + +theorem rank_lt_of_rel (h : r a b) : hwf.rank a < hwf.rank b := + Acc.rank_lt_of_rel _ h +#align well_founded.rank_lt_of_rel WellFounded.rank_lt_of_rel + +theorem rank_strictMono [Preorder α] [WellFoundedLT α] : + StrictMono (rank <| @IsWellFounded.wf α (· < ·) _) := fun _ _ => rank_lt_of_rel _ +#align well_founded.rank_strict_mono WellFounded.rank_strictMono + +theorem rank_strictAnti [Preorder α] [WellFoundedGT α] : + StrictAnti (rank <| @IsWellFounded.wf α (· > ·) _) := fun _ _ => + rank_lt_of_rel <| @IsWellFounded.wf α (· > ·) _ +#align well_founded.rank_strict_anti WellFounded.rank_strictAnti + +end WellFounded From 6fa803ed895e75ed6bcd93a68e24e722fd24d295 Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Thu, 16 Feb 2023 18:14:41 +0000 Subject: [PATCH 12/14] feat: port CategoryTheory.Arrow (#2315) Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Arrow.lean | 337 ++++++++++++++++++++++++++++++ 2 files changed, 338 insertions(+) create mode 100644 Mathlib/CategoryTheory/Arrow.lean diff --git a/Mathlib.lean b/Mathlib.lean index 77fdddc8da43a..32883cab7d4bb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -218,6 +218,7 @@ import Mathlib.Algebra.Support import Mathlib.Algebra.Tropical.Basic import Mathlib.Algebra.Tropical.BigOperators import Mathlib.Algebra.Tropical.Lattice +import Mathlib.CategoryTheory.Arrow import Mathlib.CategoryTheory.Balanced import Mathlib.CategoryTheory.Bicategory.Basic import Mathlib.CategoryTheory.Bicategory.Strict diff --git a/Mathlib/CategoryTheory/Arrow.lean b/Mathlib/CategoryTheory/Arrow.lean new file mode 100644 index 0000000000000..475368b88c326 --- /dev/null +++ b/Mathlib/CategoryTheory/Arrow.lean @@ -0,0 +1,337 @@ +/- +Copyright (c) 2020 Markus Himmel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel + +! This file was ported from Lean 3 source module category_theory.arrow +! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.Comma + +/-! +# The category of arrows + +The category of arrows, with morphisms commutative squares. +We set this up as a specialization of the comma category `Comma L R`, +where `L` and `R` are both the identity functor. + +## Tags + +comma, arrow +-/ + + +namespace CategoryTheory + +universe v u + +-- morphism levels before object levels. See note [CategoryTheory universes]. +variable {T : Type u} [Category.{v} T] + +section + +variable (T) + +/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative + squares in `T`. -/ +def Arrow := + Comma.{v, v, v} (𝟭 T) (𝟭 T) +#align category_theory.arrow CategoryTheory.Arrow + +/- Porting note: could not derive `Category` above so this instance works in its place-/ +instance : Category (Arrow T) := commaCategory + +-- Satisfying the inhabited linter +instance Arrow.inhabited [Inhabited T] : Inhabited (Arrow T) + where default := show Comma (𝟭 T) (𝟭 T) from default +#align category_theory.arrow.inhabited CategoryTheory.Arrow.inhabited + +end + +namespace Arrow + +@[simp] +theorem id_left (f : Arrow T) : CommaMorphism.left (𝟙 f) = 𝟙 f.left := + rfl +#align category_theory.arrow.id_left CategoryTheory.Arrow.id_left + +@[simp] +theorem id_right (f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right := + rfl +#align category_theory.arrow.id_right CategoryTheory.Arrow.id_right + +/-- An object in the arrow category is simply a morphism in `T`. -/ +@[simps] +def mk {X Y : T} (f : X ⟶ Y) : Arrow T where + left := X + right := Y + hom := f +#align category_theory.arrow.mk CategoryTheory.Arrow.mk + +@[simp] +theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f := by + cases f + rfl +#align category_theory.arrow.mk_eq CategoryTheory.Arrow.mk_eq + +theorem mk_injective (A B : T) : Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => + by + cases h + rfl +#align category_theory.arrow.mk_injective CategoryTheory.Arrow.mk_injective + +theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g := + (mk_injective A B).eq_iff +#align category_theory.arrow.mk_inj CategoryTheory.Arrow.mk_inj + +/- Porting note : was marked as dangerous instance so changed from `Coe` to `CoeOut` -/ +instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where + coe := mk + +/-- A morphism in the arrow category is a commutative square connecting two objects of the arrow + category. -/ +@[simps] +def homMk {f g : Arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right} + (w : u ≫ g.hom = f.hom ≫ v) : f ⟶ g where + left := u + right := v + w := w +#align category_theory.arrow.hom_mk CategoryTheory.Arrow.homMk + +/-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/ +@[simps] +def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q} (w : u ≫ g = f ≫ v) : + Arrow.mk f ⟶ Arrow.mk g where + left := u + right := v + w := w +#align category_theory.arrow.hom_mk' CategoryTheory.Arrow.homMk' + +/- Porting note : was warned simp could prove reassoc'd version. Found simp could not. +Added nolint. -/ +@[reassoc (attr := simp, nolint simpNF)] +theorem w {f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := + sq.w +#align category_theory.arrow.w CategoryTheory.Arrow.w + +-- `w_mk_left` is not needed, as it is a consequence of `w` and `mk_hom`. +@[reassoc (attr := simp)] +theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) : + sq.left ≫ g = f.hom ≫ sq.right := + sq.w +#align category_theory.arrow.w_mk_right CategoryTheory.Arrow.w_mk_right + +theorem isIso_of_iso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left] + [IsIso ff.right] : IsIso ff where + out := by + let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩ + apply Exists.intro inverse + constructor + · apply CommaMorphism.ext + · rw [Comma.comp_left, IsIso.hom_inv_id, ←Comma.id_left] + · rw [Comma.comp_right, IsIso.hom_inv_id, ←Comma.id_right] + · apply CommaMorphism.ext + · rw [Comma.comp_left, IsIso.inv_hom_id, ←Comma.id_left] + · rw [Comma.comp_right, IsIso.inv_hom_id, ←Comma.id_right] +#align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right + +/-- Create an isomorphism between arrows, +by providing isomorphisms between the domains and codomains, +and a proof that the square commutes. -/ +@[simps!] +def isoMk {f g : Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right) + (h : l.hom ≫ g.hom = f.hom ≫ r.hom) : f ≅ g := + Comma.isoMk l r h +#align category_theory.arrow.iso_mk CategoryTheory.Arrow.isoMk + +/-- A variant of `Arrow.isoMk` that creates an iso between two `Arrow.mk`s with a better type +signature. -/ +abbrev isoMk' {W X Y Z : T} (f : W ⟶ X) (g : Y ⟶ Z) (e₁ : W ≅ Y) (e₂ : X ≅ Z) + (h : e₁.hom ≫ g = f ≫ e₂.hom) : Arrow.mk f ≅ Arrow.mk g := + Arrow.isoMk e₁ e₂ h +#align category_theory.arrow.iso_mk' CategoryTheory.Arrow.isoMk' + +theorem hom.congr_left {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left := by + rw [h] +#align category_theory.arrow.hom.congr_left CategoryTheory.Arrow.hom.congr_left + +@[simp] +theorem hom.congr_right {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right := by + rw [h] +#align category_theory.arrow.hom.congr_right CategoryTheory.Arrow.hom.congr_right + +theorem iso_w {f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right := by + have eq := Arrow.hom.congr_right e.inv_hom_id + dsimp at eq + erw [Arrow.w_assoc, ←Comma.comp_right, eq, Category.comp_id] +#align category_theory.arrow.iso_w CategoryTheory.Arrow.iso_w + +theorem iso_w' {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : + g = e.inv.left ≫ f ≫ e.hom.right := + iso_w e +#align category_theory.arrow.iso_w' CategoryTheory.Arrow.iso_w' + +section + +variable {f g : Arrow T} (sq : f ⟶ g) + +instance isIso_left [IsIso sq] : IsIso sq.left where + out := by + apply Exists.intro (inv sq).left + simp only [← Comma.comp_left, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_left, + eq_self_iff_true, and_self_iff] + simp +#align category_theory.arrow.is_iso_left CategoryTheory.Arrow.isIso_left + +instance isIso_right [IsIso sq] : IsIso sq.right where + out := by + apply Exists.intro (inv sq).right + simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_right, + eq_self_iff_true, and_self_iff] + simp +#align category_theory.arrow.is_iso_right CategoryTheory.Arrow.isIso_right + +@[simp] +theorem inv_left [IsIso sq] : (inv sq).left = inv sq.left := + IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_left, IsIso.hom_inv_id, id_left] +#align category_theory.arrow.inv_left CategoryTheory.Arrow.inv_left + +@[simp] +theorem inv_right [IsIso sq] : (inv sq).right = inv sq.right := + IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_right, IsIso.hom_inv_id, id_right] +#align category_theory.arrow.inv_right CategoryTheory.Arrow.inv_right + +/- Porting note : simp can prove this so removed @[simp] -/ +theorem left_hom_inv_right [IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom := by + simp only [← Category.assoc, IsIso.comp_inv_eq, w] +#align category_theory.arrow.left_hom_inv_right CategoryTheory.Arrow.left_hom_inv_right + +-- simp proves this +theorem inv_left_hom_right [IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.hom := by + simp only [w, IsIso.inv_comp_eq] +#align category_theory.arrow.inv_left_hom_right CategoryTheory.Arrow.inv_left_hom_right + +instance mono_left [Mono sq] : Mono sq.left where + right_cancellation {Z} φ ψ h := + by + let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ => + { left := φ + right := φ ≫ f.hom } + have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp + show (aux φ).left = (aux ψ).left + congr 1 + rw [← cancel_mono sq] + apply CommaMorphism.ext + · exact h + · rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc] + rw [←Arrow.w] + simp only [← Category.assoc, h] +#align category_theory.arrow.mono_left CategoryTheory.Arrow.mono_left + +instance epi_right [Epi sq] : Epi sq.right where + left_cancellation {Z} φ ψ h := by + let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ => + { right := φ + left := g.hom ≫ φ } + show (aux φ).right = (aux ψ).right + congr 1 + rw [← cancel_epi sq] + apply CommaMorphism.ext + · rw [Comma.comp_left, Comma.comp_left, Arrow.w_assoc, Arrow.w_assoc, h] + · exact h +#align category_theory.arrow.epi_right CategoryTheory.Arrow.epi_right + +end + +/-- Given a square from an arrow `i` to an isomorphism `p`, express the source part of `sq` +in terms of the inverse of `p`. -/ +@[simp] +theorem square_to_iso_invert (i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ Arrow.mk p.hom) : + i.hom ≫ sq.right ≫ p.inv = sq.left := by + simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm +#align category_theory.arrow.square_to_iso_invert CategoryTheory.Arrow.square_to_iso_invert + +/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq` +in terms of the inverse of `i`. -/ +theorem square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : Arrow.mk i.hom ⟶ p) : + i.inv ≫ sq.left ≫ p.hom = sq.right := by simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom] +#align category_theory.arrow.square_from_iso_invert CategoryTheory.Arrow.square_from_iso_invert + +variable {C : Type u} [Category.{v} C] + +/-- A helper construction: given a square between `i` and `f ≫ g`, produce a square between +`i` and `g`, whose top leg uses `f`: +A → X + ↓f +↓i Y --> A → Y + ↓g ↓i ↓g +B → Z B → Z + -/ +@[simps] +def squareToSnd {X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ Arrow.mk (f ≫ g)) : + i ⟶ Arrow.mk g where + left := sq.left ≫ f + right := sq.right +#align category_theory.arrow.square_to_snd CategoryTheory.Arrow.squareToSnd + +/-- The functor sending an arrow to its source. -/ +@[simps!] +def leftFunc : Arrow C ⥤ C := + Comma.fst _ _ +#align category_theory.arrow.left_func CategoryTheory.Arrow.leftFunc + +/-- The functor sending an arrow to its target. -/ +@[simps!] +def rightFunc : Arrow C ⥤ C := + Comma.snd _ _ +#align category_theory.arrow.right_func CategoryTheory.Arrow.rightFunc + +/-- The natural transformation from `leftFunc` to `rightFunc`, given by the arrow itself. -/ +@[simps] +def leftToRight : (leftFunc : Arrow C ⥤ C) ⟶ rightFunc where app f := f.hom +#align category_theory.arrow.left_to_right CategoryTheory.Arrow.leftToRight + +end Arrow + +namespace Functor + +universe v₁ v₂ u₁ u₂ + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +/-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/ +@[simps] +def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D + where + obj a := + { left := F.obj a.left + right := F.obj a.right + hom := F.map a.hom } + map f := + { left := F.map f.left + right := F.map f.right + w := by + let w := f.w + simp only [id_map] at w + dsimp + simp only [← F.map_comp, w] } + map_id := by aesop_cat + map_comp := fun f g => by + apply CommaMorphism.ext + · dsimp; rw [Comma.comp_left,F.map_comp]; rw [Comma.comp_left] + · dsimp; rw [Comma.comp_right,F.map_comp]; rw [Comma.comp_right] +#align category_theory.functor.map_arrow CategoryTheory.Functor.mapArrow + +end Functor + +/-- The images of `f : Arrow C` by two isomorphic functors `F : C ⥤ D` are +isomorphic arrows in `D`. -/ +def Arrow.isoOfNatIso {C D : Type _} [Category C] [Category D] {F G : C ⥤ D} (e : F ≅ G) + (f : Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f := + Arrow.isoMk (e.app f.left) (e.app f.right) (by simp) +#align category_theory.arrow.iso_of_nat_iso CategoryTheory.Arrow.isoOfNatIso + +end CategoryTheory +#lint From 7872193d1e0dcb1ce7393da890d987abbbba5a09 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Thu, 16 Feb 2023 19:50:35 +0000 Subject: [PATCH 13/14] fix: avoid sorryAx in library_search (#2304) Fixes #226, which is still reproducible. #239 was intended to fix it, but apparently plugged in the wrong bool value. Adds a new `assert_no_sorry` command and uses it in a new testcase. Also fixes up the "inj" and "noConfusionType" cases, which have the same bug. --- Mathlib.lean | 1 + Mathlib/Tactic/LibrarySearch.lean | 6 +++--- Mathlib/Util/AssertNoSorry.lean | 22 ++++++++++++++++++++++ test/librarySearch.lean | 11 +++++++++++ 4 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 Mathlib/Util/AssertNoSorry.lean diff --git a/Mathlib.lean b/Mathlib.lean index 32883cab7d4bb..1b810c4cb1e16 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1155,6 +1155,7 @@ import Mathlib.Topology.UniformSpace.Pi import Mathlib.Topology.UniformSpace.Separation import Mathlib.Topology.UniformSpace.UniformConvergence import Mathlib.Topology.UniformSpace.UniformEmbedding +import Mathlib.Util.AssertNoSorry import Mathlib.Util.AtomM import Mathlib.Util.Export import Mathlib.Util.IncludeStr diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean index 2c93d244e9b11..3fd5c078afbc0 100644 --- a/Mathlib/Tactic/LibrarySearch.lean +++ b/Mathlib/Tactic/LibrarySearch.lean @@ -31,9 +31,9 @@ initialize registerTraceClass `Tactic.librarySearch -- from Lean.Server.Completion private def isBlackListed (declName : Name) : MetaM Bool := do - if declName == ``sorryAx then return false - if declName matches .str _ "inj" then return false - if declName matches .str _ "noConfusionType" then return false + if declName == ``sorryAx then return true + if declName matches .str _ "inj" then return true + if declName matches .str _ "noConfusionType" then return true let env ← getEnv pure $ declName.isInternal || isAuxRecursor env declName diff --git a/Mathlib/Util/AssertNoSorry.lean b/Mathlib/Util/AssertNoSorry.lean new file mode 100644 index 0000000000000..dc740eeff0116 --- /dev/null +++ b/Mathlib/Util/AssertNoSorry.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2023 David Renshaw. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Renshaw +-/ + +import Lean.Elab.Print +import Lean.Environment + +/-! +# Defines the `assert_no_sorry` command. + +Throws an error if the given identifier uses sorryAx. +-/ + +/-- Throws an error if the given identifier uses sorryAx. -/ +elab "assert_no_sorry " n:ident : command => do + let env ← Lean.getEnv + let (_, s) := ((Lean.Elab.Command.CollectAxioms.collect + (← Lean.Elab.resolveGlobalConstNoOverloadWithInfo n)).run env).run {} + if s.axioms.contains ``sorryAx + then throwError "{n} contains sorry" diff --git a/test/librarySearch.lean b/test/librarySearch.lean index 344050ea17828..df2c0d2b37620 100644 --- a/test/librarySearch.lean +++ b/test/librarySearch.lean @@ -102,3 +102,14 @@ by library_search using P, Q -- exact P ∩ Q example (n : ℕ) (r : ℚ) : ℚ := by library_search using n, r -- exact nsmulRec n r + +-- Check that we don't use sorryAx: +-- (see https://github.com/leanprover-community/mathlib4/issues/226) + +theorem Bool_eq_iff {A B: Bool} : (A = B) = (A ↔ B) := + by (cases A <;> cases B <;> simp) + +theorem Bool_eq_iff2 {A B: Bool} : (A = B) = (A ↔ B) := + by library_search -- exact Bool_eq_iff + +assert_no_sorry Bool_eq_iff2 From 68e722a8873bff0e0780fe5bb8544cc2d533ab59 Mon Sep 17 00:00:00 2001 From: Pol_tta Date: Thu, 16 Feb 2023 23:48:55 +0000 Subject: [PATCH 14/14] refactor: semireducible Language (#2307) --- Mathlib/Computability/Language.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Mathlib/Computability/Language.lean b/Mathlib/Computability/Language.lean index c7dd49d1a24c4..cb2c005b7e0ba 100644 --- a/Mathlib/Computability/Language.lean +++ b/Mathlib/Computability/Language.lean @@ -44,7 +44,7 @@ namespace Language variable {l m : Language α} {a b x : List α} -- Porting note: `reducible` attribute cannot be local. -attribute [reducible] Language +-- attribute [local reducible] Language /-- Zero language has no elements. -/ instance : Zero (Language α) := @@ -59,7 +59,7 @@ instance : Inhabited (Language α) := /-- The sum of two languages is their union. -/ instance : Add (Language α) := - ⟨(· ∪ ·)⟩ + ⟨((· ∪ ·) : Set (List α) → Set (List α) → Set (List α))⟩ /-- The product of two languages `l` and `m` is the language made of the strings `x ++ y` where `x ∈ l` and `y ∈ m`. -/ @@ -70,11 +70,11 @@ theorem zero_def : (0 : Language α) = (∅ : Set _) := rfl #align language.zero_def Language.zero_def -theorem one_def : (1 : Language α) = {[]} := +theorem one_def : (1 : Language α) = ({[]} : Set (List α)) := rfl #align language.one_def Language.one_def -theorem add_def (l m : Language α) : l + m = l ∪ m := +theorem add_def (l m : Language α) : l + m = (l ∪ m : Set (List α)) := rfl #align language.add_def Language.add_def @@ -90,6 +90,12 @@ lemma kstar_def (l : Language α) : l∗ = {x | ∃ L : List (List α), x = L.jo rfl #align language.kstar_def Language.kstar_def +-- Porting note: `reducible` attribute cannot be local, +-- so this new theorem is required in place of `Set.ext`. +@[ext] +theorem ext {l m : Language α} (h : ∀ (x : List α), x ∈ l ↔ x ∈ m) : l = m := + Set.ext h + @[simp] theorem not_mem_zero (x : List α) : x ∉ (0 : Language α) := id