Theorem: mem_direct_succ_list_iff (FOL/Parsing/DFT.lean)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (x y : Node), y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
Tactic:
induction g
State after:
case nil
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ direct_succ_list [] x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []

case cons
Node : Type
inst✝ : DecidableEq Node
head✝ : Node × List Node
tail✝ : List (Node × List Node)
tail_ih✝ : ∀ (x y : Node), y ∈ direct_succ_list tail✝ x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tail✝
⊢ ∀ (x y : Node), y ∈ direct_succ_list (head✝ :: tail✝) x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ head✝ :: tail✝

State before:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ direct_succ_list [] x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Tactic:
case nil =>
  simp only [direct_succ_list]
  simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ direct_succ_list [] x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Tactic:
simp only [direct_succ_list]
State after:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ [] ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []

State before:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ [] ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Tactic:
simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∀ (x y : Node), y ∈ direct_succ_list (hd :: tl) x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
simp only [direct_succ_list]
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∀ (x y : Node),
    (y ∈ if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∀ (x y : Node),
    (y ∈ if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
intro x y
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
⊢ (y ∈ if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
⊢ (y ∈ if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
split_ifs
State after:
case pos
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
h✝ : hd.1 = x
⊢ y ∈ hd.2 ++ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl

case neg
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
h✝ : ¬hd.1 = x
⊢ y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : hd.1 = x
⊢ y ∈ hd.2 ++ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
subst c1
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ y ∈ hd.2 ++ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ hd :: tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ y ∈ hd.2 ++ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ hd :: tl
Tactic:
simp
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ y ∈ hd.2 ∨ y ∈ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ y ∈ hd.2 ∨ y ∈ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
simp only [ih]
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
constructor
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) → ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)) → y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) → ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
intro a1
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
cases a1
State after:
case mp.inl
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
h✝ : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

case mp.inr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
h✝ : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
left : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
case _ left =>
  apply Exists.intro hd.snd
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
case _ right =>
  apply Exists.elim right
  intro zs a2
  apply Exists.intro zs
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
left : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
apply Exists.intro hd.snd
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
left : y ∈ hd.2
⊢ y ∈ hd.2 ∧ ((hd.1, hd.2) = hd ∨ (hd.1, hd.2) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
left : y ∈ hd.2
⊢ y ∈ hd.2 ∧ ((hd.1, hd.2) = hd ∨ (hd.1, hd.2) ∈ tl)
Tactic:
tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
apply Exists.elim right
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∀ (a : List Node), y ∈ a ∧ (hd.1, a) ∈ tl → ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∀ (a : List Node), y ∈ a ∧ (hd.1, a) ∈ tl → ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
intro zs a2
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (hd.1, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (hd.1, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
apply Exists.intro zs
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (hd.1, zs) ∈ tl
⊢ y ∈ zs ∧ ((hd.1, zs) = hd ∨ (hd.1, zs) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (hd.1, zs) ∈ tl
⊢ y ∈ zs ∧ ((hd.1, zs) = hd ∨ (hd.1, zs) ∈ tl)
Tactic:
tauto
State after:
no goals

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
⊢ (∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)) → y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
intro a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
simp only [Prod.eq_iff_fst_eq_snd_eq] at a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (True ∧ ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (True ∧ ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
simp at a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
apply Exists.elim a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ ∀ (a : List Node), y ∈ a ∧ (a = hd.2 ∨ (hd.1, a) ∈ tl) → y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ ∀ (a : List Node), y ∈ a ∧ (a = hd.2 ∨ (hd.1, a) ∈ tl) → y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
intro zs a2
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2 : y ∈ zs ∧ (zs = hd.2 ∨ (hd.1, zs) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2 : y ∈ zs ∧ (zs = hd.2 ∨ (hd.1, zs) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
cases a2
State after:
case mpr.intro
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
left✝ : y ∈ zs
right✝ : zs = hd.2 ∨ (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
a2_right : zs = hd.2 ∨ (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
case _ a2_left a2_right =>
  cases a2_right
  case _ left =>
    subst left
    tauto
  case _ right =>
    right
    apply Exists.intro zs
    tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
a2_right : zs = hd.2 ∨ (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
cases a2_right
State after:
case inl
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
h✝ : zs = hd.2
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

case inr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
h✝ : (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
left : zs = hd.2
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
case _ left =>
  subst left
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
case _ right =>
  right
  apply Exists.intro zs
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
left : zs = hd.2
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
subst left
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
a2_left : y ∈ hd.2
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
a2_left : y ∈ hd.2
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
right
State after:
case h
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl

State before:
case h
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
apply Exists.intro zs
State after:
case h
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ y ∈ zs ∧ (hd.1, zs) ∈ tl

State before:
case h
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2_left : y ∈ zs
right : (hd.1, zs) ∈ tl
⊢ y ∈ zs ∧ (hd.1, zs) ∈ tl
Tactic:
tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
simp
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
simp only [ih]
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ (x, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ (x, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
constructor
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ (x, ys) ∈ tl) → ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)) → ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ (x, ys) ∈ tl) → ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
intro a1
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
apply Exists.elim a1
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ tl → ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ tl → ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
intro zs a2
State after:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
case mp
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
cases a2
State after:
case mp.intro
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
left✝ : y ∈ zs
right✝ : (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2_left : y ∈ zs
a2_right : (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
case _ a2_left a2_right =>
  apply Exists.intro zs
  tauto
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2_left : y ∈ zs
a2_right : (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
Tactic:
apply Exists.intro zs
State after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2_left : y ∈ zs
a2_right : (x, zs) ∈ tl
⊢ y ∈ zs ∧ ((x, zs) = hd ∨ (x, zs) ∈ tl)

State before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2_left : y ∈ zs
a2_right : (x, zs) ∈ tl
⊢ y ∈ zs ∧ ((x, zs) = hd ∨ (x, zs) ∈ tl)
Tactic:
tauto
State after:
no goals

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
⊢ (∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)) → ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
Tactic:
intro a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
⊢ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
⊢ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
Tactic:
simp only [Prod.eq_iff_fst_eq_snd_eq] at a1
State after:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x = hd.1 ∧ ys = hd.2 ∨ (x, ys) ∈ tl)
⊢ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl

State before:
case mpr
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x = hd.1 ∧ ys = hd.2 ∨ (x, ys) ∈ tl)
⊢ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
Tactic:
tauto
State after:
no goals