internlm/Lean-Github huggingface dataset:
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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]
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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)
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: direct_succ_list_set_equiv
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ↑(direct_succ_list g x).toFinset = direct_succ_set g x
Tactic:
ext a
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ direct_succ_set g x
Theorem: direct_succ_list_set_equiv
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ direct_succ_set g x
Tactic:
simp only [direct_succ_set]
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ {y | ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Theorem: direct_succ_list_set_equiv
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ {y | ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ direct_succ_list g x ↔ ∃ ys, a ∈ ys ∧ (x, ys) ∈ g
Theorem: direct_succ_list_set_equiv
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ direct_succ_list g x ↔ ∃ ys, a ∈ ys ∧ (x, ys) ∈ g
Tactic:
simp only [mem_direct_succ_list_iff]
Proof state after:
no goals
Theorem: mem_list_direct_succ_list_iff
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node), y ∈ list_direct_succ_list g xs ↔ ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
Tactic:
simp only [list_direct_succ_list]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
Theorem: mem_list_direct_succ_list_iff
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
Tactic:
simp only [← mem_direct_succ_list_iff]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, y ∈ direct_succ_list g x
Theorem: mem_list_direct_succ_list_iff
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, y ∈ direct_succ_list g x
Tactic:
simp
Proof state after:
no goals
Theorem: list_direct_succ_list_set_equiv
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = list_direct_succ_set g xs
Tactic:
simp only [list_direct_succ_set]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Theorem: list_direct_succ_list_set_equiv
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp only [← mem_list_direct_succ_list_iff]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | y ∈ list_direct_succ_list g xs}
Theorem: list_direct_succ_list_set_equiv
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | y ∈ list_direct_succ_list g xs}
Tactic:
simp
Proof state after:
no goals
Theorem: list_direct_succ_list_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ list_direct_succ_list g (x :: xs) = direct_succ_list g x ++ list_direct_succ_list g xs
Tactic:
simp only [list_direct_succ_list]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ (List.map (fun x => direct_succ_list g x) (x :: xs)).join =
    direct_succ_list g x ++ (List.map (fun x => direct_succ_list g x) xs).join
Theorem: list_direct_succ_list_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ (List.map (fun x => direct_succ_list g x) (x :: xs)).join =
    direct_succ_list g x ++ (List.map (fun x => direct_succ_list g x) xs).join
Tactic:
simp
Proof state after:
no goals
Theorem: list_direct_succ_set_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ list_direct_succ_set g (x :: xs) = ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g xs
Tactic:
simp only [list_direct_succ_set]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, ∃ ys, y ∈ ys ∧ (x_1, ys) ∈ g} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Theorem: list_direct_succ_set_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, ∃ ys, y ∈ ys ∧ (x_1, ys) ∈ g} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp only [← mem_direct_succ_list_iff]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, y ∈ direct_succ_list g x_1} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Theorem: list_direct_succ_set_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, y ∈ direct_succ_list g x_1} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Tactic:
simp
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | y ∈ direct_succ_list g x ∨ ∃ a ∈ xs, y ∈ direct_succ_list g a} =
    {a | a ∈ direct_succ_list g x} ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Theorem: list_direct_succ_set_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | y ∈ direct_succ_list g x ∨ ∃ a ∈ xs, y ∈ direct_succ_list g a} =
    {a | a ∈ direct_succ_list g x} ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Tactic:
rfl
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
h1 : x ∉ g.nodes_of
⊢ direct_succ_list g x = []
Tactic:
induction g
Proof state after:
case nil
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []

case cons
Node : Type
inst✝ : DecidableEq Node
x : Node
head✝ : Node × List Node
tail✝ : List (Node × List Node)
tail_ih✝ : x ∉ Graph.nodes_of tail✝ → direct_succ_list tail✝ x = []
h1 : x ∉ Graph.nodes_of (head✝ :: tail✝)
⊢ direct_succ_list (head✝ :: tail✝) x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []
Tactic:
case nil =>
  simp only [direct_succ_list]
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ Graph.nodes_of tl → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
case cons hd tl ih =>
  simp only [Graph.nodes_of] at ih
  simp at ih
  simp only [Graph.nodes_of] at h1
  simp at h1
  simp only [direct_succ_list]
  split_ifs
  case pos c1 =>
    subst c1
    simp at h1
  case neg c1 =>
    tauto
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []
Tactic:
simp only [direct_succ_list]
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ Graph.nodes_of tl → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [Graph.nodes_of] at ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ List.map Prod.fst tl ∪ (List.map Prod.snd tl).join → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ List.map Prod.fst tl ∪ (List.map Prod.snd tl).join → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp at ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ Graph.nodes_of (hd :: tl)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ Graph.nodes_of (hd :: tl)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [Graph.nodes_of] at h1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ List.map Prod.fst (hd :: tl) ∪ (List.map Prod.snd (hd :: tl)).join
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
h1 : x ∉ List.map Prod.fst (hd :: tl) ∪ (List.map Prod.snd (hd :: tl)).join
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp at h1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ direct_succ_list (hd :: tl) x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ direct_succ_list (hd :: tl) x = []
Tactic:
simp only [direct_succ_list]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ (if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) = []