internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.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
⊢ List.map (fun x => x.snd) (edges p) = List.tail (support p)
Tactic:
simpa using congr_arg List.tail (cons_map_snd_edges p)
Proof state after:
no goals
Theorem: Digraph.Walk.map_fst_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 : V
p : Walk G u v
⊢ List.map (fun x => x.fst) (edges p) ++ [v] = support p
Tactic:
induction p <;> simp! [*]
Proof state after:
no goals
Theorem: Digraph.Walk.map_fst_darts
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
⊢ List.map (fun x => x.fst) (edges p) = List.dropLast (support p)
Tactic:
simpa! using congr_arg List.dropLast (map_fst_edges_append p)
Proof state after:
no goals
Theorem: Digraph.Walk.length_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
⊢ List.length (support p) = length p + 1
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.length_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
⊢ List.length (edges p) = length p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.edges_fst_mem_support_of_mem_darts
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
d : V × V
hd : d ∈ edges (cons h p')
⊢ d.fst ∈ support (cons h p')
Tactic:
simp only [support_cons, edges_cons, List.mem_cons] at hd ⊢
Proof state after:
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
d : V × V
hd : d = (u, v✝) ∨ d ∈ edges p'
⊢ d.fst = u ∨ d.fst ∈ support p'
Theorem: Digraph.Walk.edges_fst_mem_support_of_mem_darts
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
d : V × V
hd : d = (u, v✝) ∨ d ∈ edges p'
⊢ d.fst = u ∨ d.fst ∈ support p'
Tactic:
rcases hd with (rfl | hd)
Proof state after:
case inl
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✝).fst = u ∨ (u, v✝).fst ∈ support p'

case inr
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
d : V × V
hd : d ∈ edges p'
⊢ d.fst = u ∨ d.fst ∈ support p'
Theorem: Digraph.Walk.edges_fst_mem_support_of_mem_darts
Proof state before:
case inl
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✝).fst = u ∨ (u, v✝).fst ∈ support p'
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: Digraph.Walk.edges_fst_mem_support_of_mem_darts
Proof state before:
case inr
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
d : V × V
hd : d ∈ edges p'
⊢ d.fst = u ∨ d.fst ∈ support p'
Tactic:
exact Or.inr (edges_fst_mem_support_of_mem_darts _ hd)
Proof state after:
no goals
Theorem: Digraph.Walk.edges_snd_mem_support_of_mem_darts
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
d : V × V
hd : d ∈ edges (cons h p')
⊢ d.snd ∈ support (cons h p')
Tactic:
simp only [support_cons, edges_cons, List.mem_cons] at hd ⊢
Proof state after:
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
d : V × V
hd : d = (u, v✝) ∨ d ∈ edges p'
⊢ d.snd = u ∨ d.snd ∈ support p'
Theorem: Digraph.Walk.edges_snd_mem_support_of_mem_darts
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
d : V × V
hd : d = (u, v✝) ∨ d ∈ edges p'
⊢ d.snd = u ∨ d.snd ∈ support p'
Tactic:
rcases hd with (rfl | hd)
Proof state after:
case inl
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✝).snd = u ∨ (u, v✝).snd ∈ support p'

case inr
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
d : V × V
hd : d ∈ edges p'
⊢ d.snd = u ∨ d.snd ∈ support p'
Theorem: Digraph.Walk.edges_snd_mem_support_of_mem_darts
Proof state before:
case inl
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✝).snd = u ∨ (u, v✝).snd ∈ support p'
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.edges_snd_mem_support_of_mem_darts
Proof state before:
case inr
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
d : V × V
hd : d ∈ edges p'
⊢ d.snd = u ∨ d.snd ∈ support p'
Tactic:
exact Or.inr (edges_snd_mem_support_of_mem_darts _ hd)
Proof state after:
no goals
Theorem: Digraph.Walk.fst_mem_support_of_mem_edges
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 v w
he : (t, u) ∈ edges p
⊢ t ∈ support p
Tactic:
exact edges_fst_mem_support_of_mem_darts _ he
Proof state after:
no goals
Theorem: Digraph.Walk.snd_mem_support_of_mem_edges
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 v w
he : (t, u) ∈ edges p
⊢ u ∈ support p
Tactic:
exact edges_snd_mem_support_of_mem_darts _ he
Proof state after:
no goals
Theorem: Digraph.Walk.edges_nodup_of_support_nodup
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
h : List.Nodup (support p)
⊢ List.Nodup (edges p)
Tactic:
induction p with
| nil => simp
| cons _ p' ih =>
  simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
  exact ⟨fun h' => h.1 (edges_fst_mem_support_of_mem_darts p' h'), ih h.2⟩
