internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ Holds D I (V ∘ σ) E F ↔ Holds D I V E (fastReplaceFree σ F)
Tactic:
apply substitution_theorem_aux D I (V ∘ σ) V E σ σ ∅ F h1
Proof state after:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ (v : VarName), v ∈ ∅ ∨ σ v ∉ ∅ → (V ∘ σ) v = V (σ v)

case h2'
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∈ ∅, v = σ v

case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∉ ∅, σ v = σ v
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ (v : VarName), v ∈ ∅ ∨ σ v ∉ ∅ → (V ∘ σ) v = V (σ v)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem
Proof state before:
case h2'
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∈ ∅, v = σ v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem
Proof state before:
case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F : Formula
h1 : admits σ F
⊢ ∀ v ∉ ∅, σ v = σ v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_is_valid
Proof state before:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : F.IsValid
⊢ (fastReplaceFree σ F).IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (fastReplaceFree σ F).IsValid
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_is_valid
Proof state before:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (fastReplaceFree σ F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (fastReplaceFree σ F)
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_is_valid
Proof state before:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (fastReplaceFree σ F)
Tactic:
intro D I V E
Proof state after:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (fastReplaceFree σ F)
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_is_valid
Proof state before:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (fastReplaceFree σ F)
Tactic:
simp only [← substitution_theorem D I V E σ F h1]
Proof state after:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_is_valid
Proof state before:
σ : VarName → VarName
F : Formula
h1 : admits σ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Tactic:
exact h2 D I (V ∘ σ) E
Proof state after:
no goals
Theorem: list_cons_to_set_union
Proof state before:
α : Type
inst : DecidableEq α
ys : List α
x : α
⊢ ↑(x :: ys).toFinset = {x} ∪ ↑ys.toFinset
Tactic:
ext a
Proof state after:
case h
α : Type
inst : DecidableEq α
ys : List α
x a : α
⊢ a ∈ ↑(x :: ys).toFinset ↔ a ∈ {x} ∪ ↑ys.toFinset
Theorem: list_cons_to_set_union
Proof state before:
case h
α : Type
inst : DecidableEq α
ys : List α
x a : α
⊢ a ∈ ↑(x :: ys).toFinset ↔ a ∈ {x} ∪ ↑ys.toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: list_append_to_set_union
Proof state before:
α : Type
inst : DecidableEq α
xs ys : List α
⊢ ↑(xs ++ ys).toFinset = ↑xs.toFinset ∪ ↑ys.toFinset
Tactic:
ext a
Proof state after:
case h
α : Type
inst : DecidableEq α
xs ys : List α
a : α
⊢ a ∈ ↑(xs ++ ys).toFinset ↔ a ∈ ↑xs.toFinset ∪ ↑ys.toFinset
Theorem: list_append_to_set_union
Proof state before:
case h
α : Type
inst : DecidableEq α
xs ys : List α
a : α
⊢ a ∈ ↑(xs ++ ys).toFinset ↔ a ∈ ↑xs.toFinset ∪ ↑ys.toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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
Proof 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✝
Theorem: mem_direct_succ_list_iff
Proof 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
Proof state after:
no goals
Theorem: mem_direct_succ_list_iff
Proof 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]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ [] ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Theorem: mem_direct_succ_list_iff
Proof state before:
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ [] ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Tactic:
simp
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), y ∈ direct_succ_list (hd :: tl) x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
simp only [direct_succ_list]
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),
    (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
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),
    (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
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
⊢ (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
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
⊢ (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
Proof 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
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 ∈ hd.2 ++ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
Tactic:
subst c1
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
⊢ y ∈ hd.2 ++ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ hd :: 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
⊢ y ∈ hd.2 ++ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ (hd.1, 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
y : Node
⊢ y ∈ hd.2 ∨ y ∈ direct_succ_list tl hd.1 ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (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
⊢ 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]
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
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (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
⊢ (y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl) ↔ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, 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
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
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
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
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
y : Node
a1 : y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, 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
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
Proof 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)
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
left : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
case _ left =>
  apply Exists.intro hd.snd
  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
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
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
left : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
apply Exists.intro hd.snd
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
left : y ∈ hd.2
⊢ y ∈ hd.2 ∧ ((hd.1, hd.2) = hd ∨ (hd.1, hd.2) ∈ 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
left : y ∈ hd.2
⊢ y ∈ hd.2 ∧ ((hd.1, hd.2) = hd ∨ (hd.1, hd.2) ∈ 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
right : ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
Tactic:
apply Exists.elim right
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
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)
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
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
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
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)
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
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
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
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)
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
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
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
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
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
y : Node
a1 : ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, 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
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
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
y : Node
a1 : ∃ ys, y ∈ ys ∧ (True ∧ ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, 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
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
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
y : Node
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, 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
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
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
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
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
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
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
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
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
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
Proof 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
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
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
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
a2_right : zs = hd.2 ∨ (hd.1, zs) ∈ tl
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
Tactic:
cases a2_right
Proof 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
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:
case _ left =>
  subst left
  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:
case _ right =>
  right
  apply Exists.intro zs
  tauto
Proof state after:
no goals