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 u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).support = List.take (n + 1) p.support
n : ℕ
⊢ ((cons h p).take n).support = List.take (n + 1) (cons h p).support
have cons : support (v := (cons h p).getVert 0) ((cons h p).take 0) = List.take (HAdd.hAdd (α := ℕ) 0 1) (cons h p).support
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.take n).support = List.take (n + 1) p.support
n : ℕ
cons :
  support (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) =
    List.take (HAdd.hAdd (α := ℕ) 0 1) (Walk.cons h p).support
⊢ ((Walk.cons h p).take n).support = List.take (n + 1) (Walk.cons h p).support
have cons₁ : ∀ (n : ℕ),
  support (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) =
    List.take (n + 1 + 1) (Walk.cons h p).support
Tactic: cases n
Cleared hypotheses: n
-- 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
n m : ℕ
⊢ (p.take n).take m = Walk.copy (p.take (min n m)) ⋯ ⋯
have h : ((p.take n).take m).support = (Walk.copy (p.take (min n m)) sorry sorry).support
Tactic: apply ext_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
⊢ p.take 0 = p.copy ⋯ ⋯
have zero : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ 0), take nil 0 = Walk.copy nil sorry sorry
Tactic: cases p
Cleared hypotheses: u, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
zero : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ 0), take nil 0 = Walk.copy nil ⋯ ⋯
⊢ p.take 0 = p.copy ⋯ ⋯
have zero₁ : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (cons h p).length ≤ 0), (cons h p).take 0 = (cons h p).copy sorry sorry
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u : V
p : G.Walk u v
h : p.length ≤ n + 1
⊢ p.take (n + 1) = p.copy ⋯ ⋯
have succ : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ n + 1), take nil (n + 1) = Walk.copy nil sorry sorry
Tactic: cases p
Cleared hypotheses: u, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u : V
p : G.Walk u v
h : p.length ≤ n + 1
succ : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ n + 1), take nil (n + 1) = Walk.copy nil ⋯ ⋯
⊢ p.take (n + 1) = p.copy ⋯ ⋯
have succ₁ : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (cons h p).length ≤ n + 1),
  (cons h p).take (n + 1) = (cons h p).copy sorry sorry
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
h : (cons h_1 p).length ≤ n + 1
⊢ (cons h_1 p).take (n + 1) = (cons h_1 p).copy ⋯ ⋯
have h₁ : p.length ≤ n
Tactic: rw [length_cons, Nat.add_le_add_iff_right] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ p.take n = p.copy ⋯ ⋯
have zero : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ 0), p.take 0 = p.copy sorry sorry
Tactic: induction n generalizing p u with
  | zero => cases p <;> simp [take] at h ⊢
  | succ n ih =>
    cases p
    · simp [take]
    rw [length_cons, Nat.add_le_add_iff_right] at h
    simp [take, ih h]
Cleared hypotheses: u, n, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
zero : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ 0), p.take 0 = p.copy ⋯ ⋯
⊢ p.take n = p.copy ⋯ ⋯
have succ : ∀ (n : ℕ) (ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy sorry sorry) {u : V} {p : G.Walk u v}
  (h : p.length ≤ n + 1), p.take (n + 1) = p.copy sorry sorry
Tactic: induction n generalizing p u with
  | zero => cases p <;> simp [take] at h ⊢
  | succ n ih =>
    cases p
    · simp [take]
    rw [length_cons, Nat.add_le_add_iff_right] at h
    simp [take, ih h]
Cleared hypotheses: u, n, p, 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
n : ℕ
hn : n ≠ 0
⊢ (cons h p).take n = cons h (Walk.copy (p.take (n - 1)) ⋯ ⋯)
have h₁ : ((cons h p).take n).support = (cons h (Walk.copy (p.take (n - 1)) sorry sorry)).support
Tactic: apply ext_support
-- 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
n : ℕ
⊢ (p.take n).darts = List.take n p.darts
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List G.Dart) (darts (u := u) (v := getVert (G := G) (u := u) nil n) (take nil n))
    (List.take n (darts (u := u) nil))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- 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
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List G.Dart) (darts (u := u) (v := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n))
      (List.take n (darts (u := u) Walk.nil))
⊢ (p.take n).darts = List.take n p.darts
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.take n).darts = List.take n p.darts) →
    ∀ (n : ℕ), ((cons h p).take n).darts = List.take n (cons h p).darts
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) nil n) (take nil n))
    (List.take n (darts (u := u_1) nil))
