internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.take_spec
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h : u ∈ support (cons h✝ p✝)
⊢ append (takeUntil (cons h✝ p✝) u h) (dropUntil (cons h✝ p✝) u h) = cons h✝ p✝
Tactic:
cases h
Proof state after:
case cons.head
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✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h✝ : G.Adj u v✝
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝))) =
    cons h✝ p✝

case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝))) =
    cons h✝ p✝
Theorem: Digraph.Walk.take_spec
Proof state before:
case cons.head
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✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h✝ : G.Adj u v✝
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝))) =
    cons h✝ p✝
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.take_spec
Proof state before:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝))) =
    cons h✝ p✝
Tactic:
simp! only
Proof state after:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G x w✝) (fun h => cons h✝ p✝) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else dropUntil p✝ u (_ : u ∈ support p✝)) =
    cons h✝ p✝
Theorem: Digraph.Walk.take_spec
Proof state before:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G x w✝) (fun h => cons h✝ p✝) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else dropUntil p✝ u (_ : u ∈ support p✝)) =
    cons h✝ p✝
Tactic:
split_ifs with h' <;> subst_vars <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_iff_exists_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✝
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p ↔ ∃ q r, p = append q r
Tactic:
constructor
Proof state after:
case mp
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p → ∃ q r, p = append q r

case mpr
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
⊢ (∃ q r, p = append q r) → w ∈ support p
Theorem: Digraph.Walk.mem_support_iff_exists_append
Proof state before:
case mp
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p → ∃ q r, p = append q r
Tactic:
exact fun h => ⟨_, _, (p.take_spec h).symm⟩
Proof state after:
no goals
Theorem: Digraph.Walk.mem_support_iff_exists_append
Proof state before:
case mpr
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
p : Walk G u v
⊢ (∃ q r, p = append q r) → w ∈ support p
Tactic:
rintro ⟨q, r, rfl⟩
Proof state after:
case mpr.intro.intro
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
q : Walk G u w
r : Walk G w v
⊢ w ∈ support (append q r)
Theorem: Digraph.Walk.mem_support_iff_exists_append
Proof state before:
case mpr.intro.intro
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V✝
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V✝
V : Type u
G : Digraph V
u v w : V
q : Walk G u w
r : Walk G w v
⊢ w ∈ support (append q r)
Tactic:
simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]
Proof state after:
no goals
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
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 v w
h : u ∈ support p
⊢ List.count u (support (takeUntil p u h)) = 1
Tactic:
induction p
Proof state after:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ support nil
⊢ List.count u (support (takeUntil nil u h)) = 1

case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
h : u ∈ support (cons h✝ p✝)
⊢ List.count u (support (takeUntil (cons h✝ p✝) u h)) = 1
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ support nil
⊢ List.count u (support (takeUntil nil u h)) = 1
Tactic:
rw [mem_support_nil_iff] at h
Proof state after:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ support nil
h : u = u✝
⊢ List.count u (support (takeUntil nil u h✝)) = 1
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ support nil
h : u = u✝
⊢ List.count u (support (takeUntil nil u h✝)) = 1
Tactic:
subst u
Proof state after:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ support nil
⊢ List.count u✝ (support (takeUntil nil u✝ h)) = 1
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ support nil
⊢ List.count u✝ (support (takeUntil nil u✝ h)) = 1
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
h : u ∈ support (cons h✝ p✝)
⊢ List.count u (support (takeUntil (cons h✝ p✝) u h)) = 1
Tactic:
cases h
Proof state after:
case cons.head
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✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
h✝ : G.Adj u v✝
⊢ List.count u (support (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))) = 1

case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
a✝ : List.Mem u (support p✝)
⊢ List.count u (support (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))) = 1
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case cons.head
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✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
h✝ : G.Adj u v✝
⊢ List.count u (support (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))) = 1
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
a✝ : List.Mem u (support p✝)
⊢ List.count u (support (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))) = 1
Tactic:
simp! only
Proof state after:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
a✝ : List.Mem u (support p✝)
⊢ List.count u
      (support
        (if h : u✝ = u then
          Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
            (_ : List.Mem u (u✝ :: support p✝))
        else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))) =
    1
Theorem: Digraph.Walk.count_support_takeUntil_eq_one
Proof state before:
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
a✝ : List.Mem u (support p✝)
⊢ List.count u
      (support
        (if h : u✝ = u then
          Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
            (_ : List.Mem u (u✝ :: support p✝))
        else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))) =
    1
