α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode (n + 0) with
      | none =>
        Classical.choose
          (_ : ∃ z, r (f (Directed.sequence f hf (n + 0))) (f z) ∧ r (f (Directed.sequence f hf (n + 0))) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f (Directed.sequence f hf (n + 0))) (f z) ∧ r (f a) (f z))))
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))
dsimp [Directed.sequence]
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
⊢ r (f p)
    (f
      (match decode (n + 0) with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode (n + 0) with
      | none =>
        Classical.choose
          (_ : ∃ z, r (f (Directed.sequence f hf (n + 0))) (f z) ∧ r (f (Directed.sequence f hf (n + 0))) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f (Directed.sequence f hf (n + 0))) (f z) ∧ r (f a) (f z))))
generalize eq : hf.sequence f n = p
case none
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
h : decode n = none
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))

case some
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
a : α
h : decode n = some a
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
⊢ r (f p)
    (f
      (match decode (n + 0) with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
cases' h : (decode n: Option α) with a
no goals
case none
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
h : decode n = none
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
exact (Classical.choose_spec (hf p p)).1
no goals
case some
α : Type u_2
β : Type u_1
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
eq : Directed.sequence f hf n = p
a : α
h : decode n = some a
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
exact (Classical.choose_spec (hf p a)).1