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

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp only [list_direct_succ_set] at h1
State after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp at h1
State after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp only [Set.subset_def]
State after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ ↑xs.toFinset

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ ↑xs.toFinset
Tactic:
simp
State after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ xs

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ xs
Tactic:
intro a a1
State after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a : α
a1 : a ∈ reachable_from_list g xs
⊢ a ∈ xs

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a : α
a1 : a ∈ reachable_from_list g xs
⊢ a ∈ xs
Tactic:
induction a1
State after:
case base
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
a✝ : x✝ ∈ xs
⊢ x✝ ∈ xs

case step
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
e✝ : α × List α
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g xs e✝.1
a_ih✝ : e✝.1 ∈ xs
⊢ x✝ ∈ xs

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
ih : x✝ ∈ xs
⊢ x✝ ∈ xs
Tactic:
case _ _ ih =>
  exact ih
State after:
no goals

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x : α
e : α × List α
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ xs
⊢ x ∈ xs
Tactic:
case _ x e ih_1 ih_2 _ ih_4 =>
  exact h1 x e.fst ih_4 e.snd ih_2 ih_1
State after:
no goals

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
ih : x✝ ∈ xs
⊢ x✝ ∈ xs
Tactic:
exact ih
State after:
no goals

State before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x : α
e : α × List α
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ xs
⊢ x ∈ xs
Tactic:
exact h1 x e.fst ih_4 e.snd ih_2 ih_1
State after:
no goals