rw [ftr.iff_Nth] at s_in_ftr_t
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]