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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
Tactic:
simp only [Set.subset_def]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
Tactic:
intro a a1
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
a1 : a ∈ reachable_from_list g (direct_succ_list g x)
⊢ a ∈ reachable_from_list g [x]

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
a1 : a ∈ reachable_from_list g (direct_succ_list g x)
⊢ a ∈ reachable_from_list g [x]
Tactic:
induction a1
State after:
case base
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
a✝ : x✝ ∈ direct_succ_list g x
⊢ x✝ ∈ reachable_from_list g [x]

case step
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
e✝ : Node × List Node
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g (direct_succ_list g x) e✝.1
a_ih✝ : e✝.1 ∈ reachable_from_list g [x]
⊢ x✝ ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
⊢ y ∈ reachable_from_list g [x]
Tactic:
case _ x y ih =>
  obtain s1 := mem_direct_succ_list_iff g x y
  simp only [s1] at ih
  apply Exists.elim ih
  intro ys a2
  cases a2
  case _ a2_left a2_right =>
    apply reachable_from_list.step y (x, ys) a2_right a2_left
    apply reachable_from_list.base x
    simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x✝ a x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g (direct_succ_list g x✝) e.1
ih_4 : e.1 ∈ reachable_from_list g [x✝]
⊢ x ∈ reachable_from_list g [x✝]
Tactic:
case _ x e ih_1 ih_2 _ ih_4 =>
  exact reachable_from_list.step x e ih_1 ih_2 ih_4
State after:
no goals

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
⊢ y ∈ reachable_from_list g [x]
Tactic:
obtain s1 := mem_direct_succ_list_iff g x y
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
simp only [s1] at ih
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
apply Exists.elim ih
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ g → y ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ g → y ∈ reachable_from_list g [x]
Tactic:
intro ys a2
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2 : y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2 : y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
cases a2
State after:
case intro
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
left✝ : y ∈ ys
right✝ : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
case _ a2_left a2_right =>
  apply reachable_from_list.step y (x, ys) a2_right a2_left
  apply reachable_from_list.base x
  simp
State after:
no goals

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
apply reachable_from_list.step y (x, ys) a2_right a2_left
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ reachable_from_list g [x] (x, ys).1

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ reachable_from_list g [x] (x, ys).1
Tactic:
apply reachable_from_list.base x
State after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ x ∈ [x]

State before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ x ∈ [x]
Tactic:
simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x✝ a x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g (direct_succ_list g x✝) e.1
ih_4 : e.1 ∈ reachable_from_list g [x✝]
⊢ x ∈ reachable_from_list g [x✝]
Tactic:
exact reachable_from_list.step x e ih_1 ih_2 ih_4
State after:
no goals