α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose (_ : ∃ x, (fun x => r (f (Directed.sequence f hf (encode a))) (f x) ∧ r (f a) (f x)) x)))
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence f hf (encode a + 1)))
simp only [Directed.sequence, add_eq, add_zero, encodek, and_self]
no goals
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose (_ : ∃ x, (fun x => r (f (Directed.sequence f hf (encode a))) (f x) ∧ r (f a) (f x)) x)))
exact (Classical.choose_spec (hf _ a)).2