Theorem: Digraph.Walk.take_spec (GraphProjects/DigraphConnectivity.lean)

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
⊢ append (takeUntil p u h) (dropUntil p u h) = p
Tactic:
induction p
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
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil

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✝

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
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil
Tactic:
rw [mem_support_nil_iff] at h
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✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil

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✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil
Tactic:
subst u
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
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil

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
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil
Tactic:
rfl
State after:
no goals

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
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✝

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!
State after:
no goals

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
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✝

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 [*]
State after:
no goals