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

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
Tactic:
induction i
State after:
case zero
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[0] [x] → y ∈ ftr f m isDec x

case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x] → y ∈ ftr f m isDec x

State before:
case zero
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[0] [x] → y ∈ ftr f m isDec x

case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x] → y ∈ ftr f m isDec x
Tactic:
all_goals intro x y y_in
State after:
case zero
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[0] [x]
⊢ y ∈ ftr f m isDec x

case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x]
⊢ y ∈ ftr f m isDec x

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[0] [x]
⊢ y ∈ ftr f m isDec x
Tactic:
case zero =>
  simp at y_in
  rw [ftr]
  simp
  left
  assumption
State after:
no goals

State before:
case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x] → y ∈ ftr f m isDec x
Tactic:
intro x y y_in
State after:
case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x]
⊢ y ∈ ftr f m isDec x

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[0] [x]
⊢ y ∈ ftr f m isDec x
Tactic:
simp at y_in
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ y ∈ ftr f m isDec x

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ y ∈ ftr f m isDec x
Tactic:
rw [ftr]
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ 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

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ 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
Tactic:
simp
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
Tactic:
left
State after:
case h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : y = x
⊢ y = x

State before:
case h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
y_in : 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
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[i + 1] [x]
⊢ y ∈ ftr f m isDec x
Tactic:
rw [ftr.iff']
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[i + 1] [x]
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ (fun X => (List.map f X).join)^[i + 1] [x]
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rw [Function.iterate_succ'] at y_in
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ ((fun X => (List.map f X).join) ∘ (fun X => (List.map f X).join)^[i]) [x]
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : y ∈ ((fun X => (List.map f X).join) ∘ (fun X => (List.map f X).join)^[i]) [x]
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
simp at y_in
State after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : ∃ a ∈ (fun X => (List.map f X).join)^[i] [x], y ∈ f a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y : α
y_in : ∃ a ∈ (fun X => (List.map f X).join)^[i] [x], y ∈ f a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
rcases y_in with ⟨b, b_in_fiX, y_in_fb⟩
State after:
case intro.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case intro.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
right
State after:
case intro.intro.h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

State before:
case intro.intro.h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
Tactic:
use b
State after:
case h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ ftr f m isDec x ∧ y ∈ f b

State before:
case h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ ftr f m isDec x ∧ y ∈ f b
Tactic:
constructor
State after:
case h.left
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ ftr f m isDec x

case h.right
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ y ∈ f b

State before:
case h.left
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ ftr f m isDec x
Tactic:
apply IH
State after:
case h.left.a
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ (fun X => (List.map f X).join)^[i] [x]

State before:
case h.left.a
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ b ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
assumption
State after:
no goals

State before:
case h.right
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ y ∈ f b
Tactic:
assumption
State after:
no goals