awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
pos : ∀ (hm0 : m = 0), n = m
⊢ n = m
have neg : ∀ (hm0 : ¬m = 0), n = m
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : ¬m = 0
⊢ n = m
have hnm₁ : v = p.getVert (m - 1)
Tactic: simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
⊢ n = m
have hvp : v ∉ p.support
Tactic: have hvp : v ∉ p.support := by aesop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m
have hnm₁ : p.getVert (n - 1) = (cons h p).getVert 0
Tactic: simp only [hm0, Walk.getVert_cons p h hn0] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
⊢ n = m
have hvp : v ∉ p.support
Tactic: have hvp : v ∉ p.support := by simp_all
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m
have hnm₁ : p.getVert (n - 1) = p.getVert (m - 1)
Tactic: simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ n = m
have this : n - 1 = m - 1
Tactic: have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m
hnm : p.getVert n = p.getVert m
⊢ n = m
have nil : ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) ⦃n : ℕ⦄
  (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} n) ⦃m : ℕ⦄
  (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} m)
  (hnm : Eq.{u + 1} (α := V) (getVert (G := G) (u := u) Walk.nil n) (getVert (G := G) (u := u) Walk.nil m)), n = m
Tactic: induction p generalizing n m with
  | nil => simp_all
  | @cons v w u h p ihp =>
    simp only [length_cons, Set.mem_setOf_eq] at hn hm hnm
    by_cases hn0 : n = 0 <;> by_cases hm0 : m = 0
    · lia
    · simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
      have hvp : v ∉ p.support := by aesop
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by lia⟩⟩)).elim
    · simp only [hm0, Walk.getVert_cons p h hn0] at hnm
      have hvp : v ∉ p.support := by simp_all
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by lia⟩⟩)).elim
    · simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
      have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
      lia
Cleared hypotheses: p, hp, n, hn, m, hm, hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m
hnm : p.getVert n = p.getVert m
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) ⦃n : ℕ⦄
    (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} m)
    (hnm : Eq.{u + 1} (α := V) (getVert (G := G) (u := u) Walk.nil n) (getVert (G := G) (u := u) Walk.nil m)), n = m
⊢ n = m
have cons : ∀ {v w u : V} (h : G.Adj v w) (p : G.Walk w u)
  (ihp :
    ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
      (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m)
  (hp : (cons h p).IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ (cons h p).length} n) ⦃m : ℕ⦄
  (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ (cons h p).length} m)
  (hnm : (cons h p).getVert n = (cons h p).getVert m), n = m
Tactic: induction p generalizing n m with
  | nil => simp_all
  | @cons v w u h p ihp =>
    simp only [length_cons, Set.mem_setOf_eq] at hn hm hnm
    by_cases hn0 : n = 0 <;> by_cases hm0 : m = 0
    · lia
    · simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
      have hvp : v ∉ p.support := by aesop
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by lia⟩⟩)).elim
    · simp only [hm0, Walk.getVert_cons p h hn0] at hnm
      have hvp : v ∉ p.support := by simp_all
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by lia⟩⟩)).elim
    · simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
      have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
      lia
