Theorem: ftr.iff_Nth (Pdl/Closure.lean)

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x ↔ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
constructor
State after:
case mp
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

case mpr
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ (∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]) → y ∈ ftr f m isDec x

State before:
case mp
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
apply ftr.toNth (m x)
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ m x = m x

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ m x = m x
Tactic:
rfl
State after:
no goals

State before:
case mpr
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ (∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]) → y ∈ ftr f m isDec x
Tactic:
rintro ⟨i,claim⟩
State after:
case mpr.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
i : ℕ
claim : y ∈ (fun X => (List.map f X).join)^[i] [x]
⊢ y ∈ ftr f m isDec x

State before:
case mpr.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
i : ℕ
claim : y ∈ (fun X => (List.map f X).join)^[i] [x]
⊢ y ∈ ftr f m isDec x
Tactic:
apply ftr.fromNth claim
State after:
no goals