Proof state after:
no goals
Theorem: Digraph.Walk.edges_nodup_of_support_nodup
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 u✝ : V
h : List.Nodup (support nil)
⊢ List.Nodup (edges nil)
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.edges_nodup_of_support_nodup
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : List.Nodup (support (cons h✝ p'))
⊢ List.Nodup (edges (cons h✝ p'))
Tactic:
simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
Proof state after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬(u✝, v✝) ∈ edges p' ∧ List.Nodup (edges p')
Theorem: Digraph.Walk.edges_nodup_of_support_nodup
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬(u✝, v✝) ∈ edges p' ∧ List.Nodup (edges p')
Tactic:
exact ⟨fun h' => h.1 (edges_fst_mem_support_of_mem_darts p' h'), ih h.2⟩
Proof state after:
no goals
Theorem: Digraph.Walk.isTrail_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'
⊢ IsTrail (Walk.copy p hu hv) ↔ IsTrail 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'
⊢ IsTrail (Walk.copy p (_ : u' = u') (_ : v' = v')) ↔ IsTrail p
Theorem: Digraph.Walk.isTrail_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'
⊢ IsTrail (Walk.copy p (_ : u' = u') (_ : v' = v')) ↔ IsTrail p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.isPath_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'
⊢ IsPath (Walk.copy p hu hv) ↔ IsPath 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'
⊢ IsPath (Walk.copy p (_ : u' = u') (_ : v' = v')) ↔ IsPath p
Theorem: Digraph.Walk.isPath_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'
⊢ IsPath (Walk.copy p (_ : u' = u') (_ : v' = v')) ↔ IsPath p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.isCircuit_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u u' : V
p : Walk G u u
hu : u = u'
⊢ IsCircuit (Walk.copy p hu hu) ↔ IsCircuit 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
p : Walk G u' u'
⊢ IsCircuit (Walk.copy p (_ : u' = u') (_ : u' = u')) ↔ IsCircuit p
Theorem: Digraph.Walk.isCircuit_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' : V
p : Walk G u' u'
⊢ IsCircuit (Walk.copy p (_ : u' = u') (_ : u' = u')) ↔ IsCircuit p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.isCycle_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u u' : V
p : Walk G u u
hu : u = u'
⊢ IsCycle (Walk.copy p hu hu) ↔ IsCycle 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
p : Walk G u' u'
⊢ IsCycle (Walk.copy p (_ : u' = u') (_ : u' = u')) ↔ IsCycle p
Theorem: Digraph.Walk.isCycle_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' : V
p : Walk G u' u'
⊢ IsCycle (Walk.copy p (_ : u' = u') (_ : u' = u')) ↔ IsCycle p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ List.Nodup (edges Walk.nil)
Tactic:
simp [edges]
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.of_cons
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
h : G.Adj u v
p : Walk G v w
⊢ IsTrail (cons h p) → IsTrail p
Tactic:
simp [isTrail_def]
Proof state after:
no goals
Theorem: Digraph.Walk.cons_isTrail_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
h : G.Adj u v
p : Walk G v w
⊢ IsTrail (cons h p) ↔ IsTrail p ∧ ¬(u, v) ∈ edges p
Tactic:
simp [isTrail_def, and_comm]
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.of_append_left
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
q : Walk G v w
h : IsTrail (append p q)
⊢ IsTrail p
Tactic:
rw [isTrail_def, edges_append, List.nodup_append] at h
Proof state after:
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
q : Walk G v w
h : List.Nodup (edges p) ∧ List.Nodup (edges q) ∧ List.Disjoint (edges p) (edges q)
⊢ IsTrail p
Theorem: Digraph.Walk.IsTrail.of_append_left
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
q : Walk G v w
h : List.Nodup (edges p) ∧ List.Nodup (edges q) ∧ List.Disjoint (edges p) (edges q)
⊢ IsTrail p
Tactic:
exact ⟨h.1⟩
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.of_append_right
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
q : Walk G v w
h : IsTrail (append p q)
⊢ IsTrail q
Tactic:
rw [isTrail_def, edges_append, List.nodup_append] at h
Proof state after:
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
q : Walk G v w
h : List.Nodup (edges p) ∧ List.Nodup (edges q) ∧ List.Disjoint (edges p) (edges q)
⊢ IsTrail q
Theorem: Digraph.Walk.IsTrail.of_append_right
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
q : Walk G v w
h : List.Nodup (edges p) ∧ List.Nodup (edges q) ∧ List.Disjoint (edges p) (edges q)
⊢ IsTrail q
Tactic:
exact ⟨h.2.1⟩
Proof state after:
no goals
Theorem: Digraph.Walk.List.count_prod_eq
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ List.count e xs = List.count e xs
Tactic:
congr!
Proof state after:
case h.e'_2
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ instBEqProd = instBEq
Theorem: Digraph.Walk.List.count_prod_eq
Proof state before:
case h.e'_2
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ instBEqProd = instBEq
Tactic:
ext p q
Proof state after:
case h.e'_2.beq.h.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e p q : V × V
⊢ (p == q) = (p == q)
Theorem: Digraph.Walk.List.count_prod_eq
Proof state before:
case h.e'_2.beq.h.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e p q : V × V
⊢ (p == q) = (p == q)
Tactic:
cases p
Proof state after:
case h.e'_2.beq.h.h.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e q : V × V
fst✝ snd✝ : V
⊢ ((fst✝, snd✝) == q) = ((fst✝, snd✝) == q)
Theorem: Digraph.Walk.List.count_prod_eq
Proof state before:
case h.e'_2.beq.h.h.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e q : V × V
fst✝ snd✝ : V
⊢ ((fst✝, snd✝) == q) = ((fst✝, snd✝) == q)
Tactic:
cases q
Proof state after:
case h.e'_2.beq.h.h.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
fst✝¹ snd✝¹ fst✝ snd✝ : V
⊢ ((fst✝¹, snd✝¹) == (fst✝, snd✝)) = ((fst✝¹, snd✝¹) == (fst✝, snd✝))
Theorem: Digraph.Walk.List.count_prod_eq
Proof state before:
case h.e'_2.beq.h.h.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
fst✝¹ snd✝¹ fst✝ snd✝ : V
⊢ ((fst✝¹, snd✝¹) == (fst✝, snd✝)) = ((fst✝¹, snd✝¹) == (fst✝, snd✝))
Tactic:
simp [BEq.beq]
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.count_edges_le_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 : Walk G u v
h : IsTrail p
e : V × V
⊢ List.count e (edges p) ≤ 1
Tactic:
simpa using List.nodup_iff_count_le_one.mp h.edges_nodup e
Proof state after:
no goals
Theorem: Digraph.Walk.IsTrail.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 : Walk G u v
h : IsTrail p
e : V × V
he : e ∈ edges p
⊢ List.count e (edges p) = 1
Tactic:
simpa using List.count_eq_one_of_mem h.edges_nodup he
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ IsPath Walk.nil
Tactic:
constructor <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.of_cons
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
h : G.Adj u v
p : Walk G v w
⊢ IsPath (cons h p) → IsPath p
Tactic:
simp [isPath_def]
Proof state after:
no goals
Theorem: Digraph.Walk.cons_isPath_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
h : G.Adj u v
p : Walk G v w
⊢ IsPath (cons h p) ↔ IsPath p ∧ ¬u ∈ support p
Tactic:
constructor <;> simp (config := { contextual := true }) [isPath_def]
Proof state after:
no goals
Theorem: Digraph.Walk.isPath_iff_eq_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ IsPath p ↔ p = nil
Tactic:
cases p <;> simp [IsPath.nil]
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.of_append_left
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
q : Walk G v w
⊢ IsPath (append p q) → IsPath p
Tactic:
simp only [isPath_def, support_append]
Proof state after:
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
q : Walk G v w
⊢ List.Nodup (support p ++ List.tail (support q)) → List.Nodup (support p)
Theorem: Digraph.Walk.IsPath.of_append_left
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
q : Walk G v w
⊢ List.Nodup (support p ++ List.tail (support q)) → List.Nodup (support p)
Tactic:
exact List.Nodup.of_append_left
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.of_append_right
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
q : Walk G v w
⊢ IsPath (append p q) → IsPath q
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''
u v w u✝ : V
q : Walk G u✝ w
⊢ IsPath (append Walk.nil q) → IsPath q

case cons
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✝
p_ih✝ : ∀ {q : Walk G w✝ w}, IsPath (append p✝ q) → IsPath q
q : Walk G w✝ w
⊢ IsPath (append (cons h✝ p✝) q) → IsPath q
Theorem: Digraph.Walk.IsPath.of_append_right
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 w u✝ : V
q : Walk G u✝ w
⊢ IsPath (append Walk.nil q) → IsPath q
Tactic:
exact id
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.of_append_right
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 w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ {q : Walk G w✝ w}, IsPath (append p✝ q) → IsPath q
q : Walk G w✝ w
⊢ IsPath (append (cons h✝ p✝) q) → IsPath q
Tactic:
simp (config := {contextual := true}) [*]
Proof state after:
no goals
Theorem: Digraph.Walk.cons_isCycle_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
p : Walk G v u
h : G.Adj u v
⊢ IsCycle (cons h p) ↔ IsPath p ∧ ¬(u, v) ∈ edges p
Tactic:
simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
  support_cons, List.tail_cons]
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 v u
h : G.Adj u v
⊢ (¬(u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬(u, v) ∈ edges p
Theorem: Digraph.Walk.cons_isCycle_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
p : Walk G v u
h : G.Adj u v
⊢ (¬(u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬(u, v) ∈ edges p
Tactic:
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
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 v u
h : G.Adj u v
this : List.Nodup (support p) → List.Nodup (edges p)
⊢ (¬(u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬(u, v) ∈ edges p
Theorem: Digraph.Walk.cons_isCycle_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
p : Walk G v u
h : G.Adj u v
this : List.Nodup (support p) → List.Nodup (edges p)
⊢ (¬(u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬(u, v) ∈ edges p
Tactic:
tauto
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.length_lt
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : Fintype V
u v : V
p : Walk G u v
hp : IsPath p
⊢ length p < Fintype.card V
Tactic:
rw [Nat.lt_iff_add_one_le, ← length_support]
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : Fintype V
u v : V
p : Walk G u v
hp : IsPath p
⊢ List.length (support p) ≤ Fintype.card V
Theorem: Digraph.Walk.IsPath.length_lt
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : Fintype V
u v : V
p : Walk G u v
hp : IsPath p
⊢ List.length (support p) ≤ Fintype.card V
Tactic:
exact hp.support_nodup.length_le_card
Proof state after:
no goals
Theorem: Digraph.Walk.take_spec
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
⊢ append (takeUntil p u h) (dropUntil p u h) = p
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
⊢ 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✝
Theorem: Digraph.Walk.take_spec
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
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil
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✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil
Theorem: Digraph.Walk.take_spec
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✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil
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
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil
Theorem: Digraph.Walk.take_spec
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
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil
Tactic:
rfl
Proof state after:
no goals