internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
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
Tactic:
simp at 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 = u' ∧ x = v'
⊢ False
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
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 = u' ∧ x = v'
⊢ False
Tactic:
obtain ⟨rfl, rfl⟩ := h''
Proof state after:
case cons.tail.inr.inl.intro
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 w' : V
h' : ¬u = u
p' : Walk G x w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
ha : G.Adj u x
⊢ False
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
case cons.tail.inr.inl.intro
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 w' : V
h' : ¬u = u
p' : Walk G x w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
ha : G.Adj u x
⊢ False
Tactic:
exact (h' rfl).elim
Proof state after:
no goals
Theorem: Digraph.Walk.count_edges_takeUntil_eq_zero
Proof state before:
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
Tactic:
simp only [List.count_prod_eq] at ih
Proof state after:
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'
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : ¬(u, x) = (u', v')
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
⊢ 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.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'
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : ¬(u, x) = (u', v')
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
⊢ List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p'))) = 0
Tactic:
apply ih
Proof state after:
no goals
Theorem: Digraph.Walk.takeUntil_copy
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' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ u ∈ 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''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
Theorem: Digraph.Walk.takeUntil_copy
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 (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
Tactic:
exact h
Proof state after:
no goals
Theorem: Digraph.Walk.takeUntil_copy
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' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ takeUntil (Walk.copy p hv hw) u h = Walk.copy (takeUntil p u (_ : u ∈ support p)) hv (_ : u = u)
Tactic:
subst_vars
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 v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ takeUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (takeUntil p u (_ : u ∈ support p)) (_ : v' = v') (_ : u = u)
Theorem: Digraph.Walk.takeUntil_copy
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 (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ takeUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (takeUntil p u (_ : u ∈ support p)) (_ : v' = v') (_ : u = u)
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.dropUntil_copy
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' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ u ∈ 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''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
Theorem: Digraph.Walk.dropUntil_copy
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 (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
Tactic:
exact h
Proof state after:
no goals
Theorem: Digraph.Walk.dropUntil_copy
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' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ dropUntil (Walk.copy p hv hw) u h = Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) hw
Tactic:
subst_vars
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 v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ dropUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) (_ : w' = w')
Theorem: Digraph.Walk.dropUntil_copy
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 (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ dropUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) (_ : w' = w')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.support_takeUntil_subset
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
hx : x ∈ support (takeUntil p u h)
⊢ x ∈ support p
Tactic:
rw [← take_spec p h, mem_support_append_iff]
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 v w
h : u ∈ support p
x : V
hx : x ∈ support (takeUntil p u h)
⊢ x ∈ support (takeUntil p u h) ∨ x ∈ support (dropUntil p u h)
Theorem: Digraph.Walk.support_takeUntil_subset
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
hx : x ∈ support (takeUntil p u h)
⊢ x ∈ support (takeUntil p u h) ∨ x ∈ support (dropUntil p u h)
Tactic:
exact Or.inl hx
Proof state after:
no goals
Theorem: Digraph.Walk.support_dropUntil_subset
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
hx : x ∈ support (dropUntil p u h)
⊢ x ∈ support p
Tactic:
rw [← take_spec p h, mem_support_append_iff]
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 v w
h : u ∈ support p
x : V
hx : x ∈ support (dropUntil p u h)
⊢ x ∈ support (takeUntil p u h) ∨ x ∈ support (dropUntil p u h)
Theorem: Digraph.Walk.support_dropUntil_subset
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
hx : x ∈ support (dropUntil p u h)
⊢ x ∈ support (takeUntil p u h) ∨ x ∈ support (dropUntil p u h)
Tactic:
exact Or.inr hx
Proof state after:
no goals
Theorem: Digraph.Walk.edges_takeUntil_subset
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 × V
hx : x ∈ edges (takeUntil p u h)
⊢ x ∈ edges p
Tactic:
rw [← take_spec p h, edges_append, List.mem_append]
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 v w
h : u ∈ support p
x : V × V
hx : x ∈ edges (takeUntil p u h)
⊢ x ∈ edges (takeUntil p u h) ∨ x ∈ edges (dropUntil p u h)
Theorem: Digraph.Walk.edges_takeUntil_subset
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 × V
hx : x ∈ edges (takeUntil p u h)
⊢ x ∈ edges (takeUntil p u h) ∨ x ∈ edges (dropUntil p u h)
Tactic:
exact Or.inl hx
Proof state after:
no goals
Theorem: Digraph.Walk.edges_dropUntil_subset
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 × V
hx : x ∈ edges (dropUntil p u h)
⊢ x ∈ edges p
Tactic:
rw [← take_spec p h, edges_append, List.mem_append]
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 v w
h : u ∈ support p
x : V × V
hx : x ∈ edges (dropUntil p u h)
⊢ x ∈ edges (takeUntil p u h) ∨ x ∈ edges (dropUntil p u h)
Theorem: Digraph.Walk.edges_dropUntil_subset
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 × V
hx : x ∈ edges (dropUntil p u h)
⊢ x ∈ edges (takeUntil p u h) ∨ x ∈ edges (dropUntil p u h)
Tactic:
exact Or.inr hx
Proof state after:
no goals
Theorem: Digraph.Walk.length_takeUntil_le
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
⊢ length (takeUntil p u h) ≤ length p
Tactic:
have := congr_arg Walk.length (p.take_spec h)
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 v w
h : u ∈ support p
this : length (append (takeUntil p u h) (dropUntil p u h)) = length p
⊢ length (takeUntil p u h) ≤ length p
Theorem: Digraph.Walk.length_takeUntil_le
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
this : length (append (takeUntil p u h) (dropUntil p u h)) = length p
⊢ length (takeUntil p u h) ≤ length p
Tactic:
rw [length_append] at this
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 v w
h : u ∈ support p
this : length (takeUntil p u h) + length (dropUntil p u h) = length p
⊢ length (takeUntil p u h) ≤ length p
Theorem: Digraph.Walk.length_takeUntil_le
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
this : length (takeUntil p u h) + length (dropUntil p u h) = length p
⊢ length (takeUntil p u h) ≤ length p
Tactic:
exact Nat.le.intro this
Proof state after:
no goals
Theorem: Digraph.Walk.length_dropUntil_le
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
⊢ length (dropUntil p u h) ≤ length p
Tactic:
have := congr_arg Walk.length (p.take_spec h)
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 v w
h : u ∈ support p
this : length (append (takeUntil p u h) (dropUntil p u h)) = length p
⊢ length (dropUntil p u h) ≤ length p
Theorem: Digraph.Walk.length_dropUntil_le
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
this : length (append (takeUntil p u h) (dropUntil p u h)) = length p
⊢ length (dropUntil p u h) ≤ length p
Tactic:
rw [length_append, add_comm] at this
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 v w
h : u ∈ support p
this : length (dropUntil p u h) + length (takeUntil p u h) = length p
⊢ length (dropUntil p u h) ≤ length p
Theorem: Digraph.Walk.length_dropUntil_le
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
this : length (dropUntil p u h) + length (takeUntil p u h) = length p
⊢ length (dropUntil p u h) ≤ length p
Tactic:
exact Nat.le.intro this
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.takeUntil
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
hc : IsTrail p
h : u ∈ support p
⊢ IsTrail (append (takeUntil p u h) (?m.221792 hc h))
Tactic:
rwa [← take_spec _ h] at hc
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.dropUntil
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
hc : IsTrail p
h : u ∈ support p
⊢ IsTrail (append (?m.222054 hc h) (dropUntil p u h))
Tactic:
rwa [← take_spec _ h] at hc
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.takeUntil
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
hc : IsPath p
h : u ∈ support p
⊢ IsPath (append (takeUntil p u h) (?m.222316 hc h))
Tactic:
rwa [← take_spec _ h] at hc
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.dropUntil
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
hc : IsPath p
h : u ∈ support p
⊢ IsPath (append (?m.222578 hc h) (dropUntil p u h))
Tactic:
rwa [← take_spec _ h] at hc
Proof state after:
no goals
Theorem: Digraph.Walk.support_rotate
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 : V
c : Walk G v v
h : u ∈ support c
⊢ List.tail (support (rotate c h)) ~r List.tail (support c)
Tactic:
simp only [rotate, tail_support_append]
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (dropUntil c u h)) ++ List.tail (support (takeUntil c u h))) ~r List.tail (support c)
Theorem: Digraph.Walk.support_rotate
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (dropUntil c u h)) ++ List.tail (support (takeUntil c u h))) ~r List.tail (support c)
Tactic:
apply List.IsRotated.trans List.isRotated_append
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (takeUntil c u h)) ++ List.tail (support (dropUntil c u h))) ~r List.tail (support c)
Theorem: Digraph.Walk.support_rotate
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (takeUntil c u h)) ++ List.tail (support (dropUntil c u h))) ~r List.tail (support c)
Tactic:
rw [← tail_support_append, take_spec]
Proof state after:
no goals
Theorem: Digraph.Walk.rotate_edges
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 : V
c : Walk G v v
h : u ∈ support c
⊢ edges (rotate c h) ~r edges c
Tactic:
simp only [rotate, edges_append]
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (edges (dropUntil c u h) ++ edges (takeUntil c u h)) ~r edges c
Theorem: Digraph.Walk.rotate_edges
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (edges (dropUntil c u h) ++ edges (takeUntil c u h)) ~r edges c
Tactic:
apply List.IsRotated.trans List.isRotated_append
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (edges (takeUntil c u h) ++ edges (dropUntil c u h)) ~r edges c
Theorem: Digraph.Walk.rotate_edges
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 : V
c : Walk G v v
h : u ∈ support c
⊢ (edges (takeUntil c u h) ++ edges (dropUntil c u h)) ~r edges c
Tactic:
rw [← edges_append, take_spec]
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.rotate
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 : V
c : Walk G v v
hc : IsTrail c
h : u ∈ support c
⊢ IsTrail (rotate c h)
Tactic:
rw [isTrail_def, (c.rotate_edges h).perm.nodup_iff]
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 : V
c : Walk G v v
hc : IsTrail c
h : u ∈ support c
⊢ List.Nodup (edges c)
Theorem: Digraph.Walk.IsTrail.rotate
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 : V
c : Walk G v v
hc : IsTrail c
h : u ∈ support c
⊢ List.Nodup (edges c)
Tactic:
exact hc.edges_nodup
Proof state after:
no goals
Theorem: Digraph.Walk.IsCircuit.rotate
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 : V
c : Walk G v v
hc : IsCircuit c
h : u ∈ support c
⊢ IsCircuit (rotate c h)
Tactic:
refine ⟨hc.isTrail.rotate _, ?_⟩
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 : V
c : Walk G v v
hc : IsCircuit c
h : u ∈ support c
⊢ rotate c h ≠ nil
Theorem: Digraph.Walk.IsCircuit.rotate
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 : V
c : Walk G v v
hc : IsCircuit c
h : u ∈ support c
⊢ rotate c h ≠ nil
Tactic:
cases c
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 : V
hc : IsCircuit nil
h : u ∈ support nil
⊢ rotate nil 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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
⊢ rotate (cons h✝ p✝) h ≠ nil
Theorem: Digraph.Walk.IsCircuit.rotate
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 : V
hc : IsCircuit nil
h : u ∈ support nil
⊢ rotate nil h ≠ nil
Tactic:
exact (hc.ne_nil rfl).elim
Proof state after:
no goals
Theorem: Digraph.Walk.IsCircuit.rotate
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
⊢ rotate (cons h✝ p✝) h ≠ nil
Tactic:
intro hn
Proof state after:
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
⊢ False
Theorem: Digraph.Walk.IsCircuit.rotate
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
⊢ False
Tactic:
have hn' := congr_arg length hn
Proof state after:
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
hn' : length (rotate (cons h✝ p✝) h) = length nil
⊢ False
Theorem: Digraph.Walk.IsCircuit.rotate
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
hn' : length (rotate (cons h✝ p✝) h) = length nil
⊢ False
Tactic:
rw [rotate, length_append, add_comm, ← length_append, take_spec] at hn'
Proof state after:
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
hn' : length (cons h✝ p✝) = length nil
⊢ False
Theorem: Digraph.Walk.IsCircuit.rotate
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 v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
hc : IsCircuit (cons h✝ p✝)
h : u ∈ support (cons h✝ p✝)
hn : rotate (cons h✝ p✝) h = nil
hn' : length (cons h✝ p✝) = length nil
⊢ False
Tactic:
simp at hn'
Proof state after:
no goals
Theorem: Digraph.Walk.IsCycle.rotate
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 : V
c : Walk G v v
hc : IsCycle c
h : u ∈ support c
⊢ IsCycle (rotate c h)
Tactic:
refine ⟨hc.isCircuit.rotate _, ?_⟩
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 : V
c : Walk G v v
hc : IsCycle c
h : u ∈ support c
⊢ List.Nodup (List.tail (support (rotate c h)))