case intro
α : Type ?u.88270
β : Type ?u.88273
γ : Type ?u.88276
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o a : Ordinal
e : o = succ a
⊢ lift (pred o) = pred (lift o)
α : Type ?u.88270
β : Type ?u.88273
γ : Type ?u.88276
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
⊢ lift (pred o) = pred (lift o)
cases' h with a e
no goals
case intro
α : Type ?u.88270
β : Type ?u.88273
γ : Type ?u.88276
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o a : Ordinal
e : o = succ a
⊢ lift (pred o) = pred (lift o)
simp only [e, pred_succ, lift_succ]
no goals
α : Type ?u.88270
β : Type ?u.88273
γ : Type ?u.88276
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ¬∃ a, o = succ a
⊢ lift (pred o) = pred (lift o)
rw [pred_eq_iff_not_succ.2 h, pred_eq_iff_not_succ.2 (mt lift_is_succ.1 h)]