have nil : Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0))
  (List.take 0 (darts (u := u_1) nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil 0) (take Walk.nil 0))
    (List.take 0 (darts (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil n) (take Walk.nil n))
    (List.take n (darts (u := u_1) Walk.nil))
have nil₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := List G.Dart)
    (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (take Walk.nil (n + 1)))
    (List.take (n + 1) (darts (u := u_1) Walk.nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.take n).darts = List.take n p.darts
n : ℕ
⊢ ((cons h p).take n).darts = List.take n (cons h p).darts
have cons : darts (v := (cons h p).getVert 0) ((cons h p).take 0) = List.take 0 (cons h p).darts
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.take n).darts = List.take n p.darts
n : ℕ
cons : darts (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) = List.take 0 (Walk.cons h p).darts
⊢ ((Walk.cons h p).take n).darts = List.take n (Walk.cons h p).darts
have cons₁ : ∀ (n : ℕ),
  darts (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) = List.take (n + 1) (Walk.cons h p).darts
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℕ
⊢ (p.take n).edges = List.take n p.edges
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u) (v := getVert (G := G) (u := u) nil n) (take nil n))
    (List.take n (edges (G := G) (u := u) nil))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- 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
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List (Sym2 V))
      (edges (G := G) (u := u) (v := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n))
      (List.take n (edges (G := G) (u := u) Walk.nil))
⊢ (p.take n).edges = List.take n p.edges
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.take n).edges = List.take n p.edges) →
    ∀ (n : ℕ), ((cons h p).take n).edges = List.take n (cons h p).edges
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil n) (take nil n))
    (List.take n (edges (G := G) (u := u_1) nil))
have nil : Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0))
  (List.take 0 (edges (G := G) (u := u_1) nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil 0) (take Walk.nil 0))
    (List.take 0 (edges (G := G) (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil n) (take Walk.nil n))
    (List.take n (edges (G := G) (u := u_1) Walk.nil))
have nil₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (take Walk.nil (n + 1)))
    (List.take (n + 1) (edges (G := G) (u := u_1) Walk.nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.take n).edges = List.take n p.edges
n : ℕ
⊢ ((cons h p).take n).edges = List.take n (cons h p).edges
have cons : edges (v := (cons h p).getVert 0) ((cons h p).take 0) = List.take 0 (cons h p).edges
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.take n).edges = List.take n p.edges
n : ℕ
cons : edges (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) = List.take 0 (Walk.cons h p).edges
⊢ ((Walk.cons h p).take n).edges = List.take n (Walk.cons h p).edges
have cons₁ : ∀ (n : ℕ),
  edges (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) = List.take (n + 1) (Walk.cons h p).edges
Tactic: cases n
Cleared hypotheses: n
-- 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.penultimate = p.snd
have nil : Eq.{u + 1} (α := V) (penultimate (G := G) (u := u) (reverse nil)) (snd (G := G) (u := u) nil)
Tactic: cases p
Cleared hypotheses: v, 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 : Eq.{u + 1} (α := V) (penultimate (G := G) (u := u) (reverse Walk.nil)) (snd (G := G) (u := u) Walk.nil)
⊢ p.reverse.penultimate = p.snd
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).reverse.penultimate = (cons h p).snd
Tactic: cases p
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
⊢ p.drop 0 = p.copy ⋯ ⋯
have nil : Eq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) nil 0) u) (drop nil 0) (Walk.copy nil sorry sorry)
Tactic: cases p
Cleared hypotheses: v, 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 : Eq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) Walk.nil 0) u) (drop Walk.nil 0) (Walk.copy Walk.nil ⋯ ⋯)
⊢ p.drop 0 = p.copy ⋯ ⋯
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).drop 0 = (cons h p).copy sorry sorry
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ (p.drop n).Nil
have rw : (p.drop n).length = 0
Tactic: rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
rw : (p.drop n).length = 0
⊢ (p.drop n).Nil
have rw₁ : p.length - n = 0
Tactic: rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
rw : (p.drop n).length = 0
rw₁ : p.length - n = 0
⊢ (p.drop n).Nil
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h]
-- 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
n : ℕ
⊢ (p.drop n).support = List.drop (min n p.length) p.support
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n))
    (List.drop (min n (length.{u} (V := V) (G := G) (u := u) nil)) (support (G := G) (u := u) nil))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- 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
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n))
      (List.drop (min n (length.{u} (V := V) (G := G) (u := u) Walk.nil)) (support (G := G) (u := u) Walk.nil))
⊢ (p.drop n).support = List.drop (min n p.length) p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support) →
    ∀ (n : ℕ), ((cons h p).drop n).support = List.drop (min n (cons h p).length) (cons h p).support
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) nil n) (drop nil n))
    (List.drop (min n (length.{u} (V := V) (G := G) (u := u_1) nil)) (support (G := G) (u := u_1) nil))
have nil : Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0))
  (List.drop (min 0 (length.{u} (V := V) (G := G) (u := u_1) nil)) (support (G := G) (u := u_1) nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0))
    (List.drop (min 0 (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)) (support (G := G) (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n))
    (List.drop (min n (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)) (support (G := G) (u := u_1) Walk.nil))
have nil₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := List V)
    (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)))
    (List.drop (min (n + 1) (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)) (support (G := G) (u := u_1) Walk.nil))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support
