awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
pos : i < p.length → p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)
neg : ¬i < p.length → (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
⊢ (if i < p.length then p.getVert (p.length - i) else (cons ⋯ nil).getVert (i - p.length)) =
    (cons h p).getVert (p.length + 1 - i)

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

Tactic:
simp [Nat.succ_sub hi.le]

Premises used: LT.lt.le, Nat.succ_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
h_1 : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

Tactic:
next hi => simp [Nat.succ_sub hi.le]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
inl :
  ∀ (ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)) (hi : ¬p.length < p.length),
    (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)
inr : ∀ (hi' : p.length < i), (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
obtain rfl | hi' := eq_or_gt_of_not_lt hi

Premises used: eq_or_gt_of_not_lt, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
inr : (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']

Premises used: Nat.sub_pos_of_lt, Nat.eq_add_of_sub_eq, Nat.sub_eq_zero_of_le, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
nil :
  ∀ {u : V},
    Eq.{u + 1} (α := V) (getVert (G := G) (u := u) (reverse Walk.nil) i)
      (getVert (G := G) (u := u) Walk.nil (length.{u} (V := V) (G := G) (u := u) Walk.nil - i))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.reverse.getVert i = p.getVert (p.length - i)),
    (Walk.cons h p).reverse.getVert i = (Walk.cons h p).getVert ((Walk.cons h p).length - i)
⊢ p.reverse.getVert i = p.getVert (p.length - i)

Tactic:
induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
    split_ifs
    next hi => simp [Nat.succ_sub hi.le]
    next hi =>
      obtain rfl | hi' := eq_or_gt_of_not_lt hi
      · simp
      · rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_reverse, SimpleGraph.Walk.length_cons, SimpleGraph.Walk.reverse_cons, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u : V
⊢ Eq (α := motive u u nil) (concatRec (motive := motive) (@Hnil) (@Hconcat) nil) Hnil

Tactic:
rfl

Premises used: SimpleGraph.Walk.reverseAux, SimpleGraph.Walk.reverse, SimpleGraph.Walk.concatRecAux, SimpleGraph.Walk.concatRec, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
simp :
  Eq.rec (motive := fun (x : G.Walk u w) (h : (p.concat h).reverse.reverse = x) ↦ motive u w x)
      (concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse) ⋯ =
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
⊢ concatRec (motive := motive) (@Hnil) (@Hconcat) (p.concat h) =
    Hconcat p h (concatRec (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p)

Tactic:
simp only [concatRec]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
apply :
  concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
⊢ Eq.rec (motive := fun (x : G.Walk u w) (h : (p.concat h).reverse.reverse = x) ↦ motive u w x)
      (concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse) ⋯ =
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)

Tactic:
apply eq_of_heq (rec_heq_of_heq _ _)

Premises used: rec_heq_of_heq, eq_of_heq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
trans :
  concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
    concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse)
trans₁ :
  concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
⊢ concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)

Tactic:
trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.cons, SimpleGraph.Walk.reverse, SimpleGraph.Walk.concatRecAux
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
e_8 : (p.concat h).reverse = cons ⋯ p.reverse
⊢ concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
    concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse)

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse = cons ⋯ p.reverse

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
rw :
  Hconcat p.reverse.reverse ⋯ (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
⊢ concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)

Tactic:
rw [concatRecAux, eqRec_heq_iff_heq]

Premises used: eqRec_heq_iff_heq, SimpleGraph.Walk.concatRecAux
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
e_4 : p.reverse.reverse = p
e_6 :
  HEq (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) (β := motive u v p)
    (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯ :
      motive u v p)
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.reverse.reverse = p

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ HEq (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) (β := motive u v p)
    (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯ :
      motive u v p)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
nil : ∀ (h : G.Adj u u), concat Walk.nil h ≠ Walk.nil
cons : ∀ {v_1 : V} (h_1 : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h_1 p).concat h ≠ Walk.nil
⊢ p.concat h ≠ Walk.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
h : G.Adj u u
⊢ concat nil h ≠ nil

