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

State before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : (fun x => s' ∈ x) ↑(dft_aux g S []).toFinset = (fun x => s' ∈ x) (reachable_from_list g S)
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
simp at this
State after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

State before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
simp [dft, this]
State after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

State before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
clear this
State after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

State before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S → ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ (∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s') → s' ∈ reachable_from_list g S

State before:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S → ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
intro h
State after:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
h : s' ∈ reachable_from_list g S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

State before:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
h : s' ∈ reachable_from_list g S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
induction h with
| base _ h => exact ⟨_, h, .refl⟩
| step _ _ h1 h2 _ ih =>
  have ⟨_, h3, h4⟩ := ih
  exact ⟨_, h3, .tail h4 ⟨_, h1, h2⟩⟩
State after:
no goals

State before:
case mp.base
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
h : x✝ ∈ S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
exact ⟨_, h, .refl⟩
State after:
no goals

State before:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
have ⟨_, h3, h4⟩ := ih
State after:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
w✝ : α
h3 : w✝ ∈ S
h4 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) w✝ e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝

State before:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
w✝ : α
h3 : w✝ ∈ S
h4 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) w✝ e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
exact ⟨_, h3, .tail h4 ⟨_, h1, h2⟩⟩
State after:
no goals

State before:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ (∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s') → s' ∈ reachable_from_list g S
Tactic:
intro ⟨s, h1, h2⟩
State after:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
h2 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
⊢ s' ∈ reachable_from_list g S

State before:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
h2 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
⊢ s' ∈ reachable_from_list g S
Tactic:
induction h2 with
| refl => exact reachable_from_list.base _ h1
| tail _ h ih =>
  have ⟨_, h3, h4⟩ := h
  exact reachable_from_list.step _ _ h3 h4 ih
State after:
no goals

State before:
case mpr.refl
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
⊢ s ∈ reachable_from_list g S
Tactic:
exact reachable_from_list.base _ h1
State after:
no goals

State before:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
⊢ c✝ ∈ reachable_from_list g S
Tactic:
have ⟨_, h3, h4⟩ := h
State after:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
w✝ : List α
h3 : (b✝, w✝) ∈ g
h4 : c✝ ∈ w✝
⊢ c✝ ∈ reachable_from_list g S

State before:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
w✝ : List α
h3 : (b✝, w✝) ∈ g
h4 : c✝ ∈ w✝
⊢ c✝ ∈ reachable_from_list g S
Tactic:
exact reachable_from_list.step _ _ h3 h4 ih
State after:
no goals