internlm/Lean-Github huggingface dataset:
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
⊢ List.Nodup (List.tail (support (rotate c h)))
Tactic:
rw [List.IsRotated.nodup_iff (support_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 c))
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
⊢ List.Nodup (List.tail (support c))
Tactic:
exact hc.support_nodup
Proof state after:
no goals
Theorem: Digraph.Walk.exists_boundary_dart
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
S : Set V
uS : u ∈ S
vS : ¬v ∈ S
⊢ ∃ e, e ∈ edges p ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
induction' p with _ x y w a 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''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ e, e ∈ edges nil ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Theorem: Digraph.Walk.exists_boundary_dart
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ e, e ∈ edges nil ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
cases vS uS
Proof state after:
no goals
Theorem: Digraph.Walk.exists_boundary_dart
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
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
by_cases h : y ∈ S
Proof state after:
case pos
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

case neg
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Theorem: Digraph.Walk.exists_boundary_dart
Proof state before:
case pos
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS
Proof state after:
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : V × V
hd : d ∈ edges p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Theorem: Digraph.Walk.exists_boundary_dart
Proof state before:
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : V × V
hd : d ∈ edges p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
exact ⟨d, List.Mem.tail _ hd, hcd⟩
Proof state after:
no goals
Theorem: Digraph.Walk.exists_boundary_dart
Proof state before:
case neg
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
exact ⟨(x, y), List.Mem.head _, uS, h⟩
Proof state after:
no goals
Theorem: Digraph.Path.mk'_mem_edges_singleton
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 : G.Adj u v
hne : u ≠ v
⊢ (u, v) ∈ Walk.edges ↑(singleton h hne)
Tactic:
simp [singleton]
Proof state after:
no goals
Theorem: Digraph.Path.count_edges_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 : V
p : Path G u v
e : V × V
hw : e ∈ Walk.edges ↑p
⊢ List.count e (Walk.edges ↑p) = 1
Tactic:
simpa using List.count_eq_one_of_mem p.property.isTrail.edges_nodup hw
Proof state after:
no goals
Theorem: Digraph.Path.loop_eq
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v : V
p : Path G v v
⊢ p = Path.nil
Tactic:
obtain ⟨_ | _, h⟩ := p
Proof state after:
case mk.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v : V
h : Walk.IsPath Walk.nil
⊢ { val := Walk.nil, property := h } = Path.nil