Tactic:
simp [concat]

Premises used: SimpleGraph.Walk.concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj v u
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h_1 p).concat h ≠ nil

Tactic:
simp [concat]

Premises used: SimpleGraph.Walk.concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
p' : G.Walk u_1 v'
he : concat Walk.nil h = p'.concat h'
nil :
  ∀ {h : G.Adj v' w} (he : concat Walk.nil h = concat Walk.nil h'),
    ∃ (hv : v' = v'), Eq (α := G.Walk v' v') (Walk.copy Walk.nil ⋯ hv) Walk.nil
nil₁ :
  ∀ {v : V} (h_1 : G.Adj u_1 v) (p : G.Walk v v') (he : concat Walk.nil h = (cons h_1 p).concat h'),
    ∃ (hv : u_1 = v'), Walk.copy Walk.nil ⋯ hv = cons h_1 p
⊢ ∃ (hv : u_1 = v'), Walk.copy Walk.nil ⋯ hv = p'

Tactic:
cases p'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : concat nil h = concat nil h'
⊢ ∃ (hv : v' = v'), Eq (α := G.Walk v' v') (Walk.copy nil ⋯ hv) nil

Tactic:
⟨rfl, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : concat nil h = concat nil h'
⊢ ∃ (hv : v' = v'), Eq (α := G.Walk v' v') (Walk.copy nil ⋯ hv) nil

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 v'
he : concat nil h = (cons h_1 p).concat h'
⊢ w = v_1 ∧ HEq (α := G.Walk w w) nil (p.concat h')

Tactic:
simp only [concat_nil, concat_cons, cons.injEq] at he

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.concat_nil, SimpleGraph.Walk.concat_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 v'
he : w = v_1 ∧ HEq (α := G.Walk w w) Walk.nil (p.concat h')
nil :
  ∀ (h : G.Adj u_1 w) (p : G.Walk w v') (he : HEq (α := G.Walk w w) Walk.nil (p.concat h')),
    ∃ (hv : u_1 = v'), Walk.copy Walk.nil ⋯ hv = cons h p
⊢ ∃ (hv : u_1 = v'), Walk.copy Walk.nil ⋯ hv = cons h_1 p

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h h_1 : G.Adj u_1 w
p : G.Walk w v'
he : HEq (α := G.Walk w w) nil (p.concat h')
⊢ ∃ (hv : u_1 = v'), Walk.copy nil ⋯ hv = cons h_1 p

Tactic:
(concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim

Premises used: False.elim, SimpleGraph.Walk.concat_ne_nil, heq_iff_eq, Iff.mp, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h h_1 : G.Adj u_1 w
p : G.Walk w v'
he : HEq (α := G.Walk w w) nil (p.concat h')
⊢ ∃ (hv : u_1 = v'), Walk.copy nil ⋯ hv = cons h_1 p

Tactic:
exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim

Premises used: False.elim, SimpleGraph.Walk.concat_ne_nil, heq_iff_eq, Iff.mp, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
p' : G.Walk u_1 v'
he : (cons h_1 p).concat h = p'.concat h'
⊢ cons h_1 (p.concat h) = p'.concat h'

Tactic:
rw [concat_cons] at he

Premises used: SimpleGraph.Walk.concat_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
p' : G.Walk u_1 v'
he : Walk.cons h_1 (p.concat h) = p'.concat h'
cons :
  ∀ (h_2 : G.Adj v' v_1) (he : Walk.cons h_2 (p.concat h) = concat nil h'),
    ∃ (hv : w_1 = v'), (Walk.cons h_2 p).copy ⋯ hv = nil
cons₁ :
  ∀ {v : V} (h_2 : G.Adj u_1 v) (p_1 : G.Walk v v') (he : Walk.cons h_1 (p.concat h) = (Walk.cons h_2 p_1).concat h'),
    ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = Walk.cons h_2 p_1
⊢ ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = p'

Tactic:
cases p'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : cons h_1 (p.concat h) = concat nil h'
⊢ v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil

Tactic:
simp only [concat_nil, cons.injEq] at he

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.concat_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
⊢ G.Adj v' v_1

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
⊢ ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
ih₁ : ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
⊢ G.Adj w_1 v_1

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
ih₁ : ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h₁ : G.Adj w_1 v_1
⊢ HEq (p.concat h₁) (β := G.Walk v_1 v_1) nil

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' v_1 w : V
p : G.Walk v_1 w
h_1 h' : G.Adj v' v_1
ih : ∀ {h : G.Adj w v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w = v'), p.copy ⋯ hv = p'
h : G.Adj w v_1
he : HEq (p.concat h) (β := G.Walk v_1 v_1) nil
⊢ ∃ (hv : w = v'), (cons h_1 p).copy ⋯ hv = nil

Tactic:
(concat_ne_nil _ _ (heq_iff_eq.mp he)).elim

Premises used: False.elim, SimpleGraph.Walk.concat_ne_nil, heq_iff_eq, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' v_1 w : V
p : G.Walk v_1 w
h_1 h' : G.Adj v' v_1
ih : ∀ {h : G.Adj w v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w = v'), p.copy ⋯ hv = p'
h : G.Adj w v_1
he : HEq (p.concat h) (β := G.Walk v_1 v_1) nil
⊢ ∃ (hv : w = v'), (cons h_1 p).copy ⋯ hv = nil

Tactic:
exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim

Premises used: False.elim, SimpleGraph.Walk.concat_ne_nil, heq_iff_eq, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 v'
he : cons h_1 (p.concat h) = (cons h_2 p_1).concat h'
⊢ v_1 = v_2 ∧ p.concat h ≍ p_1.concat h'

Tactic:
rw [concat_cons, cons.injEq] at he

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.concat_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 v'
he : v_1 = v_2 ∧ p.concat h ≍ p_1.concat h'
cons :
  ∀ (h_3 : G.Adj u_1 v_1) (p_2 : G.Walk v_1 v') (he : p.concat h ≍ p_2.concat h'),
    ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = Walk.cons h_3 p_2
⊢ ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = Walk.cons h_2 p_1

Tactic:
obtain ⟨rfl, he⟩ := he

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_2 : G.Adj u_1 v_1
p_1 : G.Walk v_1 v'
he : p.concat h ≍ p_1.concat h'
cons :
  ∀ {h' : G.Adj w_1 w}
    (ih :
      ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 w_1} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = w_1), p.copy ⋯ hv = p')
    (he : p.concat h ≍ (p.copy ⋯ ⋯).concat h'),
    ∃ (hv : w_1 = w_1), (Walk.cons h_1 p).copy ⋯ hv = Walk.cons h_2 (p.copy ⋯ ⋯)
⊢ ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = Walk.cons h_2 p_1

Tactic:
obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)

Premises used: heq_iff_eq, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph 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
h : G.Adj w_1 w
h_2 : G.Adj u_1 v_1
h' : G.Adj w_1 w
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 w_1} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = w_1), p.copy ⋯ hv = p'
he : p.concat h ≍ (p.copy ⋯ ⋯).concat h'
⊢ ∃ (hv : w_1 = w_1), (cons h_1 p).copy ⋯ hv = cons h_2 (p.copy ⋯ ⋯)

Tactic:
⟨rfl, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph 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
h : G.Adj w_1 w
h_2 : G.Adj u_1 v_1
h' : G.Adj w_1 w
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 w_1} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = w_1), p.copy ⋯ hv = p'
he : p.concat h ≍ (p.copy ⋯ ⋯).concat h'
⊢ ∃ (hv : w_1 = w_1), (cons h_1 p).copy ⋯ hv = cons h_2 (p.copy ⋯ ⋯)

Tactic:
exact ⟨rfl, rfl⟩