-- Ordinal arithmetic is monotone and continuous in the right argument:
-- limit membership for products and powers, strict and inclusive
-- monotonicity, limits stay limits, and cancellation
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Ordinal.Monotone
import Arithmetic

-- Limit stages of products and powers

theorem ordinalMul.limit_membership (x : Set, α λ : Ordinal)
  requires limit : Limit(λ)
  shows x ∈ α * λ ↔ ∃ β ∈ λ, x ∈ ordinalMul(α, β)
proof
  have equation := ordinalMul.limit at α, λ with limit
  rw equation
  constructor
  . intro hx
    simp [set.union] at hx
    obtain ⟨stage, hStage, hxStage⟩ := hx
    obtain ⟨β, hβ, shape⟩ := ordinalMul.history_range.forward with hStage
    witness β
    constructor
    . exact hβ
    . rw ← shape
      exact hxStage
  . intro h
    obtain ⟨β, hβ, hx⟩ := h
    have inRange : ordinalMul(α, β) ∈ Relation.range(ordinalMul.history(α, λ))
      apply ordinalMul.history_range.backward
      exact ⟨β, hβ, rfl⟩
    exact union.contains with inRange, hx

theorem ordinalPow.limit_membership (x : Set, α λ : Ordinal)
  requires limit : Limit(λ)
  shows x ∈ α ^ λ ↔ ∃ β ∈ λ, x ∈ ordinalPow(α, β)
proof
  have equation := ordinalPow.limit at α, λ with limit
  rw equation
  constructor
  . intro hx
    simp [set.union] at hx
    obtain ⟨stage, hStage, hxStage⟩ := hx
    obtain ⟨β, hβ, shape⟩ := ordinalPow.history_range.forward with hStage
    witness β
    constructor
    . exact hβ
    . rw ← shape
      exact hxStage
  . intro h
    obtain ⟨β, hβ, hx⟩ := h
    have inRange : ordinalPow(α, β) ∈ Relation.range(ordinalPow.history(α, λ))
      apply ordinalPow.history_range.backward
      exact ⟨β, hβ, rfl⟩
    exact union.contains with inRange, hx

-- A nonzero ordinal contains zero.
theorem Ordinal.zero_member (α : Ordinal)
  requires nonzero : α ≠ ∅
  shows ∅ ∈ α
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have cases := Ordinal.trichotomy at ∅ with Ordinal.empty, α, αOrdinal
  cases cases with member | rest
  . exact member
  . cases rest with equal | below
    . exfalso
      apply nonzero
      symm
      exact equal
    . exfalso
      exact set.empty with below

-- Addition

theorem ordinalAdd.subset_monotone (α β γ : Ordinal)
  requires h : β ⊆ γ
  shows α + β ⊆ α + γ
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have γOrdinal : γ ∈ Ordinal by assumption
  have below := Ordinal.subset_iff_member_next.forward
    with βOrdinal, γOrdinal, h
  have nextOrdinal := Ordinal.next with γOrdinal
  have step := ordinalAdd.monotone at α, β, next(γ) with nextOrdinal, below
  rw ordinalAdd.next at step
  have sumβ := ordinalAdd.ordinal at α, β with βOrdinal
  have sumγ := ordinalAdd.ordinal at α, γ with γOrdinal
  exact Ordinal.subset_iff_member_next.backward with sumβ, sumγ, step

theorem ordinalAdd.subset_right (α : Ordinal, β : Set)
  shows β ∈ Ordinal → β ⊆ α + β
proof
  induction β using membership
  intros current ih hCurrent
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    exact empty.subset
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      rw ordinalAdd.next
      have sumOrdinal := ordinalAdd.ordinal at α, γ with γOrdinal
      have bound := Ordinal.subset_bound with γOrdinal, sumOrdinal, step
      intros x hx
      simp [next.membership] at hx
      apply next.membership.backward
      cases hx with earlier | equal
      . left
        exact step with x, earlier
      . rw equal
        simp [next.membership] at bound
        exact bound
    . intros x hx
      apply ordinalAdd.limit_membership.backward at x, α, current with limit
      have xOrdinal := Ordinal.member with hCurrent, hx
      have nextIn := limit.right.right with x, hx
      witness next(x)
      constructor
      . exact nextIn
      . have step := ih with hx, xOrdinal
        have sumOrdinal := ordinalAdd.ordinal at α, x with xOrdinal
        rw ordinalAdd.next
        exact Ordinal.subset_bound with xOrdinal, sumOrdinal, step

