no goals
α : Type ?u.87265
β : Type ?u.87268
γ : Type ?u.87271
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x✝ : ∃ a, lift o = succ a
a : Ordinal
h : lift o = succ a
b : Ordinal
e : lift b = a
⊢ lift o = lift (succ b)
rw [h, ← e, lift_succ]
no goals
α : Type ?u.87265
β : Type ?u.87268
γ : Type ?u.87271
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x✝ : ∃ a, o = succ a
a : Ordinal
h : o = succ a
⊢ lift o = succ (lift a)
simp only [h, lift_succ]