awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk w x
nil : ∀ {u : V} (q : G.Walk u w), append Walk.nil (q.append r) = (append Walk.nil q).append r
⊢ p.append (q.append r) = (p.append q).append r
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (q : G.Walk w_1 w), p.append (q.append r) = (p.append q).append r) →
    ∀ (q : G.Walk w_1 w), (cons h p).append (q.append r) = ((cons h p).append q).append r
Tactic: induction p
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u' v' w' : V
p : G.Walk u v
q : G.Walk v w
hu : u = u'
hv : v = v'
hw : w = w'
⊢ (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
have subst_vars : ∀ (p : G.Walk u' v') (q : G.Walk v' w'), (p.copy sorry sorry).append (q.copy sorry sorry) = (p.append q).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: u, v, w, p, q, hu, hv, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
⊢ (p.concat h).append q = p.append (cons h q)
have rw : (p.append (cons h nil)).append q = p.append (cons h q)
Tactic: rw [concat_eq_append, ← append_assoc, cons_nil_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
rw : (p.append (cons h nil)).append q = p.append (cons h q)
⊢ (p.concat h).append q = p.append (cons h q)
have rw₁ : p.append ((cons h nil).append q) = p.append (cons h q)
Tactic: rw [concat_eq_append, ← append_assoc, cons_nil_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
rw : (p.append (cons h nil)).append q = p.append (cons h q)
rw₁ : p.append ((cons h nil).append q) = p.append (cons h q)
⊢ (p.concat h).append q = p.append (cons h q)
have rw₂ : p.append (cons h q) = p.append (cons h q)
Tactic: rw [concat_eq_append, ← append_assoc, cons_nil_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u_1 v_1 w_1 : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {u : V} (h : G.Adj u v_1), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w_1), cons h p = q.concat h'
u : V
h : G.Adj u u_1
⊢ ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), cons h (cons h' p) = q.concat h'_1
have cons : ∀ (y : V) (q : G.Walk u_1 y) (h'' : G.Adj y w_1) (hc : cons h' p = q.concat h''),
  ∃ (x : V) (q : G.Walk u x) (h'_1 : G.Adj x w_1), cons h (cons h' p) = q.concat h'_1
Tactic: obtain ⟨y, q, h'', hc⟩ := ih h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), cons h p = q.concat h'
have nil : ∀ {u u_1 : V} (h : G.Adj u_1 u), ∃ (x : V) (q : G.Walk u_1 x) (h' : G.Adj x u), cons h nil = q.concat h'
Tactic: induction p generalizing u with
  | nil => exact ⟨_, nil, h, rfl⟩
  | cons h' p ih =>
    obtain ⟨y, q, h'', hc⟩ := ih h'
    exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩
Cleared hypotheses: u, h, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
nil : ∀ {u u_1 : V} (h : G.Adj u_1 u), ∃ (x : V) (q : G.Walk u_1 x) (h' : G.Adj x u), cons h Walk.nil = q.concat h'
⊢ ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), cons h p = q.concat h'
have cons : ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ {u : V} (h : G.Adj u v), ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), cons h p = q.concat h') {u_1 : V}
  (h : G.Adj u_1 u), ∃ (x : V) (q : G.Walk u_1 x) (h'_1 : G.Adj x w), cons h (cons h' p) = q.concat h'_1
Tactic: induction p generalizing u with
  | nil => exact ⟨_, nil, h, rfl⟩
  | cons h' p ih =>
    obtain ⟨y, q, h'', hc⟩ := ih h'
    exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩
Cleared hypotheses: u, h, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk u x
⊢ (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
have nil : ∀ {u : V} (q : G.Walk u w) (r : G.Walk u x), (append nil q).reverseAux r = q.reverseAux (Walk.reverseAux nil r)
Tactic: induction p with
  | nil => rfl
  | cons h _ ih => exact ih q (cons (G.symm h) r)
Cleared hypotheses: p, q, r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk u x
nil :
  ∀ {u : V} (q : G.Walk u w) (r : G.Walk u x),
    (append Walk.nil q).reverseAux r = q.reverseAux (Walk.reverseAux Walk.nil r)
⊢ (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
  (ih : ∀ (q : G.Walk w_1 w) (r : G.Walk v x), (p.append q).reverseAux r = q.reverseAux (p.reverseAux r))
  (q : G.Walk w_1 w) (r : G.Walk u x), ((cons h p).append q).reverseAux r = q.reverseAux ((cons h p).reverseAux r)
Tactic: induction p with
  | nil => rfl
  | cons h _ ih => exact ih q (cons (G.symm h) r)
Cleared hypotheses: p, q, r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)
have nil : ∀ {u : V} (q : G.Walk u w), (Walk.reverseAux nil q).append r = Walk.reverseAux nil (q.append r)
Tactic: induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons (G.symm h) q)]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
nil : ∀ {u : V} (q : G.Walk u w), (Walk.reverseAux Walk.nil q).append r = Walk.reverseAux Walk.nil (q.append r)
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
  (ih : ∀ (q : G.Walk v w), (p.reverseAux q).append r = p.reverseAux (q.append r)) (q : G.Walk u w),
  ((cons h p).reverseAux q).append r = (cons h p).reverseAux (q.append r)
Tactic: induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons (G.symm h) q)]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).reverse = p.reverse.copy hv hu
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).reverse = p.reverse.copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.reverse = p
have nil : ∀ {u : V}, Eq.{u + 1} (α := G.Walk u u) (reverse (reverse nil)) nil
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Eq.{u + 1} (α := G.Walk u u) (reverse (reverse Walk.nil)) Walk.nil
⊢ p.reverse.reverse = p
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.reverse.reverse = p), (cons h p).reverse.reverse = cons h p
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).length = p.length
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).length = p.length
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).length = p.length + q.length
have nil : ∀ {u : V} (q : G.Walk u w), (append nil q).length = length.{u} (V := V) (G := G) (u := u) nil + q.length
Tactic: induction p
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
nil : ∀ {u : V} (q : G.Walk u w), (append Walk.nil q).length = length.{u} (V := V) (G := G) (u := u) Walk.nil + q.length
⊢ (p.append q).length = p.length + q.length
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (q : G.Walk w_1 w), (p.append q).length = p.length + q.length) →
    ∀ (q : G.Walk w_1 w), ((cons h p).append q).length = (cons h p).length + q.length
