internlm/Lean-Github huggingface dataset:
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof state after:
no goals
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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]
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof state after:
no goals
Theorem: ftr.fromNth
Proof 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']
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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⟩
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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
Theorem: ftr.fromNth
Proof 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
Proof 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]
Theorem: ftr.fromNth
Proof 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
Proof state after:
no goals
Theorem: ftr.fromNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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⟩
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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⟩
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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]
Theorem: ftr.toNth
Proof 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
Proof 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)
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals
Theorem: ftr.toNth
Proof 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]
Proof 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
Theorem: ftr.toNth
Proof 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
Proof state after:
no goals