Cleared hypotheses: p, hp, n, hn, m, hm, hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h : ¬p.Nil
⊢ p.getVert i = u ↔ i = 0
have refine : ∀ (h : p.getVert i = u), i = 0
Tactic: refine ⟨fun h ↦ ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
⊢ i = 0
have pos : ∀ (h' : i ≤ p.length), i = 0
Tactic: by_cases h' : i ≤ p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
pos : ∀ (h' : i ≤ p.length), i = 0
⊢ i = 0
have neg : ∀ (h' : ¬i ≤ p.length), i = 0
Tactic: by_cases h' : i ≤ p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i = 0
have pos : p.getVert i = p.getVert 0
Tactic: apply hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by rw [Set.mem_setOf]; lia)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : ¬i ≤ p.length
⊢ i = 0
have h₁ : w = u
Tactic: rw [p.getVert_of_length_le (le_of_not_ge h')] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : w = u
h' : ¬i ≤ p.length
⊢ i = 0
have neg : ∀ {p : G.Walk w w} (hp : p.IsPath) (h : ¬p.Nil) (h' : ¬i ≤ p.length), i = 0
Tactic: subst h
Cleared hypotheses: u, p, hp, h_1, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0
have nil : ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hi : i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil),
  getVert (G := G) (u := u) Walk.nil i = u ↔ i = 0
Tactic: cases p
Cleared hypotheses: w, p, hp, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
nil :
  ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hi : i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil),
    getVert (G := G) (u := u) Walk.nil i = u ↔ i = 0
⊢ p.getVert i = u ↔ i = 0
have cons : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v w) (hp : (cons h p).IsPath) (hi : i ≤ (cons h p).length),
  (cons h p).getVert i = u ↔ i = 0
Tactic: cases p
Cleared hypotheses: p, hp, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = w ↔ i = p.length
have this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
Tactic: have := hp.reverse.getVert_eq_start_iff (by lia : p.reverse.length - i ≤ p.reverse.length)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.getVert i = w ↔ i = p.length
have this₁ : p.getVert i = w ↔ p.length - i = 0
Tactic: simp only [length_reverse, getVert_reverse, show p.length - (p.length - i) = i by lia] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.getVert i = w ↔ i = p.length
have rw : p.length - i = 0 ↔ i = p.length
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i : ℕ | i ≤ p.length} ↔ p.IsPath
have refine : Set.InjOn p.getVert {i : ℕ | i ≤ p.length} → p.IsPath
Tactic: refine ⟨?_, fun a => a.getVert_injOn⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
⊢ (cons h q).IsPath
have cons : q.IsPath ∧ u_1 ∉ q.support
Tactic: rw [cons_isPath_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n = m
have this : n + 1 = m + 1
Tactic: have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
⊢ q.IsPath ∧ u_1 ∉ q.support
have cons : ∀ (h' : u_1 ∈ q.support), False
Tactic: refine ⟨ih (by
      intro n hn m hm hnm
      simp only [Set.mem_setOf_eq] at hn hm
      have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia), fun h' => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
h' : u_1 ∈ q.support
⊢ False
have cons : ∀ (n : ℕ) (hn : q.getVert n = u_1) (hnl : n ≤ q.length), False
Tactic: obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
h' : u_1 ∈ q.support
n : ℕ
hn : q.getVert n = u_1
hnl : n ≤ q.length
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert 0
have rwa : q.getVert (n + 1 - 1) = (cons h q).getVert 0
Tactic: rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
h' : u_1 ∈ q.support
n : ℕ
hn : q.getVert n = u_1
hnl : n ≤ q.length
rwa : q.getVert (n + 1 - 1) = (cons h q).getVert 0
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert 0
have rwa₁ : q.getVert (n + 1 - 1) = u_1
Tactic: rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length}
h' : u_1 ∈ q.support
n : ℕ
hn : q.getVert n = u_1
hnl : n ≤ q.length
⊢ False
have this : n + 1 = 0
Tactic: have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i : ℕ | i ≤ p.length} → p.IsPath
have nil : ∀ {u : V},
  Set.InjOn.{0, u} (β := V) (getVert (G := G) (u := u) Walk.nil)
      {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} →
    IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
Tactic: induction p with
  | nil => simp
  | cons h q ih =>
    intro hinj
    rw [cons_isPath_iff]
    refine ⟨ih (by
      intro n hn m hm hnm
      simp only [Set.mem_setOf_eq] at hn hm
      have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia), fun h' => ?_⟩
    obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
    have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
    lia
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Set.InjOn.{0, u} (β := V) (getVert (G := G) (u := u) Walk.nil)
        {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} →
      IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ Set.InjOn p.getVert {i : ℕ | i ≤ p.length} → p.IsPath
have cons : ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w) (ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath),
  Set.InjOn (cons h q).getVert {i : ℕ | i ≤ (cons h q).length} → (cons h q).IsPath
Tactic: induction p with
  | nil => simp
  | cons h q ih =>
    intro hinj
    rw [cons_isPath_iff]
    refine ⟨ih (by
      intro n hn m hm hnm
      simp only [Set.mem_setOf_eq] at hn hm
      have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia), fun h' => ?_⟩
    obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
    have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
    lia
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
⊢ w = p.snd
have hnil : ¬p.Nil
Tactic: have hnil := edges_eq_nil.not.mp <| List.ne_nil_of_mem hmem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
hnil : ¬p.Nil
⊢ w = p.snd
have hmem₁ : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
Tactic: rw [← cons_tail_eq _ hnil, edges_cons, List.mem_cons, Sym2.eq, Sym2.rel_iff'] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ u ∉ p.tail.support
have nil : ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil)
  (hmem :
    ((u, w) = (u, snd (G := G) (u := u) Walk.nil) ∨ (u, w) = Prod.swap (u, snd (G := G) (u := u) Walk.nil)) ∨
      Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil))
        s(u, w)),
  u ∉ support (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
Tactic: induction p
Cleared hypotheses: p, hp, hnil, hmem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil)
    (hmem :
      ((u, w) = (u, snd (G := G) (u := u) Walk.nil) ∨ (u, w) = Prod.swap (u, snd (G := G) (u := u) Walk.nil)) ∨
        Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil))
          s(u, w)),
    u ∉ support (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
⊢ u ∉ p.tail.support
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (hp : p.IsPath) (hnil : ¬p.Nil) (hmem : ((v, w) = (v, p.snd) ∨ (v, w) = (v, p.snd).swap) ∨ s(v, w) ∈ p.tail.edges),
      v ∉ p.tail.support) →
    ∀ (hp : (cons h p).IsPath) (hnil : ¬(cons h p).Nil)
      (hmem : ((u, w) = (u, (cons h p).snd) ∨ (u, w) = (u, (cons h p).snd).swap) ∨ s(u, w) ∈ (cons h p).tail.edges),
      u ∉ (cons h p).tail.support
Tactic: induction p
Cleared hypotheses: p, hp, hnil, hmem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd
have this : u ∉ p.tail.support
Tactic: have : u ∉ p.tail.support := by induction p <;> simp_all
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} u
v : V
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} v
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') u : V') ((f : (a : V) → V') v : V')
⊢ u = v
have obtain : ∀ (u : Fin p.support.length) (hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u))
  (hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') v : V')),
  p.support.get u = v
Tactic: obtain ⟨u, rfl⟩ := List.get_of_mem hu
Cleared hypotheses: u, hu, hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
v : V
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} v
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') v : V')
⊢ p.support.get u = v
have obtain : ∀ (v : Fin p.support.length) (hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v))
  (hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')),
  p.support.get u = p.support.get v
Tactic: obtain ⟨v, rfl⟩ := List.get_of_mem hv
Cleared hypotheses: v, hv, hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
⊢ p.support.get u = p.support.get v
have e_a : u = v
Tactic: congr