theorem ordinalAdd.limit_right (α λ : Ordinal)
  requires limit : Limit(λ)
  shows Limit(α + λ)
proof
  have λOrdinal : λ ∈ Ordinal by assumption
  have sumOrdinal := ordinalAdd.ordinal at α, λ with λOrdinal
  constructor
  . exact sumOrdinal
  . constructor
    . intro equal
      have zeroIn := Ordinal.zero_member with limit.right.left
      have member := ordinalAdd.monotone at α, ∅, λ with λOrdinal, zeroIn
      rw equal at member
      exact set.empty with member
    . intros x hx
      obtain ⟨β, hβ, hxβ⟩ := ordinalAdd.limit_membership.forward at x, α, λ
        with limit, hx
      have βOrdinal := Ordinal.member with λOrdinal, hβ
      have stageOrdinal := ordinalAdd.ordinal at α, β with βOrdinal
      have xOrdinal := Ordinal.member with stageOrdinal, hxβ
      apply ordinalAdd.limit_membership.backward at next(x), α, λ with limit
      witness next(β)
      constructor
      . exact limit.right.right with β, hβ
      . rw ordinalAdd.next
        exact next.member_iff.backward with xOrdinal, stageOrdinal, hxβ

theorem ordinalAdd.cancel (α β γ : Ordinal)
  requires equal : α + β = α + γ
  shows β = γ
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have γOrdinal : γ ∈ Ordinal by assumption
  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal
  cases cases with below | rest
  . exfalso
    have member := ordinalAdd.monotone at α, β, γ with γOrdinal, below
    rw ← equal at member
    exact Ordinal.not_member_self with member
  . cases rest with same | above
    . exact same
    . exfalso
      have member := ordinalAdd.monotone at α, γ, β with βOrdinal, above
      rw equal at member
      exact Ordinal.not_member_self with member

theorem next.monotone (α β : Ordinal)
  requires h : α ⊆ β
  shows next(α) ⊆ next(β)
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have βOrdinal : β ∈ Ordinal by assumption
  have member := Ordinal.subset_bound with αOrdinal, βOrdinal, h
  exact Ordinal.member_iff_next_subset.forward with
    αOrdinal, (Ordinal.next with βOrdinal), member

theorem ordinalAdd.member_right (α β : Ordinal)
  requires positive : ∅ ∈ β
  shows α ∈ α + β
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have grows := ordinalAdd.monotone at α, ∅, β with βOrdinal, positive
  rw ← nat.zero at grows
  rw ordinalAdd.zero at grows
  exact grows

-- Multiplication

theorem ordinalMul.zero_left (β : Set)
  shows β ∈ Ordinal → ordinalMul(0, β) = 0
proof
  induction β using membership
  intros current ih hCurrent
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    have base := ordinalMul.zero at 0
    rw ← nat.zero
    rw base
    symm
    exact nat.zero
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      rw [ordinalMul.next, step]
      exact ordinalAdd.zero at 0
    . apply Subset.antisymmetric
      . intros x hx
        obtain ⟨stage, hStage, hxStage⟩ :=
          ordinalMul.limit_membership.forward at x, 0, current with limit, hx
        have step := ih with hStage, (Ordinal.member with hCurrent, hStage)
        rw [step, nat.zero] at hxStage
        exfalso
        exact set.empty with hxStage
      . rw nat.zero
        exact empty.subset

theorem ordinalMul.subset_monotone (α β : Ordinal, γ : Set)
  shows γ ∈ Ordinal → β ∈ γ → α * β ⊆ α * γ
