OrdConnected.succOrder, type classes are confusing

Stream: lean4

[Nir Paz]

I want to prove this, which I think is true if the inherited SuccOrder is the obvious one:

import Mathlib

open Set Order

example {o : Ordinal} {h : o.IsLimit} {α : Iio o} : (succ α).1 = α.1 + 1 := sorry

I'm having a lot of trouble just getting to the actual definition of succ here. It's inherited through many layers of type classes (from Iio α being ordConnected) and I can't find a theorem that just "says" what it is. I don't know how to deal with this except by naively unfolding everything, which only gets me even more confusing proof states.

[Ruben Van de Velde]

If such a lemma is missing and you know what it should be, you can write the lemma yourself with proof rfl

[Nir Paz]

I guess the lemma would be that if S is an OrdConnected subtype of something and s : S is such that there is an element of S above it, then (succ s).1 = succ s.1 (not 100% this is true, I'm extrapolating from the OrdConnected requirement). But I straight up can't prove this.

[Matt Diamond]

import Mathlib

open Set Order

example {o : Ordinal} {h : o.IsLimit} {α : Iio o} : (succ α).1 = α.1 + 1 :=
by
  rw [Ordinal.add_one_eq_succ]
  apply coe_succ_of_mem
  have := Subtype.mem α
  rw [mem_Iio] at this ⊢
  exact h.succ_lt this

[Matt Diamond]

I think docs#coe_succ_of_mem might've been the missing piece here

[Nir Paz]

Thanks!