Tactic:
split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]
Proof state after:
no goals
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
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 v w
h : u ∈ support p
x : V
⊢ List.count (u, x) (edges (takeUntil p u h)) = 0
Tactic:
induction' p with u' u' v' w' ha p' ih
Proof state after:
case nil
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 v w
h✝ : u ∈ support p
x u' : V
h : u ∈ support nil
⊢ List.count (u, x) (edges (takeUntil nil u h)) = 0

case cons
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 v w
h✝ : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
h : u ∈ support (cons ha p')
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u h)) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case nil
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 v w
h✝ : u ∈ support p
x u' : V
h : u ∈ support nil
⊢ List.count (u, x) (edges (takeUntil nil u h)) = 0
Tactic:
rw [mem_support_nil_iff] at h
Proof state after:
case nil
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 v w
h✝¹ : u ∈ support p
x u' : V
h✝ : u ∈ support nil
h : u = u'
⊢ List.count (u, x) (edges (takeUntil nil u h✝)) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case nil
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 v w
h✝¹ : u ∈ support p
x u' : V
h✝ : u ∈ support nil
h : u = u'
⊢ List.count (u, x) (edges (takeUntil nil u h✝)) = 0
Tactic:
subst u
Proof state after:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' : V
h✝ : u' ∈ support p
h : u' ∈ support nil
⊢ List.count (u', x) (edges (takeUntil nil u' h)) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' : V
h✝ : u' ∈ support p
h : u' ∈ support nil
⊢ List.count (u', x) (edges (takeUntil nil u' h)) = 0
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons
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 v w
h✝ : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
h : u ∈ support (cons ha p')
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u h)) = 0
Tactic:
cases h
Proof state after:
case cons.head
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 v w
h : u ∈ support p
x v' w' : V
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
ha : G.Adj u v'
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u (_ : List.Mem u (u :: support p')))) = 0

case cons.tail
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u (_ : List.Mem u (u' :: support p')))) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.head
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 v w
h : u ∈ support p
x v' w' : V
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
ha : G.Adj u v'
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u (_ : List.Mem u (u :: support p')))) = 0
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u (_ : List.Mem u (u' :: support p')))) = 0
Tactic:
simp! only
Proof state after:
case cons.tail
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
⊢ List.count (u, x)
      (edges
        (if h : u' = u then
          Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
            (_ : List.Mem u (u' :: support p'))
        else cons ha (takeUntil p' u (_ : u ∈ support p')))) =
    0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
⊢ List.count (u, x)
      (edges
        (if h : u' = u then
          Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
            (_ : List.Mem u (u' :: support p'))
        else cons ha (takeUntil p' u (_ : u ∈ support p')))) =
    0
Tactic:
split_ifs with h'
Proof state after:
case cons.tail.inl
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : u' = u
⊢ List.count (u, x)
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
          (_ : List.Mem u (u' :: support p')))) =
    0

case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (u, x) (edges (cons ha (takeUntil p' u (_ : u ∈ support p')))) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inl
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : u' = u
⊢ List.count (u, x)
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
          (_ : List.Mem u (u' :: support p')))) =
    0
Tactic:
subst h'
Proof state after:
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
h : u' ∈ support p
ih : ∀ (h : u' ∈ support p'), List.count (u', x) (edges (takeUntil p' u' h)) = 0
a✝ : List.Mem u' (support p')
⊢ List.count (u', x)
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u')
          (_ : List.Mem u' (u' :: support p')))) =
    0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
h : u' ∈ support p
ih : ∀ (h : u' ∈ support p'), List.count (u', x) (edges (takeUntil p' u' h)) = 0
a✝ : List.Mem u' (support p')
⊢ List.count (u', x)
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u')
          (_ : List.Mem u' (u' :: support p')))) =
    0
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (u, x) (edges (cons ha (takeUntil p' u (_ : u ∈ support p')))) = 0
Tactic:
rw [edges_cons]
Proof state after:
case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (u, x) ((u', v') :: edges (takeUntil p' u (_ : u ∈ support p'))) = 0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (u, x) ((u', v') :: edges (takeUntil p' u (_ : u ∈ support p'))) = 0
Tactic:
simp only [List.count_prod_eq, List.count_cons]
Proof state after:
case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ (if (u, x) = (u', v') then Nat.succ (List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p'))))
    else List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p')))) =
    0
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ (if (u, x) = (u', v') then Nat.succ (List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p'))))
    else List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p')))) =
    0
Tactic:
split_ifs with h''
Proof state after:
case cons.tail.inr.inl
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : (u, x) = (u', v')
⊢ False

case cons.tail.inr.inr
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 v w
h : u ∈ support p
x u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : ¬(u, x) = (u', v')
⊢ List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p'))) = 0