proof
  induction γ using membership
  intros current ih hCurrent hBelow
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . exfalso
    rw zero at hBelow
    exact set.empty at β with hBelow
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have αOrdinal : α ∈ Ordinal by assumption
      have productOrdinal := ordinalMul.ordinal at α, δ with δOrdinal
      have included := ordinalAdd.subset_left at α * δ, α with αOrdinal
      rw ordinalMul.next
      rw ← shape at hBelow
      simp [next.membership] at hBelow
      cases hBelow with earlier | equal
      . have step := ih with hδ, δOrdinal, earlier
        exact Subset.transitive with step, included
      . rw equal
        exact included
    . intros x hx
      apply ordinalMul.limit_membership.backward at x, α, current with limit
      witness β
      constructor
      . exact hBelow
      . exact hx

theorem ordinalMul.subset_monotone_of_subset (α β γ : Ordinal)
  requires h : β ⊆ γ
  shows α * β ⊆ α * γ
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have γOrdinal : γ ∈ Ordinal by assumption
  have below := Ordinal.subset_iff_member_next.forward
    with βOrdinal, γOrdinal, h
  simp [next.membership] at below
  cases below with earlier | equal
  . exact ordinalMul.subset_monotone at α, β, γ with γOrdinal, earlier
  . rw equal
    exact Subset.reflexive

theorem Ordinal.one_subset (α : Ordinal)
  requires positive : ∅ ∈ α
  shows 1 ⊆ α
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have one : 1 = next(0) by simp [next.natural]
  rw [one, nat.zero]
  exact Ordinal.member_iff_next_subset.forward
    with Ordinal.empty, αOrdinal, positive

theorem Ordinal.zero_member_one
  shows ∅ ∈ 1
proof
  have one : 1 = next(0) by simp [next.natural]
  rw [one, nat.zero]
  exact next.contains at ∅

theorem Ordinal.zero_member_of_one (α : Ordinal)
  requires above : 1 ∈ α
  shows ∅ ∈ α
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have included := Ordinal.member_subset with αOrdinal, above
  exact included with ∅, Ordinal.zero_member_one

theorem ordinalMul.subset_left_factor (α β : Ordinal)
  requires positive : ∅ ∈ β
  shows α ⊆ α * β
proof
  have oneIn := Ordinal.one_subset with positive
  have grows := ordinalMul.subset_monotone_of_subset at α, 1, β with oneIn
  rw ordinalMul.one at grows
  exact grows

theorem ordinalMul.monotone (α β : Ordinal, γ : Set)
  requires positive : ∅ ∈ α
  shows γ ∈ Ordinal → β ∈ γ → α * β ∈ α * γ
proof
  induction γ using membership
  intros current ih hCurrent hBelow
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . exfalso
    rw zero at hBelow
    exact set.empty at β with hBelow
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have productOrdinal := ordinalMul.ordinal at α, δ with δOrdinal
      have grows := ordinalAdd.member_right at α * δ, α with positive
      rw ordinalMul.next
      rw ← shape at hBelow
      simp [next.membership] at hBelow
      cases hBelow with earlier | equal
      . have step := ih with hδ, δOrdinal, earlier
        have αOrdinal : α ∈ Ordinal by assumption
        have included := ordinalAdd.subset_left at α * δ, α with αOrdinal
        exact included with α * β, step
      . rw equal
        exact grows
    . apply ordinalMul.limit_membership.backward at α * β, α, current with limit
      witness next(β)
      constructor
      . exact limit.right.right with β, hBelow
      . rw ordinalMul.next
        have βOrdinal : β ∈ Ordinal by assumption
        have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal
        exact ordinalAdd.member_right at α * β, α with positive

theorem ordinalMul.member_right (α β : Ordinal)
  requires positive : ∅ ∈ α
  requires above : 1 ∈ β
  shows α ∈ α * β
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have grows := ordinalMul.monotone at α, 1, β with positive, βOrdinal, above
  rw ordinalMul.one at grows
  exact grows

theorem ordinalMul.limit_right (α λ : Ordinal)
  requires positive : ∅ ∈ α
  requires limit : Limit(λ)
  shows Limit(α * λ)
