case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
⊢ a ♯ 0 = a
a b c : Ordinal
⊢ a ♯ 0 = a
induction' a using Ordinal.induction with a IH
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
⊢ (blsub a fun a' x => a' ♯ 0) = a
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
⊢ a ♯ 0 = a
rw [nadd_def, blsub_zero, max_zero_right]
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
x✝¹ : Ordinal
x✝ : x✝¹ < a
⊢ x✝¹ ♯ 0 = x✝¹
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
⊢ (blsub a fun a' x => a' ♯ 0) = a
convert blsub_id a
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
x✝ : Ordinal
hb : x✝ < a
⊢ x✝ ♯ 0 = x✝
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
x✝¹ : Ordinal
x✝ : x✝¹ < a
⊢ x✝¹ ♯ 0 = x✝¹
rename_i hb
no goals
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 0 = k
x✝ : Ordinal
hb : x✝ < a
⊢ x✝ ♯ 0 = x✝
exact IH _ hb