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

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
⊢ ∀ {x : α} {x_1 : k = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
induction k using Nat.strong_induction_on
State after:
case h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ :
  ∀ m_1 < n✝, ∀ {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 : α} {x_1 : n✝ = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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 : α} {x_1 : k = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
case h k IH =>
  intro x k_is y
  intro y_in rw [ftr] at y_in
  simp at y_in
  cases y_in
  case inl y_is_x =>
    use 0
    simp
    assumption
  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
State after:
no goals

State before:
α : 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 : α} {x_1 : k = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
intro x k_is y
State after:
α : 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 ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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 ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
intro y_in
State after:
α : 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 : y ∈ ftr f m isDec x
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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 : y ∈ ftr f m isDec x
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
rw [ftr] at y_in
State after:
α : 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 :
  y ∈
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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 :
  y ∈
    [x] ++
      (List.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, y_in⟩ =>
              let_fun this := y_in;
              ftr f m isDec y)
          (f x).attach).join
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
simp at y_in
State after:
α : 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 : y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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 : y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
cases y_in
State after:
case inl
α : 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 : α
h✝ : y = x
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

case inr
α : 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 : α
h✝ : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
α : 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_is_x : y = x
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
case inl y_is_x =>
  use 0
  simp
  assumption
State after:
no goals

State before:
α : 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]
Tactic:
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
State after:
no goals

State before:
α : 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_is_x : y = x
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
use 0
State after:
case h
α : 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_is_x : y = x
⊢ y ∈ (fun X => (List.map f X).join)^[0] [x]

State before:
case h
α : 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_is_x : y = x
⊢ y ∈ (fun X => (List.map f X).join)^[0] [x]
Tactic:
simp
State after:
case h
α : 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_is_x : y = x
⊢ y = x

State before:
case h
α : 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_is_x : y = x
⊢ y = x
Tactic:
assumption
State after:
no goals

State before:
α : 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]
Tactic:
rcases y_in with ⟨z, z_in_fx, y_in_ftr_z⟩
State after:
case intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
case intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
have := (@IH (m z) (by rw [k_is]; exact isDec x z z_in_fx) z rfl y) y_in_ftr_z
State after:
case intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
this : ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [z]
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
case intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
this : ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [z]
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
rcases this with ⟨j,y_in⟩
State after:
case intro.intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
case intro.intro.intro
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
use j + 1
State after:
case h
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ y ∈ (fun X => (List.map f X).join)^[j + 1] [x]

State before:
case h
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ y ∈ (fun X => (List.map f X).join)^[j + 1] [x]
Tactic:
simp
State after:
case h
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ y ∈ (fun X => (List.map f X).join)^[j] (f x)

State before:
case h
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ y ∈ (fun X => (List.map f X).join)^[j] (f x)
Tactic:
exact biUnion_subset f j [z] (f x) (by simp; assumption) y_in
State after:
no goals

State before:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ m z < k
Tactic:
rw [k_is]
State after:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ m z < m x

State before:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ m z < m x
Tactic:
exact isDec x z z_in_fx
State after:
no goals

State before:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ [z] ⊆ f x
Tactic:
simp
State after:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ z ∈ f x

State before:
α : 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 z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ z ∈ f x
Tactic:
assumption
State after:
no goals