awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

Tactic:
fun h => ⟨_, _, (p.take_spec h).symm⟩

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.dropUntil, Exists.intro, SimpleGraph.Walk.takeUntil, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

Tactic:
exact fun h => ⟨_, _, (p.take_spec h).symm⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk u w
r : G.Walk w v
⊢ w ∈ (q.append r).support

Tactic:
simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]

Premises used: SimpleGraph.Walk.start_mem_support, or_self_iff, SimpleGraph.Walk.end_mem_support, SimpleGraph.Walk.mem_support_append_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
mp : w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
mpr mpr₁ : (∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r) → w ∈ p.support
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

Tactic:
classical
  constructor
  · exact fun h => ⟨_, _, (p.take_spec h).symm⟩
  · rintro ⟨q, r, rfl⟩
    simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]

Premises used: SimpleGraph.Walk.start_mem_support, or_self_iff, SimpleGraph.Walk.end_mem_support, rfl, SimpleGraph.Walk.mem_support_append_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
nil :
  ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u),
    List.count u (takeUntil Walk.nil u h).support = 1
cons :
  ∀ {u_1 v w : V} (h : G.Adj u_1 v) (p : G.Walk v w),
    (∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1) →
      ∀ (h_1 : u ∈ (Walk.cons h p).support), List.count u ((Walk.cons h p).takeUntil u h_1).support = 1
⊢ List.count u (p.takeUntil u h).support = 1

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 : V
h_1 : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u
h : u = u_1
nil :
  ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u_1),
    List.count u_1 (takeUntil Walk.nil u_1 h).support = 1
⊢ List.count u (takeUntil Walk.nil u h_1).support = 1

Tactic:
subst u
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w u : V
h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
⊢ List.count u (takeUntil nil u h).support = 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h : u ∈ (Walk.cons h_1 p).support
cons : ∀ (h : G.Adj u v_1), List.count u ((Walk.cons h p).takeUntil u ⋯).support = 1
cons₁ : ∀ (a : List.Mem u p.support), List.count u ((Walk.cons h_1 p).takeUntil u ⋯).support = 1
⊢ List.count u ((Walk.cons h_1 p).takeUntil u h).support = 1