proof
  have λOrdinal : λ ∈ Ordinal by assumption
  have productOrdinal := ordinalMul.ordinal at α, λ with λOrdinal
  constructor
  . exact productOrdinal
  . constructor
    . intro equal
      have zeroIn := Ordinal.zero_member with limit.right.left
      have member := ordinalMul.monotone at α, ∅, λ
        with positive, λOrdinal, zeroIn
      rw equal at member
      exact set.empty with member
    . intros x hx
      obtain ⟨β, hβ, hxβ⟩ :=
        ordinalMul.limit_membership.forward at x, α, λ with limit, hx
      have βOrdinal := Ordinal.member with λOrdinal, hβ
      have stageOrdinal := ordinalMul.ordinal at α, β with βOrdinal
      have xOrdinal := Ordinal.member with stageOrdinal, hxβ
      have αOrdinal : α ∈ Ordinal by assumption
      have sumOrdinal := ordinalAdd.ordinal at α * β, α with αOrdinal
      apply ordinalMul.limit_membership.backward at next(x), α, λ with limit
      witness next(β)
      constructor
      . exact limit.right.right with β, hβ
      . rw ordinalMul.next
        have grows := ordinalAdd.member_right at α * β, α with positive
        have included := Ordinal.member_iff_next_subset.forward with
          stageOrdinal, sumOrdinal, grows
        have step := next.member_iff.backward with xOrdinal, stageOrdinal, hxβ
        exact included with next(x), step

theorem ordinalMul.subset_right (α : Ordinal, β : Set)
  requires positive : ∅ ∈ α
  shows β ∈ Ordinal → β ⊆ α * β
proof
  induction β using membership
  intros current ih hCurrent
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    exact empty.subset
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      have productOrdinal := ordinalMul.ordinal at α, γ with γOrdinal
      have αOrdinal : α ∈ Ordinal by assumption
      have sumOrdinal := ordinalAdd.ordinal at α * γ, α with αOrdinal
      rw ordinalMul.next
      have first := next.monotone at γ, α * γ with step
      have grows := ordinalAdd.member_right at α * γ, α with positive
      have second := Ordinal.member_iff_next_subset.forward with
        productOrdinal, sumOrdinal, grows
      exact Subset.transitive with first, second
    . intros x hx
      apply ordinalMul.limit_membership.backward at x, α, current with limit
      have xOrdinal := Ordinal.member with hCurrent, hx
      have nextIn := limit.right.right with x, hx
      witness next(x)
      constructor
      . exact nextIn
      . have step := ih with hx, xOrdinal
        have productOrdinal := ordinalMul.ordinal at α, x with xOrdinal
        have αOrdinal : α ∈ Ordinal by assumption
        have sumOrdinal := ordinalAdd.ordinal at α * x, α with αOrdinal
        rw ordinalMul.next
        have grows := ordinalAdd.member_right at α * x, α with positive
        have included := Ordinal.member_iff_next_subset.forward with
          productOrdinal, sumOrdinal, grows
        have member := Ordinal.subset_bound with xOrdinal, productOrdinal, step
        exact included with x, member

theorem ordinalMul.cancel (α β γ : Ordinal)
  requires positive : ∅ ∈ α
  requires equal : α * β = α * γ
  shows β = γ
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have γOrdinal : γ ∈ Ordinal by assumption
  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal
  cases cases with below | rest
  . exfalso
    have member := ordinalMul.monotone at α, β, γ with positive, γOrdinal, below
    rw ← equal at member
    exact Ordinal.not_member_self with member
  . cases rest with same | above
    . exact same
    . exfalso
      have member := ordinalMul.monotone at α, γ, β
        with positive, βOrdinal, above
      rw equal at member
      exact Ordinal.not_member_self with member

-- Exponentiation

theorem ordinalPow.positive (α : Ordinal, β : Set)
  requires positive : ∅ ∈ α
  shows β ∈ Ordinal → ∅ ∈ α ^ β
proof
  induction β using membership
  intros current ih hCurrent
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    have base := ordinalPow.zero at α
    rw nat.zero at base
    rw base
    exact Ordinal.zero_member_one
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      have powerOrdinal := ordinalPow.ordinal at α, γ with γOrdinal
      have αOrdinal : α ∈ Ordinal by assumption
      rw ordinalPow.next
      have grows := ordinalMul.monotone at α ^ γ, ∅, α
        with step, αOrdinal, positive
      rw ← nat.zero at grows
      rw ordinalMul.zero at grows
      exact grows
    . apply ordinalPow.limit_membership.backward at ∅, α, current with limit
      witness ∅
      constructor
      . exact Ordinal.zero_member with limit.right.left
      . have base := ordinalPow.zero at α
        rw nat.zero at base
        rw base
        exact Ordinal.zero_member_one

