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
a : α
y_in_fa : y ∈ f a
hyp : ∃ z ∈ f x, a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
no goals