case mk.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
h : Walk.IsPath (Walk.cons h✝ p✝)
⊢ { val := Walk.cons h✝ p✝, property := h } = Path.nil
Theorem: Digraph.Path.loop_eq
Proof state before:
case mk.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v : V
h : Walk.IsPath Walk.nil
⊢ { val := Walk.nil, property := h } = Path.nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Path.loop_eq
Proof state before:
case mk.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v v✝ : V
h✝ : G.Adj v v✝
p✝ : Walk G v✝ v
h : Walk.IsPath (Walk.cons h✝ p✝)
⊢ { val := Walk.cons h✝ p✝, property := h } = Path.nil
Tactic:
simp at h
Proof state after:
no goals
Theorem: Digraph.Path.not_mem_edges_of_loop
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v : V
e : V × V
p : Path G v v
⊢ ¬e ∈ Walk.edges ↑p
Tactic:
simp [p.loop_eq]
Proof state after:
no goals
Theorem: Digraph.Path.cons_isCycle
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 : Path G v u
h : G.Adj u v
he : ¬(u, v) ∈ Walk.edges ↑p
⊢ Walk.IsCycle (Walk.cons h ↑p)
Tactic:
simp [Walk.isCycle_def, Walk.cons_isTrail_iff, he]
Proof state after:
no goals
Theorem: Digraph.Walk.bypass_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 u' v' : V
p : Walk G u v
hu : u = u'
hv : v = v'
⊢ bypass (Walk.copy p hu hv) = Walk.copy (bypass p) hu hv
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' : V
p : Walk G u' v'
⊢ bypass (Walk.copy p (_ : u' = u') (_ : v' = v')) = Walk.copy (bypass p) (_ : u' = u') (_ : v' = v')
Theorem: Digraph.Walk.bypass_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' : V
p : Walk G u' v'
⊢ bypass (Walk.copy p (_ : u' = u') (_ : v' = v')) = Walk.copy (bypass p) (_ : u' = u') (_ : v' = v')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.bypass_isPath
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 u✝ : V
⊢ IsPath (bypass nil)
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.bypass_isPath
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
⊢ IsPath (bypass (cons h✝ p'))
Tactic:
simp only [bypass]
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
⊢ IsPath (if hs : u✝ ∈ support (bypass p') then dropUntil (bypass p') u✝ hs else cons h✝ (bypass p'))
Theorem: Digraph.Walk.bypass_isPath
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
⊢ IsPath (if hs : u✝ ∈ support (bypass p') then dropUntil (bypass p') u✝ hs else cons h✝ (bypass p'))
Tactic:
split_ifs with hs
Proof state after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
hs : u✝ ∈ support (bypass p')
⊢ IsPath (dropUntil (bypass p') u✝ hs)

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
hs : ¬u✝ ∈ support (bypass p')
⊢ IsPath (cons h✝ (bypass p'))
Theorem: Digraph.Walk.bypass_isPath
Proof state before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
hs : u✝ ∈ support (bypass p')
⊢ IsPath (dropUntil (bypass p') u✝ hs)
Tactic:
exact ih.dropUntil hs
Proof state after:
no goals
Theorem: Digraph.Walk.bypass_isPath
Proof state before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : IsPath (bypass p')
hs : ¬u✝ ∈ support (bypass p')
⊢ IsPath (cons h✝ (bypass p'))
Tactic:
simp [*, cons_isPath_iff]
Proof state after:
no goals
Theorem: Digraph.Walk.length_bypass_le
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 u✝ : V
⊢ length (bypass nil) ≤ length nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.length_bypass_le
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (bypass (cons h✝ p✝)) ≤ length (cons h✝ p✝)
Tactic:
simp only [bypass]
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ≤
    length (cons h✝ p✝)
Theorem: Digraph.Walk.length_bypass_le
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ≤
    length (cons h✝ p✝)
Tactic:
split_ifs
Proof state after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ length (cons h✝¹ p✝)

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (cons h✝¹ (bypass p✝)) ≤ length (cons h✝¹ p✝)
Theorem: Digraph.Walk.length_bypass_le
Proof state before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ length (cons h✝¹ p✝)
Tactic:
trans
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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ ?m.249227

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ?m.249227 ≤ length (cons h✝¹ p✝)

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ
Theorem: Digraph.Walk.length_bypass_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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ ?m.249227

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ?m.249227 ≤ length (cons h✝¹ p✝)

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ
Tactic:
apply length_dropUntil_le
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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length (cons h✝¹ p✝)
Theorem: Digraph.Walk.length_bypass_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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length (cons h✝¹ p✝)
Tactic:
rw [length_cons]
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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1
Theorem: Digraph.Walk.length_bypass_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 u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1
Tactic:
exact le_add_right ih
Proof state after:
no goals
Theorem: Digraph.Walk.length_bypass_le
Proof state before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (cons h✝¹ (bypass p✝)) ≤ length (cons h✝¹ p✝)
Tactic:
rw [length_cons, length_cons]
Proof state after:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) + 1 ≤ length p✝ + 1
Theorem: Digraph.Walk.length_bypass_le
Proof state before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) + 1 ≤ length p✝ + 1
Tactic:
exact add_le_add_right ih 1
Proof state after:
no goals
Theorem: Digraph.Walk.support_bypass_subset
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 u✝ : V
⊢ support (bypass nil) ⊆ support nil
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.support_bypass_subset
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (bypass (cons h✝ p✝)) ⊆ support (cons h✝ p✝)
Tactic:
simp! only
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    u✝ :: support p✝
Theorem: Digraph.Walk.support_bypass_subset
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    u✝ :: support p✝
Tactic:
split_ifs
Proof state after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (dropUntil (bypass p✝) u✝ h✝) ⊆ u✝ :: support p✝

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (cons h✝¹ (bypass p✝)) ⊆ u✝ :: support p✝
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (dropUntil (bypass p✝) u✝ h✝) ⊆ u✝ :: support p✝
Tactic:
apply List.Subset.trans (support_dropUntil_subset _ _)
Proof state after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ u✝ :: support p✝
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ u✝ :: support p✝
Tactic:
apply List.subset_cons_of_subset
Proof state after:
case cons.inl.a
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inl.a
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (cons h✝¹ (bypass p✝)) ⊆ u✝ :: support p✝
Tactic:
rw [support_cons]
Proof state after:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ u✝ :: support (bypass p✝) ⊆ u✝ :: support p✝
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ u✝ :: support (bypass p✝) ⊆ u✝ :: support p✝
Tactic:
apply List.cons_subset_cons
Proof state after:
case cons.inr.s
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
Theorem: Digraph.Walk.support_bypass_subset
Proof state before:
case cons.inr.s
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Digraph.Walk.edges_bypass_subset
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 u✝ : V
⊢ edges (bypass nil) ⊆ edges nil
Tactic:
simp!
Proof state after:
no goals
Theorem: Digraph.Walk.edges_bypass_subset
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
⊢ edges (bypass (cons h✝ p✝)) ⊆ edges (cons h✝ p✝)
Tactic:
simp! only
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
⊢ edges (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    (u✝, v✝) :: edges p✝