n : ℕ
⊢ ((cons h p).drop n).support = List.drop (min n (cons h p).length) (cons h p).support
have cons : support (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop (min 0 (cons h p).length) (cons h p).support
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
p_ih : ∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support
n : ℕ
cons :
  support (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) =
    List.drop (min 0 (Walk.cons h p).length) (Walk.cons h p).support
⊢ ((Walk.cons h p).drop n).support = List.drop (min n (Walk.cons h p).length) (Walk.cons h p).support
have cons₁ : ∀ (n : ℕ),
  support (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) =
    List.drop (min (n + 1) (Walk.cons h p).length) (Walk.cons h p).support
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℕ
⊢ (p.take n).append (p.drop n) = p
have h : ((p.take n).append (p.drop n)).support = p.support
Tactic: apply ext_support
-- 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
n : ℕ
⊢ ((p.take n).append (p.drop n)).support = p.support
have h : List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
Tactic: rw [support_append, take_support_eq_support_take_succ, drop_support_eq_support_drop_min,
    List.tail_drop]
-- 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
n : ℕ
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
have pos : ∀ (h : n < p.length), List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
Tactic: by_cases! h : n < p.length
-- 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
n : ℕ
pos : ∀ (h : n < p.length), List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
have neg : ∀ (h : p.length ≤ n), List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
Tactic: by_cases! h : n < p.length
-- 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
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
have neg : List.take (n + 1) p.support ++ [] = p.support
Tactic: rw [Nat.min_eq_right h, ← length_support, List.drop_length]
-- 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
⊢ (cons h p).tail = p.copy ⋯ ⋯
have nil : (cons h nil).tail = Walk.copy nil sorry sorry
Tactic: cases p
Cleared hypotheses: w, 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 : (cons h Walk.nil).tail = Walk.copy Walk.nil ⋯ ⋯
⊢ (cons h p).tail = p.copy ⋯ ⋯
have cons : ∀ {v_1 : V} (h_1 : G.Adj v v_1) (p : G.Walk v_1 w), (cons h (cons h_1 p)).tail = (cons h_1 p).copy sorry sorry
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).dropLast = p.copy ⋯ ⋯
have nil : ∀ {u : V} (h : G.Adj u t), (concat nil h).dropLast = Walk.copy nil sorry sorry
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
nil : ∀ {u : V} (h : G.Adj u t), (concat Walk.nil h).dropLast = Walk.copy Walk.nil ⋯ ⋯
⊢ (p.concat h).dropLast = p.copy ⋯ ⋯
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy sorry sorry) →
    ∀ (h_1 : G.Adj w t), ((cons h p).concat h_1).dropLast = (cons h p).copy sorry sorry
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯
h : G.Adj w t
⊢ ((cons h_1 p).concat h).dropLast = (cons h_1 p).copy ⋯ ⋯
have cons : cons h_1 ((p.concat h).dropLast.copy sorry sorry) = (cons h_1 p).copy sorry sorry
Tactic: rw! [concat_cons, dropLast_cons_of_not_nil]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯
h : G.Adj w t
cons : Walk.cons h_1 ((p.concat h).dropLast.copy ⋯ ⋯) = (Walk.cons h_1 p).copy ⋯ ⋯
⊢ ((Walk.cons h_1 p).concat h).dropLast = (Walk.cons h_1 p).copy ⋯ ⋯
have cons₁ : ¬(p.concat h).Nil
Tactic: rw! [concat_cons, dropLast_cons_of_not_nil]
-- 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
hp : ¬p.Nil
⊢ cons ⋯ p.tail = p
have nil : ∀ (hp : ¬Nil.{u} (V := V) (G := G) (v := u) nil), cons sorry (tail nil) = nil
Tactic: cases p
Cleared hypotheses: v, p, hp
-- 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
hp : ¬p.Nil
nil : ∀ (hp : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil), cons ⋯ (tail Walk.nil) = Walk.nil
⊢ cons ⋯ p.tail = p
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (hp : ¬(cons h p).Nil), cons sorry (cons h p).tail = cons h p
Tactic: cases p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hadj : G.Adj u_1 v_1
p : G.Walk v_1 w
hind : ∀ (hp : G.Adj p.penultimate w), p.dropLast.concat hp = p
hp : G.Adj (cons hadj p).penultimate w
⊢ (cons hadj p).dropLast.concat hp = cons hadj p
have cons : ∀ (hind : ∀ (hp : G.Adj (penultimate (G := G) (u := v_1) nil) v_1), concat (dropLast nil) hp = nil)
  (hp : G.Adj (cons hadj nil).penultimate v_1), (cons hadj nil).dropLast.concat hp = cons hadj nil
Tactic: cases p with
    | nil => rfl
    | _ => simp [hind]
Cleared hypotheses: w, p, hind, hp