case inr hyp =>
  rcases hyp with ⟨a, a_in_ftr_x, y_in_fa⟩
  rw [ftr.iff] at a_in_ftr_x
  cases a_in_ftr_x
  case inl a_is_x =>
    subst a_is_x
    unfold ftr
    unfold ftr
    aesop
  case inr hyp =>
    rcases hyp with ⟨z, z_in_fx, a_in_ftr_z⟩
    have y_in_ftr_z : y ∈ ftr f m isDec z := by
      rw [ftr.iff']
      right
      use a
    unfold ftr
    aesop
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ z ∈ ftr f m isDec x, y ∈ f z
⊢ y ∈ ftr f m isDec x
no goals