Tactic: induction p
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk u w
⊢ (p.reverseAux q).length = p.length + q.length
have nil : ∀ {u : V} (q : G.Walk u w), (Walk.reverseAux nil q).length = length.{u} (V := V) (G := G) (u := u) nil + q.length
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, add_assoc]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk u w
nil :
  ∀ {u : V} (q : G.Walk u w),
    (Walk.reverseAux Walk.nil q).length = length.{u} (V := V) (G := G) (u := u) Walk.nil + q.length
⊢ (p.reverseAux q).length = p.length + q.length
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
  (ih : ∀ (q : G.Walk v w), (p.reverseAux q).length = p.length + q.length) (q : G.Walk u w),
  ((cons h p).reverseAux q).length = (cons h p).length + q.length
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, add_assoc]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
have nil : ∀ {u : V} (q : G.Walk u w) (i : ℕ),
  (append nil q).getVert i =
    if i < length.{u} (V := V) (G := G) (u := u) nil then getVert (G := G) (u := u) nil i
    else q.getVert (i - length.{u} (V := V) (G := G) (u := u) nil)
Tactic: induction p generalizing i
Cleared hypotheses: p, q, i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
i : ℕ
nil :
  ∀ {u : V} (q : G.Walk u w) (i : ℕ),
    (append Walk.nil q).getVert i =
      if i < length.{u} (V := V) (G := G) (u := u) Walk.nil then getVert (G := G) (u := u) Walk.nil i
      else q.getVert (i - length.{u} (V := V) (G := G) (u := u) Walk.nil)
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (q : G.Walk w_1 w) (i : ℕ),
      (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)) →
    ∀ (q : G.Walk w_1 w) (i : ℕ),
      ((cons h p).append q).getVert i =
        if i < (cons h p).length then (cons h p).getVert i else q.getVert (i - (cons h p).length)
Tactic: induction p generalizing i
Cleared hypotheses: p, q, i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
i : ℕ
⊢ (append nil q).getVert i =
    if i < length.{u} (V := V) (G := G) (u := u_1) nil then getVert (G := G) (u := u_1) nil i
    else q.getVert (i - length.{u} (V := V) (G := G) (u := u_1) nil)
