case inr y_in =>
  rcases y_in with ⟨z, z_in_fx, y_in_ftr_z⟩
  have := (@IH (m z) (by rw [k_is]; exact isDec x z z_in_fx) z rfl y) y_in_ftr_z
  rcases this with ⟨j,y_in⟩
  use j + 1
  simp
  exact biUnion_subset f j [z] (f x) (by simp; assumption) y_in
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y : α
y_in : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
no goals