Typein for ordinals

Stream: Is there code for X?

[Sky Wilshaw]

I'm trying to prove some facts about the definition of typein on the order type of the ordinals.

import Mathlib

open Ordinal

theorem typein_ordinal (o : Ordinal.{u}) :
    -- Also, why can't Lean find this instance?
    letI := inferInstanceAs (IsWellOrder Ordinal (· < ·))
    typein (· < ·) o = lift.{u + 1} o :=
  sorry

[Sky Wilshaw]

For future reference, this code works:

@[simp]
theorem typein_ordinal (o : Ordinal.{u}) :
    -- TODO: Why can't Lean find this instance?
    letI := inferInstanceAs (IsWellOrder Ordinal (· < ·))
    typein (· < ·) o = lift.{u + 1} o := by
  letI := inferInstanceAs (IsWellOrder Ordinal (· < ·))
  induction o using Ordinal.induction with
  | h o ih =>
    apply le_antisymm
    · by_contra! h
      have := ih (enum ((· < ·) : Ordinal → Ordinal → Prop)
        ⟨lift.{u + 1} o, h.trans (typein_lt_type _ o)⟩) ?_
      · simp only [typein_enum, lift_inj] at this
        conv_rhs at h => rw [this]
        simp only [typein_enum, lt_self_iff_false] at h
      · conv_rhs => rw [← enum_typein (· < ·) o]
        exact enum_lt_enum.mpr h
    · by_contra! h
      rw [Ordinal.lt_lift_iff] at h
      obtain ⟨o', ho'₁, ho'₂⟩ := h
      rw [← ih o' ho'₂, typein_inj] at ho'₁
      exact ho'₂.ne ho'₁

[Floris van Doorn]

This seems like something that should be in Mathlib. I couldn't find anything about @typein Ordinal or @enum Ordinal, which surprised me.

[Violeta Hernández]

I think this should be def-eq to Ordinal.type_subrel_lt

[Floris van Doorn]

Ah, it is. Should that result be reformulated using typein?

[Violeta Hernández]

It should. I think @Nir Paz has a PR renaming this theorem, so it might be a good idea to reformulate it while we're at it.

[Nir Paz]

It's #16929. Should I reformulate it with the haveI and the TODO? It's really weird it doesn't synth

[Nir Paz]

Actually giving it Ordinal.{u} explicitly fixes it, even though when it fails to synth otherwise it looks like it filled in Ordinal.{u} itself.

[Nir Paz]

Changed it