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

State before:
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x ↔ y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
Tactic:
constructor
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x → y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z

case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z) → y ∈ ftr f m isDec x

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

State before:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in : y ∈ ftr f m isDec x
⊢ y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
Tactic:
unfold ftr at y_in
State after:
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
y_in :
  y ∈
    let x := x;
    [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
⊢ y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z

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

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

State before:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z) → y ∈ ftr f m isDec x
Tactic:
intro claim
State after:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x

State before:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
Tactic:
unfold ftr
State after:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y ∈
    let x := x;
    [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:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y ∈
    let x := x;
    [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:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a

State before:
case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
claim : y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
⊢ y = x ∨ ∃ a ∈ f x, y ∈ ftr f m isDec a
Tactic:
convert claim
State after:
no goals