awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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) nil) u
h : u = u_1
⊢ List.count u (takeUntil nil u h_1).support = 1
have nil : ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1),
  List.count u_1 (takeUntil nil u_1 h).support = 1
Tactic: subst u
Cleared hypotheses: u, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 ∈ (cons h_1 p).support
⊢ List.count u ((cons h_1 p).takeUntil u h).support = 1
have cons : ∀ (h : G.Adj u v_1), List.count u ((cons h p).takeUntil u sorry).support = 1
Tactic: cases h
Cleared hypotheses: u_1, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count u ((Walk.cons h_1 p).takeUntil u h).support = 1
have cons₁ : ∀ (a : List.Mem u p.support), List.count u ((Walk.cons h_1 p).takeUntil u sorry).support = 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have neg : ∀ (h' : ¬u_1 = u), List.count u (cons h (p.takeUntil u sorry)).support = 1
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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
⊢ 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
have h'₁ : u = u_1
Tactic: rw [eq_comm] at h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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
⊢ List.count u (cons h (p.takeUntil u ⋯)).support = 1
have h'₁ : ¬u = u_1
Tactic: rw [eq_comm] at h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
      (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
have 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 sorry)) =
        1
Tactic: subst_vars
Cleared hypotheses: u, p_ih, h_1, h'_1, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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
⊢ List.count s(u, x) (takeUntil nil u h).edges ≤ 1
have h₁ : u = u_1
Tactic: rw [mem_support_nil_iff] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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) nil) u
h : u = u_1
⊢ List.count s(u, x) (takeUntil nil u h_1).edges ≤ 1
have nil : ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1),
  List.count s(u_1, x) (takeUntil nil u_1 h).edges ≤ 1
Tactic: subst u
Cleared hypotheses: u, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 ∈ (cons ha p').support
⊢ List.count s(u, x) ((cons ha p').takeUntil u h).edges ≤ 1
have cons : ∀ (ha : G.Adj u v_1), List.count s(u, x) ((cons ha p').takeUntil u sorry).edges ≤ 1
Tactic: cases h
Cleared hypotheses: u_1, ha, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) ((Walk.cons ha p').takeUntil u h).edges ≤ 1
have cons₁ : ∀ (a : List.Mem u p'.support), List.count s(u, x) ((Walk.cons ha p').takeUntil u sorry).edges ≤ 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have neg : ∀ (h' : ¬u_1 = u), List.count s(u, x) (cons ha (p'.takeUntil u sorry)).edges ≤ 1
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have 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 sorry)) ≤
      1
Tactic: subst h'
Cleared hypotheses: u, ih, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1
have neg : (List.count s(u, x) (p'.takeUntil u sorry).edges + if (s(u_1, v_1) == s(u, x)) = true then 1 else 0) ≤ 1
Tactic: rw [edges_cons, List.count_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u_1, v_1) == s(u, x)) = true then 1 else 0) ≤ 1
have pos : ∀ (h'' : (s(u_1, v_1) == s(u, x)) = true), List.count s(u, x) (p'.takeUntil u sorry).edges + 1 ≤ 1
Tactic: split_ifs with h''
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u_1, v_1) == s(u, x)) = true then 1 else 0) ≤ 1
have neg : ∀ (h'' : ¬(s(u_1, v_1) == s(u, x)) = true), List.count s(u, x) (p'.takeUntil u sorry).edges + 0 ≤ 1
Tactic: split_ifs with h''
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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 + 1 ≤ 1
have h''₁ : (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''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
have 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 sorry).edges + 1 ≤ 1
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
Cleared hypotheses: u_1, v_1, ha, p', ih, h, h', h''
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
have 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 sorry).edges + 1 ≤ 1
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
Cleared hypotheses: u_1, v_1, ha, p', ih, h, h', h''
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
have 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 sorry).edges + 1 ≤ 1
Tactic: cases p'
Cleared hypotheses: w_1, p', ih, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
have 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 sorry).edges + 1 ≤ 1
Tactic: cases p'
Cleared hypotheses: p', ih, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p.takeUntil u h).edges ≤ 1
have nil : ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u),
  List.count s(u, x) (takeUntil nil 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
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ List.count s(u, x) (p.takeUntil u h).edges ≤ 1
have 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 ∈ (cons ha p').support),
  List.count s(u, x) ((cons ha 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
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ u ∈ p.support
have subst_vars : ∀ (p : G.Walk v' w') (h : u ∈ (p.copy sorry sorry).support), u ∈ p.support
Tactic: subst_vars
Cleared hypotheses: v, w, p, hv, hw, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯
have subst_vars : ∀ (p : G.Walk v' w') (h : u ∈ (p.copy sorry sorry).support), (p.copy sorry sorry).takeUntil u h = (p.takeUntil u sorry).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: v, w, p, hv, hw, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw
have subst_vars : ∀ (p : G.Walk v' w') (h : u ∈ (p.copy sorry sorry).support), (p.copy sorry sorry).dropUntil u h = (p.dropUntil u sorry).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: v, w, p, hv, hw, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).support <+: p.support
have grw : (Walk.copy (v := p.getVert (List.idxOf u p.support)) (p.take (List.idxOf u p.support)) sorry sorry).support <+: p.support
Tactic: grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.takeUntil u h).support <+: p.support
have grw₁ : support (v := p.getVert (List.idxOf u p.support)) (p.take (List.idxOf u p.support)) <+: p.support
Tactic: grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.takeUntil u h).support <+: p.support
have grw₂ : List.take (List.idxOf u p.support + 1) p.support <+: p.support
Tactic: grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.takeUntil u h).support <+: p.support
have grw₃ : p.support <+: p.support
Tactic: grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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.support
have rw : x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
Tactic: rw [← take_spec p h, mem_support_append_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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.support
have rw : x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
Tactic: rw [← take_spec p h, mem_support_append_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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.darts
have rw : x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
Tactic: rw [← take_spec p h, darts_append, List.mem_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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.darts
have rw : x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
Tactic: rw [← take_spec p h, darts_append, List.mem_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).length ≤ p.length
have this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
Tactic: have := congr_arg Walk.length (p.take_spec h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length
have this₁ : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length
Tactic: rw [length_append] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).length ≤ p.length
have this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
Tactic: have := congr_arg Walk.length (p.take_spec h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length
have this₁ : (p.dropUntil u h).length + (p.takeUntil u h).length = p.length
Tactic: rw [length_append, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x u_1 : V
q : G.Walk u_1 w
hx : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) x
⊢ (append nil q).takeUntil x ⋯ = takeUntil nil x hx
have hx₁ : x = u_1
Tactic: rw [mem_support_nil_iff] at hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x u_1 : V
q : G.Walk u_1 w
hx_1 : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) x
hx : x = u_1
⊢ (append nil q).takeUntil x ⋯ = takeUntil nil x hx_1
have nil : ∀ (hx : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1),
  (append nil q).takeUntil u_1 sorry = takeUntil nil u_1 hx
Tactic: subst_vars
Cleared hypotheses: x, hx_1, hx