have nil : (append nil q).getVert 0 =
  if 0 < length.{u} (V := V) (G := G) (u := u_1) nil then getVert (G := G) (u := u_1) nil 0
  else q.getVert (0 - length.{u} (V := V) (G := G) (u := u_1) nil)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
i : ℕ
nil :
  (append Walk.nil q).getVert 0 =
    if 0 < length.{u} (V := V) (G := G) (u := u_1) Walk.nil then getVert (G := G) (u := u_1) Walk.nil 0
    else q.getVert (0 - length.{u} (V := V) (G := G) (u := u_1) Walk.nil)
⊢ (append Walk.nil q).getVert i =
    if i < length.{u} (V := V) (G := G) (u := u_1) Walk.nil then getVert (G := G) (u := u_1) Walk.nil i
    else q.getVert (i - length.{u} (V := V) (G := G) (u := u_1) Walk.nil)
have nil₁ : ∀ (n : ℕ),
  (append Walk.nil q).getVert (n + 1) =
    if n + 1 < length.{u} (V := V) (G := G) (u := u_1) Walk.nil then getVert (G := G) (u := u_1) Walk.nil (n + 1)
    else q.getVert (n + 1 - length.{u} (V := V) (G := G) (u := u_1) Walk.nil)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph 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 :
  ∀ (q : G.Walk w_1 w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w_1 w
i : ℕ
⊢ ((cons h p).append q).getVert i =
    if i < (cons h p).length then (cons h p).getVert i else q.getVert (i - (cons h p).length)
have cons : ((cons h p).append q).getVert 0 =
  if 0 < (cons h p).length then (cons h p).getVert 0 else q.getVert (0 - (cons h p).length)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph 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 :
  ∀ (q : G.Walk w_1 w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w_1 w
i : ℕ
cons :
  ((Walk.cons h p).append q).getVert 0 =
    if 0 < (Walk.cons h p).length then (Walk.cons h p).getVert 0 else q.getVert (0 - (Walk.cons h p).length)
⊢ ((Walk.cons h p).append q).getVert i =
    if i < (Walk.cons h p).length then (Walk.cons h p).getVert i else q.getVert (i - (Walk.cons h p).length)
have cons₁ : ∀ (n : ℕ),
  ((Walk.cons h p).append q).getVert (n + 1) =
    if n + 1 < (Walk.cons h p).length then (Walk.cons h p).getVert (n + 1)
    else q.getVert (n + 1 - (Walk.cons h p).length)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ (cons h p).reverse.getVert i = (cons h p).getVert ((cons h p).length - i)
have cons : (if i < p.length then p.getVert (p.length - i) else (cons sorry nil).getVert (i - p.length)) =
  (cons h p).getVert (p.length + 1 - i)
Tactic: simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ (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)
have pos : i < p.length → p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ (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)
have neg : ¬i < p.length → (cons sorry nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
have inl : ∀ (ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)) (hi : ¬p.length < p.length),
  (cons sorry nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)
Tactic: obtain rfl | hi' := eq_or_gt_of_not_lt hi
Cleared hypotheses: i, ih, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
have inr : ∀ (hi' : p.length < i), (cons sorry nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)
Tactic: obtain rfl | hi' := eq_or_gt_of_not_lt hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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) = (cons h p).getVert (p.length + 1 - i)
have inr : (cons sorry nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0
Tactic: rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.reverse.getVert i = p.getVert (p.length - i)
have nil : ∀ {u : V},
  Eq.{u + 1} (α := V) (getVert (G := G) (u := u) (reverse nil) i)
    (getVert (G := G) (u := u) nil (length.{u} (V := V) (G := G) (u := u) nil - 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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ p.reverse.getVert i = p.getVert (p.length - i)
have 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)),
  (cons h p).reverse.getVert i = (cons h p).getVert ((cons h 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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ 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)
have 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) sorry =
  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) sorry)
Tactic: simp only [concatRec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ 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)
        ⋯)
have 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) sorry)
Tactic: apply eq_of_heq (rec_heq_of_heq _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ 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)
        ⋯)
have trans : concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
  concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons sorry p.reverse)
Tactic: trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ 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)
        ⋯)
have trans₁ : concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons sorry 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) sorry)
Tactic: trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)