theorem ordinalPow.subset_monotone (α β : Ordinal, γ : Set)
  requires positive : ∅ ∈ α
  shows γ ∈ Ordinal → β ∈ γ → α ^ β ⊆ α ^ γ
proof
  induction γ using membership
  intros current ih hCurrent hBelow
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . exfalso
    rw zero at hBelow
    exact set.empty at β with hBelow
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have powerOrdinal := ordinalPow.ordinal at α, δ with δOrdinal
      have included := ordinalMul.subset_left_factor at α ^ δ, α with positive
      rw ordinalPow.next
      rw ← shape at hBelow
      simp [next.membership] at hBelow
      cases hBelow with earlier | equal
      . have step := ih with hδ, δOrdinal, earlier
        exact Subset.transitive with step, included
      . rw equal
        exact included
    . intros x hx
      apply ordinalPow.limit_membership.backward at x, α, current with limit
      witness β
      constructor
      . exact hBelow
      . exact hx

theorem ordinalPow.monotone (α β : Ordinal, γ : Set)
  requires above : 1 ∈ α
  shows γ ∈ Ordinal → β ∈ γ → α ^ β ∈ α ^ γ
proof
  induction γ using membership
  intros current ih hCurrent hBelow
  have positive := Ordinal.zero_member_of_one with above
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . exfalso
    rw zero at hBelow
    exact set.empty at β with hBelow
  . cases rest with successor | limit
    . obtain ⟨δ, hδ, shape⟩ := successor
      rw ← shape
      have δOrdinal := Ordinal.member with hCurrent, hδ
      have powerOrdinal := ordinalPow.ordinal at α, δ with δOrdinal
      have basePositive := ordinalPow.positive at α, δ with positive, δOrdinal
      have grows := ordinalMul.member_right at α ^ δ, α with basePositive, above
      rw ordinalPow.next
      rw ← shape at hBelow
      simp [next.membership] at hBelow
      cases hBelow with earlier | equal
      . have step := ih with hδ, δOrdinal, earlier
        have included := ordinalMul.subset_left_factor at α ^ δ, α with positive
        exact included with α ^ β, step
      . rw equal
        exact grows
    . apply ordinalPow.limit_membership.backward at α ^ β, α, current with limit
      witness next(β)
      constructor
      . exact limit.right.right with β, hBelow
      . rw ordinalPow.next
        have βOrdinal : β ∈ Ordinal by assumption
        have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal
        have basePositive := ordinalPow.positive at α, β with positive, βOrdinal
        exact ordinalMul.member_right at α ^ β, α with basePositive, above

theorem ordinalPow.limit_right (α λ : Ordinal)
  requires above : 1 ∈ α
  requires limit : Limit(λ)
  shows Limit(α ^ λ)
proof
  have λOrdinal : λ ∈ Ordinal by assumption
  have positive := Ordinal.zero_member_of_one with above
  have powerOrdinal := ordinalPow.ordinal at α, λ with λOrdinal
  constructor
  . exact powerOrdinal
  . constructor
    . intro equal
      have member := ordinalPow.positive at α, λ with positive, λOrdinal
      rw equal at member
      exact set.empty with member
    . intros x hx
      obtain ⟨β, hβ, hxβ⟩ :=
        ordinalPow.limit_membership.forward at x, α, λ with limit, hx
      have βOrdinal := Ordinal.member with λOrdinal, hβ
      have stageOrdinal := ordinalPow.ordinal at α, β with βOrdinal
      have xOrdinal := Ordinal.member with stageOrdinal, hxβ
      have αOrdinal : α ∈ Ordinal by assumption
      have productOrdinal := ordinalMul.ordinal at α ^ β, α with αOrdinal
      have basePositive := ordinalPow.positive at α, β with positive, βOrdinal
      apply ordinalPow.limit_membership.backward at next(x), α, λ with limit
      witness next(β)
      constructor
      . exact limit.right.right with β, hβ
      . rw ordinalPow.next
        have grows := ordinalMul.member_right at α ^ β, α
          with basePositive, above
        have included := Ordinal.member_iff_next_subset.forward with
          stageOrdinal, productOrdinal, grows
        have step := next.member_iff.backward with xOrdinal, stageOrdinal, hxβ
        exact included with next(x), step

