Grace/Cumulus/Set/Ordinal/Monotone.g17

Open in Workbench Download source

Imports

Arithmetic

Declarations

Source

1-- Ordinal arithmetic is monotone and continuous in the right argument:2-- limit membership for products and powers, strict and inclusive3-- monotonicity, limits stay limits, and cancellation4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Set.Ordinal.Monotone10import Arithmetic1112-- Limit stages of products and powers1314theorem ordinalMul.limit_membership (x : Set, α λ : Ordinal)15  requires limit : Limit(λ)16  shows x ∈ α * λ ↔ ∃ β ∈ λ, x ∈ ordinalMul(α, β)17proof18  have equation := ordinalMul.limit at α, λ with limit19  rw equation20  constructor21  . intro hx22    simp [set.union] at hx23    obtain ⟨stage, hStage, hxStage⟩ := hx24    obtain ⟨β, hβ, shape⟩ := ordinalMul.history_range.forward with hStage25    witness β26    constructor27    . exact hβ28    . rw ← shape29      exact hxStage30  . intro h31    obtain ⟨β, hβ, hx⟩ := h32    have inRange : ordinalMul(α, β) ∈ Relation.range(ordinalMul.history(α, λ))33      apply ordinalMul.history_range.backward34      exact ⟨β, hβ, rfl⟩35    exact union.contains with inRange, hx3637theorem ordinalPow.limit_membership (x : Set, α λ : Ordinal)38  requires limit : Limit(λ)39  shows x ∈ α ^ λ ↔ ∃ β ∈ λ, x ∈ ordinalPow(α, β)40proof41  have equation := ordinalPow.limit at α, λ with limit42  rw equation43  constructor44  . intro hx45    simp [set.union] at hx46    obtain ⟨stage, hStage, hxStage⟩ := hx47    obtain ⟨β, hβ, shape⟩ := ordinalPow.history_range.forward with hStage48    witness β49    constructor50    . exact hβ51    . rw ← shape52      exact hxStage53  . intro h54    obtain ⟨β, hβ, hx⟩ := h55    have inRange : ordinalPow(α, β) ∈ Relation.range(ordinalPow.history(α, λ))56      apply ordinalPow.history_range.backward57      exact ⟨β, hβ, rfl⟩58    exact union.contains with inRange, hx5960-- A nonzero ordinal contains zero.61theorem Ordinal.zero_member (α : Ordinal)62  requires nonzero : α ≠ ∅63  shows ∅ ∈ α64proof65  have αOrdinal : α ∈ Ordinal by assumption66  have cases := Ordinal.trichotomy at ∅ with Ordinal.empty, α, αOrdinal67  cases cases with member | rest68  . exact member69  . cases rest with equal | below70    . exfalso71      apply nonzero72      symm73      exact equal74    . exfalso75      exact set.empty with below7677-- Addition7879theorem ordinalAdd.subset_monotone (α β γ : Ordinal)80  requires h : β ⊆ γ81  shows α + β ⊆ α + γ82proof83  have βOrdinal : β ∈ Ordinal by assumption84  have γOrdinal : γ ∈ Ordinal by assumption85  have below := Ordinal.subset_iff_member_next.forward86    with βOrdinal, γOrdinal, h87  have nextOrdinal := Ordinal.next with γOrdinal88  have step := ordinalAdd.monotone at α, β, next(γ) with nextOrdinal, below89  rw ordinalAdd.next at step90  have sumβ := ordinalAdd.ordinal at α, β with βOrdinal91  have sumγ := ordinalAdd.ordinal at α, γ with γOrdinal92  exact Ordinal.subset_iff_member_next.backward with sumβ, sumγ, step9394theorem ordinalAdd.subset_right (α : Ordinal, β : Set)95  shows β ∈ Ordinal → β ⊆ α + β96proof97  induction β using membership98  intros current ih hCurrent99  have cases := Ordinal.cases with hCurrent100  cases cases with zero | rest101  . rw zero102    exact empty.subset103  . cases rest with successor | limit104    . obtain ⟨γ, hγ, shape⟩ := successor105      rw ← shape106      have γOrdinal := Ordinal.member with hCurrent, hγ107      have step := ih with hγ, γOrdinal108      rw ordinalAdd.next109      have sumOrdinal := ordinalAdd.ordinal at α, γ with γOrdinal110      have bound := Ordinal.subset_bound with γOrdinal, sumOrdinal, step111      intros x hx112      simp [next.membership] at hx113      apply next.membership.backward114      cases hx with earlier | equal115      . left116        exact step with x, earlier117      . rw equal118        simp [next.membership] at bound119        exact bound120    . intros x hx121      apply ordinalAdd.limit_membership.backward at x, α, current with limit122      have xOrdinal := Ordinal.member with hCurrent, hx123      have nextIn := limit.right.right with x, hx124      witness next(x)125      constructor126      . exact nextIn127      . have step := ih with hx, xOrdinal128        have sumOrdinal := ordinalAdd.ordinal at α, x with xOrdinal129        rw ordinalAdd.next130        exact Ordinal.subset_bound with xOrdinal, sumOrdinal, step131132theorem ordinalAdd.limit_right (α λ : Ordinal)133  requires limit : Limit(λ)134  shows Limit(α + λ)135proof136  have λOrdinal : λ ∈ Ordinal by assumption137  have sumOrdinal := ordinalAdd.ordinal at α, λ with λOrdinal138  constructor139  . exact sumOrdinal140  . constructor141    . intro equal142      have zeroIn := Ordinal.zero_member with limit.right.left143      have member := ordinalAdd.monotone at α, ∅, λ with λOrdinal, zeroIn144      rw equal at member145      exact set.empty with member146    . intros x hx147      obtain ⟨β, hβ, hxβ⟩ := ordinalAdd.limit_membership.forward at x, α, λ148        with limit, hx149      have βOrdinal := Ordinal.member with λOrdinal, hβ150      have stageOrdinal := ordinalAdd.ordinal at α, β with βOrdinal151      have xOrdinal := Ordinal.member with stageOrdinal, hxβ152      apply ordinalAdd.limit_membership.backward at next(x), α, λ with limit153      witness next(β)154      constructor155      . exact limit.right.right with β, hβ156      . rw ordinalAdd.next157        exact next.member_iff.backward with xOrdinal, stageOrdinal, hxβ158159theorem ordinalAdd.cancel (α β γ : Ordinal)160  requires equal : α + β = α + γ161  shows β = γ162proof163  have βOrdinal : β ∈ Ordinal by assumption164  have γOrdinal : γ ∈ Ordinal by assumption165  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal166  cases cases with below | rest167  . exfalso168    have member := ordinalAdd.monotone at α, β, γ with γOrdinal, below169    rw ← equal at member170    exact Ordinal.not_member_self with member171  . cases rest with same | above172    . exact same173    . exfalso174      have member := ordinalAdd.monotone at α, γ, β with βOrdinal, above175      rw equal at member176      exact Ordinal.not_member_self with member177178theorem next.monotone (α β : Ordinal)179  requires h : α ⊆ β180  shows next(α) ⊆ next(β)181proof182  have αOrdinal : α ∈ Ordinal by assumption183  have βOrdinal : β ∈ Ordinal by assumption184  have member := Ordinal.subset_bound with αOrdinal, βOrdinal, h185  exact Ordinal.member_iff_next_subset.forward with186    αOrdinal, (Ordinal.next with βOrdinal), member187188theorem ordinalAdd.member_right (α β : Ordinal)189  requires positive : ∅ ∈ β190  shows α ∈ α + β191proof192  have βOrdinal : β ∈ Ordinal by assumption193  have grows := ordinalAdd.monotone at α, ∅, β with βOrdinal, positive194  rw ← nat.zero at grows195  rw ordinalAdd.zero at grows196  exact grows197198-- Multiplication199200theorem ordinalMul.zero_left (β : Set)201  shows β ∈ Ordinal → ordinalMul(0, β) = 0202proof203  induction β using membership204  intros current ih hCurrent205  have cases := Ordinal.cases with hCurrent206  cases cases with zero | rest207  . rw zero208    have base := ordinalMul.zero at 0209    rw ← nat.zero210    rw base211    symm212    exact nat.zero213  . cases rest with successor | limit214    . obtain ⟨γ, hγ, shape⟩ := successor215      rw ← shape216      have γOrdinal := Ordinal.member with hCurrent, hγ217      have step := ih with hγ, γOrdinal218      rw [ordinalMul.next, step]219      exact ordinalAdd.zero at 0220    . apply Subset.antisymmetric221      . intros x hx222        obtain ⟨stage, hStage, hxStage⟩ :=223          ordinalMul.limit_membership.forward at x, 0, current with limit, hx224        have step := ih with hStage, (Ordinal.member with hCurrent, hStage)225        rw [step, nat.zero] at hxStage226        exfalso227        exact set.empty with hxStage228      . rw nat.zero229        exact empty.subset230231theorem ordinalMul.subset_monotone (α β : Ordinal, γ : Set)232  shows γ ∈ Ordinal → β ∈ γ → α * β ⊆ α * γ233proof234  induction γ using membership235  intros current ih hCurrent hBelow236  have cases := Ordinal.cases with hCurrent237  cases cases with zero | rest238  . exfalso239    rw zero at hBelow240    exact set.empty at β with hBelow241  . cases rest with successor | limit242    . obtain ⟨δ, hδ, shape⟩ := successor243      rw ← shape244      have δOrdinal := Ordinal.member with hCurrent, hδ245      have αOrdinal : α ∈ Ordinal by assumption246      have productOrdinal := ordinalMul.ordinal at α, δ with δOrdinal247      have included := ordinalAdd.subset_left at α * δ, α with αOrdinal248      rw ordinalMul.next249      rw ← shape at hBelow250      simp [next.membership] at hBelow251      cases hBelow with earlier | equal252      . have step := ih with hδ, δOrdinal, earlier253        exact Subset.transitive with step, included254      . rw equal255        exact included256    . intros x hx257      apply ordinalMul.limit_membership.backward at x, α, current with limit258      witness β259      constructor260      . exact hBelow261      . exact hx262263theorem ordinalMul.subset_monotone_of_subset (α β γ : Ordinal)264  requires h : β ⊆ γ265  shows α * β ⊆ α * γ266proof267  have βOrdinal : β ∈ Ordinal by assumption268  have γOrdinal : γ ∈ Ordinal by assumption269  have below := Ordinal.subset_iff_member_next.forward270    with βOrdinal, γOrdinal, h271  simp [next.membership] at below272  cases below with earlier | equal273  . exact ordinalMul.subset_monotone at α, β, γ with γOrdinal, earlier274  . rw equal275    exact Subset.reflexive276277theorem Ordinal.one_subset (α : Ordinal)278  requires positive : ∅ ∈ α279  shows 1 ⊆ α280proof281  have αOrdinal : α ∈ Ordinal by assumption282  have one : 1 = next(0) by simp [next.natural]283  rw [one, nat.zero]284  exact Ordinal.member_iff_next_subset.forward285    with Ordinal.empty, αOrdinal, positive286287theorem Ordinal.zero_member_one288  shows ∅ ∈ 1289proof290  have one : 1 = next(0) by simp [next.natural]291  rw [one, nat.zero]292  exact next.contains at ∅293294theorem Ordinal.zero_member_of_one (α : Ordinal)295  requires above : 1 ∈ α296  shows ∅ ∈ α297proof298  have αOrdinal : α ∈ Ordinal by assumption299  have included := Ordinal.member_subset with αOrdinal, above300  exact included with ∅, Ordinal.zero_member_one301302theorem ordinalMul.subset_left_factor (α β : Ordinal)303  requires positive : ∅ ∈ β304  shows α ⊆ α * β305proof306  have oneIn := Ordinal.one_subset with positive307  have grows := ordinalMul.subset_monotone_of_subset at α, 1, β with oneIn308  rw ordinalMul.one at grows309  exact grows310311theorem ordinalMul.monotone (α β : Ordinal, γ : Set)312  requires positive : ∅ ∈ α313  shows γ ∈ Ordinal → β ∈ γ → α * β ∈ α * γ314proof315  induction γ using membership316  intros current ih hCurrent hBelow317  have cases := Ordinal.cases with hCurrent318  cases cases with zero | rest319  . exfalso320    rw zero at hBelow321    exact set.empty at β with hBelow322  . cases rest with successor | limit323    . obtain ⟨δ, hδ, shape⟩ := successor324      rw ← shape325      have δOrdinal := Ordinal.member with hCurrent, hδ326      have productOrdinal := ordinalMul.ordinal at α, δ with δOrdinal327      have grows := ordinalAdd.member_right at α * δ, α with positive328      rw ordinalMul.next329      rw ← shape at hBelow330      simp [next.membership] at hBelow331      cases hBelow with earlier | equal332      . have step := ih with hδ, δOrdinal, earlier333        have αOrdinal : α ∈ Ordinal by assumption334        have included := ordinalAdd.subset_left at α * δ, α with αOrdinal335        exact included with α * β, step336      . rw equal337        exact grows338    . apply ordinalMul.limit_membership.backward at α * β, α, current with limit339      witness next(β)340      constructor341      . exact limit.right.right with β, hBelow342      . rw ordinalMul.next343        have βOrdinal : β ∈ Ordinal by assumption344        have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal345        exact ordinalAdd.member_right at α * β, α with positive346347theorem ordinalMul.member_right (α β : Ordinal)348  requires positive : ∅ ∈ α349  requires above : 1 ∈ β350  shows α ∈ α * β351proof352  have βOrdinal : β ∈ Ordinal by assumption353  have grows := ordinalMul.monotone at α, 1, β with positive, βOrdinal, above354  rw ordinalMul.one at grows355  exact grows356357theorem ordinalMul.limit_right (α λ : Ordinal)358  requires positive : ∅ ∈ α359  requires limit : Limit(λ)360  shows Limit(α * λ)361proof362  have λOrdinal : λ ∈ Ordinal by assumption363  have productOrdinal := ordinalMul.ordinal at α, λ with λOrdinal364  constructor365  . exact productOrdinal366  . constructor367    . intro equal368      have zeroIn := Ordinal.zero_member with limit.right.left369      have member := ordinalMul.monotone at α, ∅, λ370        with positive, λOrdinal, zeroIn371      rw equal at member372      exact set.empty with member373    . intros x hx374      obtain ⟨β, hβ, hxβ⟩ :=375        ordinalMul.limit_membership.forward at x, α, λ with limit, hx376      have βOrdinal := Ordinal.member with λOrdinal, hβ377      have stageOrdinal := ordinalMul.ordinal at α, β with βOrdinal378      have xOrdinal := Ordinal.member with stageOrdinal, hxβ379      have αOrdinal : α ∈ Ordinal by assumption380      have sumOrdinal := ordinalAdd.ordinal at α * β, α with αOrdinal381      apply ordinalMul.limit_membership.backward at next(x), α, λ with limit382      witness next(β)383      constructor384      . exact limit.right.right with β, hβ385      . rw ordinalMul.next386        have grows := ordinalAdd.member_right at α * β, α with positive387        have included := Ordinal.member_iff_next_subset.forward with388          stageOrdinal, sumOrdinal, grows389        have step := next.member_iff.backward with xOrdinal, stageOrdinal, hxβ390        exact included with next(x), step391392theorem ordinalMul.subset_right (α : Ordinal, β : Set)393  requires positive : ∅ ∈ α394  shows β ∈ Ordinal → β ⊆ α * β395proof396  induction β using membership397  intros current ih hCurrent398  have cases := Ordinal.cases with hCurrent399  cases cases with zero | rest400  . rw zero401    exact empty.subset402  . cases rest with successor | limit403    . obtain ⟨γ, hγ, shape⟩ := successor404      rw ← shape405      have γOrdinal := Ordinal.member with hCurrent, hγ406      have step := ih with hγ, γOrdinal407      have productOrdinal := ordinalMul.ordinal at α, γ with γOrdinal408      have αOrdinal : α ∈ Ordinal by assumption409      have sumOrdinal := ordinalAdd.ordinal at α * γ, α with αOrdinal410      rw ordinalMul.next411      have first := next.monotone at γ, α * γ with step412      have grows := ordinalAdd.member_right at α * γ, α with positive413      have second := Ordinal.member_iff_next_subset.forward with414        productOrdinal, sumOrdinal, grows415      exact Subset.transitive with first, second416    . intros x hx417      apply ordinalMul.limit_membership.backward at x, α, current with limit418      have xOrdinal := Ordinal.member with hCurrent, hx419      have nextIn := limit.right.right with x, hx420      witness next(x)421      constructor422      . exact nextIn423      . have step := ih with hx, xOrdinal424        have productOrdinal := ordinalMul.ordinal at α, x with xOrdinal425        have αOrdinal : α ∈ Ordinal by assumption426        have sumOrdinal := ordinalAdd.ordinal at α * x, α with αOrdinal427        rw ordinalMul.next428        have grows := ordinalAdd.member_right at α * x, α with positive429        have included := Ordinal.member_iff_next_subset.forward with430          productOrdinal, sumOrdinal, grows431        have member := Ordinal.subset_bound with xOrdinal, productOrdinal, step432        exact included with x, member433434theorem ordinalMul.cancel (α β γ : Ordinal)435  requires positive : ∅ ∈ α436  requires equal : α * β = α * γ437  shows β = γ438proof439  have βOrdinal : β ∈ Ordinal by assumption440  have γOrdinal : γ ∈ Ordinal by assumption441  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal442  cases cases with below | rest443  . exfalso444    have member := ordinalMul.monotone at α, β, γ with positive, γOrdinal, below445    rw ← equal at member446    exact Ordinal.not_member_self with member447  . cases rest with same | above448    . exact same449    . exfalso450      have member := ordinalMul.monotone at α, γ, β451        with positive, βOrdinal, above452      rw equal at member453      exact Ordinal.not_member_self with member454455-- Exponentiation456457theorem ordinalPow.positive (α : Ordinal, β : Set)458  requires positive : ∅ ∈ α459  shows β ∈ Ordinal → ∅ ∈ α ^ β460proof461  induction β using membership462  intros current ih hCurrent463  have cases := Ordinal.cases with hCurrent464  cases cases with zero | rest465  . rw zero466    have base := ordinalPow.zero at α467    rw nat.zero at base468    rw base469    exact Ordinal.zero_member_one470  . cases rest with successor | limit471    . obtain ⟨γ, hγ, shape⟩ := successor472      rw ← shape473      have γOrdinal := Ordinal.member with hCurrent, hγ474      have step := ih with hγ, γOrdinal475      have powerOrdinal := ordinalPow.ordinal at α, γ with γOrdinal476      have αOrdinal : α ∈ Ordinal by assumption477      rw ordinalPow.next478      have grows := ordinalMul.monotone at α ^ γ, ∅, α479        with step, αOrdinal, positive480      rw ← nat.zero at grows481      rw ordinalMul.zero at grows482      exact grows483    . apply ordinalPow.limit_membership.backward at ∅, α, current with limit484      witness ∅485      constructor486      . exact Ordinal.zero_member with limit.right.left487      . have base := ordinalPow.zero at α488        rw nat.zero at base489        rw base490        exact Ordinal.zero_member_one491492theorem ordinalPow.subset_monotone (α β : Ordinal, γ : Set)493  requires positive : ∅ ∈ α494  shows γ ∈ Ordinal → β ∈ γ → α ^ β ⊆ α ^ γ495proof496  induction γ using membership497  intros current ih hCurrent hBelow498  have cases := Ordinal.cases with hCurrent499  cases cases with zero | rest500  . exfalso501    rw zero at hBelow502    exact set.empty at β with hBelow503  . cases rest with successor | limit504    . obtain ⟨δ, hδ, shape⟩ := successor505      rw ← shape506      have δOrdinal := Ordinal.member with hCurrent, hδ507      have powerOrdinal := ordinalPow.ordinal at α, δ with δOrdinal508      have included := ordinalMul.subset_left_factor at α ^ δ, α with positive509      rw ordinalPow.next510      rw ← shape at hBelow511      simp [next.membership] at hBelow512      cases hBelow with earlier | equal513      . have step := ih with hδ, δOrdinal, earlier514        exact Subset.transitive with step, included515      . rw equal516        exact included517    . intros x hx518      apply ordinalPow.limit_membership.backward at x, α, current with limit519      witness β520      constructor521      . exact hBelow522      . exact hx523524theorem ordinalPow.monotone (α β : Ordinal, γ : Set)525  requires above : 1 ∈ α526  shows γ ∈ Ordinal → β ∈ γ → α ^ β ∈ α ^ γ527proof528  induction γ using membership529  intros current ih hCurrent hBelow530  have positive := Ordinal.zero_member_of_one with above531  have cases := Ordinal.cases with hCurrent532  cases cases with zero | rest533  . exfalso534    rw zero at hBelow535    exact set.empty at β with hBelow536  . cases rest with successor | limit537    . obtain ⟨δ, hδ, shape⟩ := successor538      rw ← shape539      have δOrdinal := Ordinal.member with hCurrent, hδ540      have powerOrdinal := ordinalPow.ordinal at α, δ with δOrdinal541      have basePositive := ordinalPow.positive at α, δ with positive, δOrdinal542      have grows := ordinalMul.member_right at α ^ δ, α with basePositive, above543      rw ordinalPow.next544      rw ← shape at hBelow545      simp [next.membership] at hBelow546      cases hBelow with earlier | equal547      . have step := ih with hδ, δOrdinal, earlier548        have included := ordinalMul.subset_left_factor at α ^ δ, α with positive549        exact included with α ^ β, step550      . rw equal551        exact grows552    . apply ordinalPow.limit_membership.backward at α ^ β, α, current with limit553      witness next(β)554      constructor555      . exact limit.right.right with β, hBelow556      . rw ordinalPow.next557        have βOrdinal : β ∈ Ordinal by assumption558        have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal559        have basePositive := ordinalPow.positive at α, β with positive, βOrdinal560        exact ordinalMul.member_right at α ^ β, α with basePositive, above561562theorem ordinalPow.limit_right (α λ : Ordinal)563  requires above : 1 ∈ α564  requires limit : Limit(λ)565  shows Limit(α ^ λ)566proof567  have λOrdinal : λ ∈ Ordinal by assumption568  have positive := Ordinal.zero_member_of_one with above569  have powerOrdinal := ordinalPow.ordinal at α, λ with λOrdinal570  constructor571  . exact powerOrdinal572  . constructor573    . intro equal574      have member := ordinalPow.positive at α, λ with positive, λOrdinal575      rw equal at member576      exact set.empty with member577    . intros x hx578      obtain ⟨β, hβ, hxβ⟩ :=579        ordinalPow.limit_membership.forward at x, α, λ with limit, hx580      have βOrdinal := Ordinal.member with λOrdinal, hβ581      have stageOrdinal := ordinalPow.ordinal at α, β with βOrdinal582      have xOrdinal := Ordinal.member with stageOrdinal, hxβ583      have αOrdinal : α ∈ Ordinal by assumption584      have productOrdinal := ordinalMul.ordinal at α ^ β, α with αOrdinal585      have basePositive := ordinalPow.positive at α, β with positive, βOrdinal586      apply ordinalPow.limit_membership.backward at next(x), α, λ with limit587      witness next(β)588      constructor589      . exact limit.right.right with β, hβ590      . rw ordinalPow.next591        have grows := ordinalMul.member_right at α ^ β, α592          with basePositive, above593        have included := Ordinal.member_iff_next_subset.forward with594          stageOrdinal, productOrdinal, grows595        have step := next.member_iff.backward with xOrdinal, stageOrdinal, hxβ596        exact included with next(x), step597598theorem ordinalPow.subset_right (α : Ordinal, β : Set)599  requires above : 1 ∈ α600  shows β ∈ Ordinal → β ⊆ α ^ β601proof602  induction β using membership603  intros current ih hCurrent604  have positive := Ordinal.zero_member_of_one with above605  have αOrdinal : α ∈ Ordinal by assumption606  have cases := Ordinal.cases with hCurrent607  cases cases with zero | rest608  . rw zero609    exact empty.subset610  . cases rest with successor | limit611    . obtain ⟨γ, hγ, shape⟩ := successor612      rw ← shape613      have γOrdinal := Ordinal.member with hCurrent, hγ614      have step := ih with hγ, γOrdinal615      have powerOrdinal := ordinalPow.ordinal at α, γ with γOrdinal616      have productOrdinal := ordinalMul.ordinal at α ^ γ, α with αOrdinal617      have basePositive := ordinalPow.positive at α, γ with positive, γOrdinal618      rw ordinalPow.next619      have first := next.monotone at γ, α ^ γ with step620      have grows := ordinalMul.member_right at α ^ γ, α with basePositive, above621      have second := Ordinal.member_iff_next_subset.forward with622        powerOrdinal, productOrdinal, grows623      exact Subset.transitive with first, second624    . intros x hx625      apply ordinalPow.limit_membership.backward at x, α, current with limit626      have xOrdinal := Ordinal.member with hCurrent, hx627      have nextIn := limit.right.right with x, hx628      witness next(x)629      constructor630      . exact nextIn631      . have step := ih with hx, xOrdinal632        have powerOrdinal := ordinalPow.ordinal at α, x with xOrdinal633        have productOrdinal := ordinalMul.ordinal at α ^ x, α with αOrdinal634        have basePositive := ordinalPow.positive at α, x with positive, xOrdinal635        rw ordinalPow.next636        have grows := ordinalMul.member_right at α ^ x, α637          with basePositive, above638        have included := Ordinal.member_iff_next_subset.forward with639          powerOrdinal, productOrdinal, grows640        have member := Ordinal.subset_bound with xOrdinal, powerOrdinal, step641        exact included with x, member642643theorem ordinalPow.cancel (α β γ : Ordinal)644  requires above : 1 ∈ α645  requires equal : α ^ β = α ^ γ646  shows β = γ647proof648  have βOrdinal : β ∈ Ordinal by assumption649  have γOrdinal : γ ∈ Ordinal by assumption650  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal651  cases cases with below | rest652  . exfalso653    have member := ordinalPow.monotone at α, β, γ with above, γOrdinal, below654    rw ← equal at member655    exact Ordinal.not_member_self with member656  . cases rest with same | above2657    . exact same658    . exfalso659      have member := ordinalPow.monotone at α, γ, β with above, βOrdinal, above2660      rw equal at member661      exact Ordinal.not_member_self with member662663-- Every ordinal is zero, a successor, or a limit.664theorem Ordinal.zero_successor_or_limit (α : Ordinal)665  shows α = 0 ∨ (∃ β, β ∈ Ordinal ∧ α = next(β)) ∨ Limit(α)666proof667  have αOrdinal : α ∈ Ordinal by assumption668  have cases := Ordinal.cases with αOrdinal669  cases cases with zero | rest670  . left671    rw nat.zero672    exact zero673  . cases rest with successor | limit674    . right675      left676      obtain ⟨β, hβ, shape⟩ := successor677      witness β678      constructor679      . exact Ordinal.member with αOrdinal, hβ680      . symm681        exact shape682    . right683      right684      exact limit685