Tactic:
cases h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w v_1 w_1 : V
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h : G.Adj u v_1
⊢ List.count u ((cons h p).takeUntil u ⋯).support = 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
pos :
  ∀ (h' : u_1 = u),
    List.count u
        (support (G := G) (u := u_1) (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h')) =
      1
neg : ∀ (h' : ¬u_1 = u), List.count u (cons h (p.takeUntil u ⋯)).support = 1
⊢ List.count u
      (support (G := G) (u := u_1) (v := u)
        (if hx : u_1 = u then Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil hx
        else cons h (p.takeUntil u ⋯))) =
    1

Tactic:
split_ifs with h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
h' : u_1 = u
⊢ u = u_1

Tactic:
rw [eq_comm] at h'

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
h' : ¬u_1 = u
⊢ ¬u = u_1

Tactic:
rw [eq_comm] at h'

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
h'_1 : u_1 = u
h' : u = u_1
pos :
  (∀ (h : u_1 ∈ p.support), List.count u_1 (p.takeUntil u_1 h).support = 1) →
    List.Mem u_1 p.support →
      ∀ (h' : u_1 = u_1),
        List.count u_1
            (support (G := G) (u := u_1) (v := u_1)
              (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil ⋯)) =
          1
⊢ List.count u
      (support (G := G) (u := u_1) (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h'_1)) =
    1

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w u v_1 w_1 : V
h : G.Adj u v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
h' : u = u
⊢ List.count u (support (G := G) (u := u) (v := u) (Eq.rec (motive := fun (x : V) (h : u = x) ↦ G.Walk u x) nil ⋯)) = 1

Tactic:
simp! [*, List.count_cons]

Premises used: List.count_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1
h_1 : List.Mem u p.support
h'_1 : ¬u_1 = u
h' : ¬u = u_1
⊢ List.count u (cons h (p.takeUntil u ⋯)).support = 1

Tactic:
simp! [*, List.count_cons]

Premises used: List.count_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 : V
h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u
⊢ u = u_1

Tactic:
rw [mem_support_nil_iff] at h

Premises used: SimpleGraph.Walk.mem_support_nil_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 : V
h_1 : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u
h : u = u_1
nil :
  ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u_1),
    List.count s(u_1, x) (takeUntil Walk.nil u_1 h).edges ≤ 1
⊢ List.count s(u, x) (takeUntil Walk.nil u h_1).edges ≤ 1

Tactic:
subst u
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w x u : V
h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
⊢ List.count s(u, x) (takeUntil nil u h).edges ≤ 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : u ∈ (Walk.cons ha p').support
cons : ∀ (ha : G.Adj u v_1), List.count s(u, x) ((Walk.cons ha p').takeUntil u ⋯).edges ≤ 1
cons₁ : ∀ (a : List.Mem u p'.support), List.count s(u, x) ((Walk.cons ha p').takeUntil u ⋯).edges ≤ 1
⊢ List.count s(u, x) ((Walk.cons ha p').takeUntil u h).edges ≤ 1

Tactic:
cases h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x v_1 w_1 : V
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v_1
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
pos :
  ∀ (h' : u_1 = u),
    List.count s(u, x)
        (edges (G := G) (u := u_1) (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h')) ≤
      1
neg : ∀ (h' : ¬u_1 = u), List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1
⊢ List.count s(u, x)
      (edges (G := G) (u := u_1) (v := u)
        (if hx : u_1 = u then Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil hx
        else cons ha (p'.takeUntil u ⋯))) ≤
    1

Tactic:
split_ifs with h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : u_1 = u
pos :
  ∀ (ih : ∀ (h : u_1 ∈ p'.support), List.count s(u_1, x) (p'.takeUntil u_1 h).edges ≤ 1),
    List.Mem u_1 p'.support →
      List.count s(u_1, x)
          (edges (G := G) (u := u_1) (v := u_1) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil ⋯)) ≤
        1
⊢ List.count s(u, x)
      (edges (G := G) (u := u_1) (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h')) ≤
    1

Tactic:
subst h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w x u v_1 w_1 : V
ha : G.Adj u v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
⊢ List.count s(u, x)
      (edges (G := G) (u := u) (v := u) (Eq.rec (motive := fun (x : V) (h : u = x) ↦ G.Walk u x) nil ⋯)) ≤
    1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : ¬u_1 = u
neg : (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u_1, v_1) == s(u, x)) = true then 1 else 0) ≤ 1
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1

Tactic:
rw [edges_cons, List.count_cons]

Premises used: List.count_cons, SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : ¬u_1 = u
pos : ∀ (h'' : (s(u_1, v_1) == s(u, x)) = true), List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
neg : ∀ (h'' : ¬(s(u_1, v_1) == s(u, x)) = true), List.count s(u, x) (p'.takeUntil u ⋯).edges + 0 ≤ 1
⊢ (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u_1, v_1) == s(u, x)) = true then 1 else 0) ≤ 1

Tactic:
split_ifs with h''
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : ¬u_1 = u
h'' : (s(u_1, v_1) == s(u, x)) = true
⊢ (u_1, v_1) = (u, x) ∨ (u_1, v_1) = (u, x).swap

Tactic:
simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''

Premises used: Sym2.eq, beq_iff_eq, Sym2.rel_iff'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : ¬u_1 = u
h'' : (u_1, v_1) = (u, x) ∨ (u_1, v_1) = (u, x).swap
pos :
  ∀ (h' : ¬u = u) (p' : G.Walk x w_1) (ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1)
    (a : List.Mem u p'.support) (ha : G.Adj u x), List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
pos₁ :
  ∀ (h' : ¬(u, x).2 = u) (p' : G.Walk (u, x).1 w_1)
    (ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1) (a : List.Mem u p'.support)
    (ha : G.Adj (u, x).2 (u, x).1), List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x w_1 : V
h' : ¬u = u
p' : G.Walk x w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
ha : G.Adj u x
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
(h' rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x w_1 : V
h' : ¬u = u
p' : G.Walk x w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
ha : G.Adj u x
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
exact (h' rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x w_1 : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
pos :
  ∀
    (ih :
      ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := (u, x).1) nil) u),
        List.count s(u, x) (takeUntil nil u h).edges ≤ 1)
    (a : List.Mem u (support (G := G) (u := (u, x).1) nil)), List.count s(u, x) (takeUntil nil u ⋯).edges + 1 ≤ 1
pos₁ :
  ∀ {v : V} (h : G.Adj (u, x).1 v) (p : G.Walk v w_1)
    (ih : ∀ (h_1 : u ∈ (cons h p).support), List.count s(u, x) ((cons h p).takeUntil u h_1).edges ≤ 1)
    (a : List.Mem u (cons h p).support), List.count s(u, x) ((cons h p).takeUntil u ⋯).edges + 1 ≤ 1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
cases p'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
ih :
  ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := (u, x).1) nil) u),
    List.count s(u, x) (takeUntil nil u h).edges ≤ 1
h : List.Mem u (support (G := G) (u := (u, x).1) nil)
⊢ List.count s(u, x) (takeUntil nil u ⋯).edges + 1 ≤ 1

Tactic:
simp!
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x w_1 : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
v_1 : V
h : G.Adj (u, x).1 v_1
p : G.Walk v_1 w_1
ih : ∀ (h_2 : u ∈ (cons h p).support), List.count s(u, x) ((cons h p).takeUntil u h_2).edges ≤ 1
h_1 : List.Mem u (cons h p).support
⊢ List.count s(u, x) ((cons h p).takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
simp!
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w x u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p' : G.Walk v_1 w_1
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : List.Mem u p'.support
h' : ¬u_1 = u
h'' : ¬(s(u_1, v_1) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 0 ≤ 1

Tactic:
apply ih
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
nil :
  ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u),
    List.count s(u, x) (takeUntil Walk.nil u h).edges ≤ 1
cons :
  ∀ {u_1 v w : V} (ha : G.Adj u_1 v) (p' : G.Walk v w)
    (ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1) (h : u ∈ (Walk.cons ha p').support),
    List.count s(u, x) ((Walk.cons ha p').takeUntil u h).edges ≤ 1
⊢ List.count s(u, x) (p.takeUntil u h).edges ≤ 1

Tactic:
induction p with
  | nil =>
    rw [mem_support_nil_iff] at h
    subst u
    simp
  | cons ha p' ih =>
    cases h
    · simp
    · simp! only
      split_ifs with h'
      · subst h'
        simp
      · rw [edges_cons, List.count_cons]
        split_ifs with h''
        · simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''
          obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
          · exact (h' rfl).elim
          · cases p' <;> simp!
        · apply ih

Premises used: Sym2.eq, beq_iff_eq, List.count_cons, SimpleGraph.Walk.mem_support_nil_iff, Sym2.rel_iff', SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
subst_vars : ∀ (p : G.Walk v' w') (h : u ∈ (p.copy ⋯ ⋯).support), u ∈ p.support
⊢ u ∈ p.support

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u_1 : V
inst : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Tactic:
h

Premises used: SimpleGraph.Walk.copy
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u_1 : V
inst : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
subst_vars :
  ∀ (p : G.Walk v' w') (h : u ∈ (p.copy ⋯ ⋯).support), (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯
⊢ (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
subst_vars :
  ∀ (p : G.Walk v' w') (h : u ∈ (p.copy ⋯ ⋯).support), (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯
⊢ (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
grw : (Walk.copy (v := p.getVert (List.idxOf u p.support)) (p.take (List.idxOf u p.support)) ⋯ ⋯).support <+: p.support
grw₁ : support (v := p.getVert (List.idxOf u p.support)) (p.take (List.idxOf u p.support)) <+: p.support
grw₂ : List.take (List.idxOf u p.support + 1) p.support <+: p.support
grw₃ grw₄ : p.support <+: p.support
⊢ (p.takeUntil u h).support <+: p.support

Tactic:
grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.takeUntil_eq_take, List.take_prefix, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
rw : x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
⊢ x ∈ p.support

Tactic:
rw [← take_spec p h, mem_support_append_iff]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.mem_support_append_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
exact Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.dropUntil u h).support
rw : x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
⊢ x ∈ p.support

Tactic:
rw [← take_spec p h, mem_support_append_iff]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.mem_support_append_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.dropUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.dropUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
exact Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
rw : x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
⊢ x ∈ p.darts

Tactic:
rw [← take_spec p h, darts_append, List.mem_append]

Premises used: SimpleGraph.Walk.take_spec, List.mem_append, SimpleGraph.Walk.darts_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
exact Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
rw : x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
⊢ x ∈ p.darts

Tactic:
rw [← take_spec p h, darts_append, List.mem_append]

Premises used: SimpleGraph.Walk.take_spec, List.mem_append, SimpleGraph.Walk.darts_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
Or.inr hx

Premises used: Or.inr