theorem ordinalPow.subset_right (α : Ordinal, β : Set)
  requires above : 1 ∈ α
  shows β ∈ Ordinal → β ⊆ α ^ β
proof
  induction β using membership
  intros current ih hCurrent
  have positive := Ordinal.zero_member_of_one with above
  have αOrdinal : α ∈ Ordinal by assumption
  have cases := Ordinal.cases with hCurrent
  cases cases with zero | rest
  . rw zero
    exact empty.subset
  . cases rest with successor | limit
    . obtain ⟨γ, hγ, shape⟩ := successor
      rw ← shape
      have γOrdinal := Ordinal.member with hCurrent, hγ
      have step := ih with hγ, γOrdinal
      have powerOrdinal := ordinalPow.ordinal at α, γ with γOrdinal
      have productOrdinal := ordinalMul.ordinal at α ^ γ, α with αOrdinal
      have basePositive := ordinalPow.positive at α, γ with positive, γOrdinal
      rw ordinalPow.next
      have first := next.monotone at γ, α ^ γ with step
      have grows := ordinalMul.member_right at α ^ γ, α with basePositive, above
      have second := Ordinal.member_iff_next_subset.forward with
        powerOrdinal, productOrdinal, grows
      exact Subset.transitive with first, second
    . intros x hx
      apply ordinalPow.limit_membership.backward at x, α, current with limit
      have xOrdinal := Ordinal.member with hCurrent, hx
      have nextIn := limit.right.right with x, hx
      witness next(x)
      constructor
      . exact nextIn
      . have step := ih with hx, xOrdinal
        have powerOrdinal := ordinalPow.ordinal at α, x with xOrdinal
        have productOrdinal := ordinalMul.ordinal at α ^ x, α with αOrdinal
        have basePositive := ordinalPow.positive at α, x with positive, xOrdinal
        rw ordinalPow.next
        have grows := ordinalMul.member_right at α ^ x, α
          with basePositive, above
        have included := Ordinal.member_iff_next_subset.forward with
          powerOrdinal, productOrdinal, grows
        have member := Ordinal.subset_bound with xOrdinal, powerOrdinal, step
        exact included with x, member

theorem ordinalPow.cancel (α β γ : Ordinal)
  requires above : 1 ∈ α
  requires equal : α ^ β = α ^ γ
  shows β = γ
proof
  have βOrdinal : β ∈ Ordinal by assumption
  have γOrdinal : γ ∈ Ordinal by assumption
  have cases := Ordinal.trichotomy with βOrdinal, γ, γOrdinal
  cases cases with below | rest
  . exfalso
    have member := ordinalPow.monotone at α, β, γ with above, γOrdinal, below
    rw ← equal at member
    exact Ordinal.not_member_self with member
  . cases rest with same | above2
    . exact same
    . exfalso
      have member := ordinalPow.monotone at α, γ, β with above, βOrdinal, above2
      rw equal at member
      exact Ordinal.not_member_self with member

-- Every ordinal is zero, a successor, or a limit.
theorem Ordinal.zero_successor_or_limit (α : Ordinal)
  shows α = 0 ∨ (∃ β, β ∈ Ordinal ∧ α = next(β)) ∨ Limit(α)
proof
  have αOrdinal : α ∈ Ordinal by assumption
  have cases := Ordinal.cases with αOrdinal
  cases cases with zero | rest
  . left
    rw nat.zero
    exact zero
  . cases rest with successor | limit
    . right
      left
      obtain ⟨β, hβ, shape⟩ := successor
      witness β
      constructor
      . exact Ordinal.member with αOrdinal, hβ
      . symm
        exact shape
    . right
      right
      exact limit