α : Type ?u.80689
β : Type ?u.80692
γ : Type ?u.80695
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, succ o = succ a
⊢ pred (succ o) = o
α : Type ?u.80689
β : Type ?u.80692
γ : Type ?u.80695
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ pred (succ o) = o
have h : ∃ a, succ o = succ a := ⟨_, rfl⟩
no goals
α : Type ?u.80689
β : Type ?u.80692
γ : Type ?u.80695
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, succ o = succ a
⊢ pred (succ o) = o
simpa only [pred, dif_pos h] using (succ_injective <| Classical.choose_spec h).symm