internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
p' : Walk G u✝ v'
he : cons h✝ (concat p✝ h) = concat p' h'
⊢ ∃ hv, Walk.copy (cons h✝ p✝) (_ : u✝ = u✝) hv = p'
Tactic:
cases p'
Proof state after:
case cons.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (concat p✝ h) = concat nil h'
⊢ ∃ hv, Walk.copy (cons h✝ p✝) (_ : v' = v') hv = nil

case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝¹ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝¹ = v✝¹) hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : cons h✝¹ (concat p✝¹ h) = concat (cons h✝ p✝) h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (concat p✝ h) = concat nil h'
⊢ ∃ hv, Walk.copy (cons h✝ p✝) (_ : v' = v') hv = nil
Tactic:
exfalso
Proof state after:
case cons.nil.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (concat p✝ h) = concat nil h'
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.nil.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (concat p✝ h) = concat nil h'
⊢ False
Tactic:
simp only [concat_nil, cons.injEq] at he
Proof state after:
case cons.nil.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : v✝ = w ∧ HEq (concat p✝ h) nil
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.nil.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : v✝ = w ∧ HEq (concat p✝ h) nil
⊢ False
Tactic:
obtain ⟨rfl, he⟩ := he
Proof state after:
case cons.nil.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' v✝ w✝ : V
p✝ : Walk G v✝ w✝
h✝ h' : G.Adj v' v✝
ih : ∀ {h : G.Adj w✝ v✝} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ v✝
he : HEq (concat p✝ h) nil
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.nil.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' v✝ w✝ : V
p✝ : Walk G v✝ w✝
h✝ h' : G.Adj v' v✝
ih : ∀ {h : G.Adj w✝ v✝} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ v✝
he : HEq (concat p✝ h) nil
⊢ False
Tactic:
rw [heq_iff_eq] at he
Proof state after:
case cons.nil.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' v✝ w✝ : V
p✝ : Walk G v✝ w✝
h✝ h' : G.Adj v' v✝
ih : ∀ {h : G.Adj w✝ v✝} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ v✝
he : concat p✝ h = nil
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.nil.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' v✝ w✝ : V
p✝ : Walk G v✝ w✝
h✝ h' : G.Adj v' v✝
ih : ∀ {h : G.Adj w✝ v✝} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ v✝
he : concat p✝ h = nil
⊢ False
Tactic:
exact concat_ne_nil _ _ he
Proof state after:
no goals
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝¹ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝¹ = v✝¹) hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : cons h✝¹ (concat p✝¹ h) = concat (cons h✝ p✝) h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Tactic:
rw [concat_cons, cons.injEq] at he
Proof state after:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝¹ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝¹ = v✝¹) hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : v✝¹ = v✝ ∧ HEq (concat p✝¹ h) (concat p✝ h')
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝¹ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝¹ = v✝¹) hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : v✝¹ = v✝ ∧ HEq (concat p✝¹ h) (concat p✝ h')
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Tactic:
obtain ⟨rfl, he⟩ := he
Proof state after:
case cons.cons.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : HEq (concat p✝¹ h) (concat p✝ h')
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.cons.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : HEq (concat p✝¹ h) (concat p✝ h')
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Tactic:
rw [heq_iff_eq] at he
Proof state after:
case cons.cons.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat p✝¹ h = concat p✝ h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.cons.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝¹ h = concat p' h' → ∃ hv, Walk.copy p✝¹ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat p✝¹ h = concat p✝ h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝¹) (_ : u✝ = u✝) hv = cons h✝ p✝
Tactic:
obtain ⟨rfl, rfl⟩ := ih he
Proof state after:
case cons.cons.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
h' : G.Adj w✝ w
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ w✝}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
he : concat p✝ h = concat (Walk.copy p✝ (_ : v✝ = v✝) (_ : w✝ = w✝)) h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝) (_ : u✝ = u✝) hv = cons h✝ (Walk.copy p✝ (_ : v✝ = v✝) (_ : w✝ = w✝))
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons.cons.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
h' : G.Adj w✝ w
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ w✝}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
he : concat p✝ h = concat (Walk.copy p✝ (_ : v✝ = v✝) (_ : w✝ = w✝)) h'
⊢ ∃ hv, Walk.copy (cons h✝¹ p✝) (_ : u✝ = u✝) hv = cons h✝ (Walk.copy p✝ (_ : v✝ = v✝) (_ : w✝ = w✝))
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: Digraph.Walk.support_concat
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
h : G.Adj v w
⊢ support (concat p h) = List.concat (support p) w
Tactic:
induction p <;> simp [*, concat_nil]
Proof state after:
no goals
Theorem: Digraph.Walk.support_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' : V
p : Walk G u v
hu : u = u'
hv : v = v'
⊢ support (Walk.copy p hu hv) = support p
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ support (Walk.copy p (_ : u' = u') (_ : v' = v')) = support p
Theorem: Digraph.Walk.support_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ support (Walk.copy p (_ : u' = u') (_ : v' = v')) = support p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.support_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ support (append p p') = support p ++ List.tail (support p')
Tactic:
induction p <;> cases p' <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.support_ne_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ support p ≠ []
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.tail_support_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ List.tail (support (append p p')) = List.tail (support p) ++ List.tail (support p')
Tactic:
rw [support_append, List.tail_append_of_ne_nil _ _ (support_ne_nil _)]
Proof state after:
no goals
Theorem: Digraph.Walk.support_eq_cons
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ support p = u :: List.tail (support p)
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.start_mem_support
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ u ∈ support p
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.end_mem_support
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ v ∈ support p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.support_nonempty
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ u ∈ {w | w ∈ support p}
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
⊢ w ∈ support p ↔ w = u ∨ w ∈ List.tail (support p)
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_nil_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ u ∈ support nil ↔ u = v
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.mem_tail_support_append_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
⊢ t ∈ List.tail (support (append p p')) ↔ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p')
Tactic:
rw [tail_support_append, List.mem_append]
Proof state after:
no goals
Theorem: Digraph.Walk.end_mem_tail_support_of_ne
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
p : Walk G u v
⊢ v ∈ List.tail (support p)
Tactic:
obtain ⟨_, _, _, rfl⟩ := exists_eq_cons_of_ne h p
Proof state after:
case intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
w✝² : V
w✝¹ : G.Adj u w✝²
w✝ : Walk G w✝² v
⊢ v ∈ List.tail (support (cons w✝¹ w✝))
Theorem: Digraph.Walk.end_mem_tail_support_of_ne
Proof state before:
case intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
w✝² : V
w✝¹ : G.Adj u w✝²
w✝ : Walk G w✝² v
⊢ v ∈ List.tail (support (cons w✝¹ w✝))
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_append_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
⊢ t ∈ support (append p p') ↔ t ∈ support p ∨ t ∈ support p'
Tactic:
simp only [mem_support_iff, mem_tail_support_append_iff]
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Theorem: Digraph.Walk.mem_support_append_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Tactic:
obtain rfl | h := eq_or_ne t v <;> obtain rfl | h' := eq_or_ne t u <;>
  (try have := h'.symm) <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_append_iff
Proof state before:
case inr.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Tactic:
try have := h'.symm
Proof state after:
case inr.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
h : t ≠ v
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Theorem: Digraph.Walk.mem_support_append_iff
Proof state before:
case inr.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Tactic:
have := h'.symm
Proof state after:
case inr.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
t u v w : V
p : Walk G u v
p' : Walk G v w
h : t ≠ v
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ List.tail (support p) ∨ t ∈ List.tail (support p') ↔
    (t = u ∨ t ∈ List.tail (support p)) ∨ t = v ∨ t ∈ List.tail (support p')
Theorem: Digraph.Walk.subset_support_append_left
Proof state before:
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
q : Walk G v w
⊢ support p ⊆ support (append p q)
Tactic:
simp only [Walk.support_append, List.subset_append_left]
Proof state after:
no goals
Theorem: Digraph.Walk.subset_support_append_right
Proof state before:
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
q : Walk G v w
⊢ support q ⊆ support (append p q)
Tactic:
intro h
Proof state after:
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
q : Walk G v w
h : V
⊢ h ∈ support q → h ∈ support (append p q)
Theorem: Digraph.Walk.subset_support_append_right
Proof state before:
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
q : Walk G v w
h : V
⊢ h ∈ support q → h ∈ support (append p q)
Tactic:
simp (config := { contextual := true }) only [mem_support_append_iff, or_true_iff, imp_true_iff]
Proof state after:
no goals
Theorem: Digraph.Walk.coe_support
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ ↑(support p) = {u} + ↑(List.tail (support p))
Tactic:
cases p <;> rfl
Proof state after:
no goals
Theorem: Digraph.Walk.coe_support_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ ↑(support (append p p')) = {u} + ↑(List.tail (support p)) + ↑(List.tail (support p'))
Tactic:
rw [support_append, ← Multiset.coe_add, coe_support]
Proof state after:
no goals
Theorem: Digraph.Walk.coe_support_append'
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ ↑(support (append p p')) = ↑(support p) + ↑(support p') - {v}
Tactic:
rw [support_append, ← Multiset.coe_add]
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ ↑(support p) + ↑(List.tail (support p')) = ↑(support p) + ↑(support p') - {v}
Theorem: Digraph.Walk.coe_support_append'
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ ↑(support p) + ↑(List.tail (support p')) = ↑(support p) + ↑(support p') - {v}
Tactic:
simp only [coe_support]
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ {u} + ↑(List.tail (support p)) + ↑(List.tail (support p')) =
    {u} + ↑(List.tail (support p)) + ({v} + ↑(List.tail (support p'))) - {v}
Theorem: Digraph.Walk.coe_support_append'
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ {u} + ↑(List.tail (support p)) + ↑(List.tail (support p')) =
    {u} + ↑(List.tail (support p)) + ({v} + ↑(List.tail (support p'))) - {v}
Tactic:
rw [add_comm ({v} : Multiset V)]
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ {u} + ↑(List.tail (support p)) + ↑(List.tail (support p')) =
    {u} + ↑(List.tail (support p)) + (↑(List.tail (support p')) + {v}) - {v}
Theorem: Digraph.Walk.coe_support_append'
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ {u} + ↑(List.tail (support p)) + ↑(List.tail (support p')) =
    {u} + ↑(List.tail (support p)) + (↑(List.tail (support p')) + {v}) - {v}
Tactic:
simp only [← add_assoc, add_tsub_cancel_right]
Proof state after:
no goals
Theorem: Digraph.Walk.edges_subset_edgeSet
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
h : e ∈ edges (cons h' p')
⊢ e ∈ edgeSet G
Tactic:
cases h
Proof state after:
case head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
⊢ (u, v✝) ∈ edgeSet G

case tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
a✝ : List.Mem e (edges p')
⊢ e ∈ edgeSet G
Theorem: Digraph.Walk.edges_subset_edgeSet
Proof state before:
case tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
a✝ : List.Mem e (edges p')
⊢ e ∈ edgeSet G
Tactic:
next h' => exact edges_subset_edgeSet p' h'
Proof state after:
no goals
Theorem: Digraph.Walk.edges_subset_edgeSet
Proof state before:
case head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
⊢ (u, v✝) ∈ edgeSet G
Tactic:
exact h'
Proof state after:
no goals
Theorem: Digraph.Walk.edges_subset_edgeSet
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h'✝ : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
h' : List.Mem e (edges p')
⊢ e ∈ edgeSet G
Tactic:
exact edges_subset_edgeSet p' h'
Proof state after:
no goals
Theorem: Digraph.Walk.edges_concat
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
h : G.Adj v w
⊢ edges (concat p h) = List.concat (edges p) (v, w)
Tactic:
induction p <;> simp [*, concat_nil]
Proof state after:
no goals
Theorem: Digraph.Walk.edges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' : V
p : Walk G u v
hu : u = u'
hv : v = v'
⊢ edges (Walk.copy p hu hv) = edges p
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) = edges p
Theorem: Digraph.Walk.edges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) = edges p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.edges_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
p' : Walk G v w
⊢ edges (append p p') = edges p ++ edges p'
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.cons_map_snd_edges
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ u :: List.map (fun x => x.snd) (edges p) = support p
Tactic:
induction p <;> simp! [*]
Proof state after:
no goals