a b : Ordinal
a0 : a ≠ 0
h : IsLimit b
⊢ (limitRecOn b 1 (fun x IH => IH * a) fun b x => bsup b) =
    bsup b fun c x => limitRecOn c 1 (fun x IH => IH * a) fun b x => bsup b
a b : Ordinal
a0 : a ≠ 0
h : IsLimit b
⊢ a ^ b = bsup b fun c x => a ^ c
simp only [opow_def, if_neg a0]
no goals
a b : Ordinal
a0 : a ≠ 0
h : IsLimit b
⊢ (limitRecOn b 1 (fun x IH => IH * a) fun b x => bsup b) =
    bsup b fun c x => limitRecOn c 1 (fun x IH => IH * a) fun b x => bsup b
rw [limitRecOn_limit _ _ _ _ h]