awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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')
⊢ u = v
have this : Injective.{1, v + 1} (β := V') fun (i : Fin (Walk.map f p).support.length) ↦
  getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (Walk.map f p).support (↑i : ℕ) sorry
Tactic: have := List.nodup_iff_injective_getElem.mp h.support_nodup
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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')
this :
  Injective.{1, v + 1} (β := V') fun (i : Fin (Walk.map f p).support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (Walk.map f p).support (↑i : ℕ) ⋯
⊢ u = v
have this₁ : Injective.{1, v + 1} (β := V') fun (i : Fin p.support.length) ↦
  getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) sorry
Tactic: rw! (castMode := .all) [support_map, List.length_map] at this
Cleared hypotheses: this
-- 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')
this :
  Injective.{1, v + 1} (β := V') fun (i : Fin p.support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) ⋯
⊢ u = v
have e_a : Eq.{v + 1} (α := V')
  ((fun (i : Fin p.support.length) ↦
      getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) sorry)
    u)
  ((fun (i : Fin p.support.length) ↦
      getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) sorry)
    v)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i : ℕ | 1 ≤ i ∧ i ≤ p.length}
have hpc₁ : (cons sorry p.tail).IsCycle
Tactic: rw [← p.cons_tail_eq hpc.not_nil] at hpc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} m
hnm : p.getVert n = p.getVert m
⊢ n = m
have rw : ∀ (hn : 1 ≤ n ∧ n ≤ p.tail.length + 1) ⦃m : ℕ⦄ (hm : 1 ≤ m ∧ m ≤ p.tail.length + 1) (hnm : p.getVert n = p.getVert m),
  n = m
Tactic: rw [← SimpleGraph.Walk.length_tail_add_one
    (p.not_nil_of_tail_not_nil (not_nil_of_isCycle_cons hpc)), Set.mem_setOf] at hn hm
Cleared hypotheses: hn, m, hm, hnm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n = m
have this : n - 1 = m - 1
Tactic: have := ((Walk.cons_isCycle_iff _ _).mp hpc).1.getVert_injOn
    (by lia : n - 1 ≤ p.tail.length) (by lia : m - 1 ≤ p.tail.length)
    (by simp_all)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
⊢ n = m
have this : 3 ≤ p.length
Tactic: have := hpc.three_le_length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.reverse.length} (p.reverse.length - n)
have simp : 1 ≤ p.length - n ∧ p.length - n ≤ p.length
Tactic: simp only [Walk.length_reverse, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.reverse.length} (p.reverse.length - m)
have simp : 1 ≤ p.length - m ∧ p.length - m ≤ p.length
Tactic: simp only [Walk.length_reverse, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ n = m
have this₁ : p.length - n = p.length - m
Tactic: have : p.length - n = p.length - m := Walk.length_reverse _ ▸ hpc.reverse.getVert_injOn
    (by simp only [Walk.length_reverse, Set.mem_setOf_eq]; lia)
    (by simp only [Walk.length_reverse, Set.mem_setOf_eq]; lia)
    (by simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by lia, hnm,
      show p.length - (p.length - m) = m by lia])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
⊢ False
have this : 3 ≤ p.length
Tactic: have := hp.three_le_length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} 1
have simp : 1 ≤ p.length
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} (p.length - 1)
have simp : 1 ≤ p.length - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ False
have h₁ : 1 = p.length - 1
Tactic: apply hp.getVert_injOn (by simp; lia) (by simp; lia) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0 ∨ i = p.length
have refine : p.getVert i = u → i = 0 ∨ i = p.length
Tactic: refine ⟨?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → i = 0 ∨ i = p.length
have rw : p.getVert i = u → ¬i = 0 → i = p.length
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False
have hl : 3 ≤ p.length
Tactic: have hl := hpc.three_le_length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
⊢ False
have pos : ∀ (hi' : i ≥ p.length - 1), False
Tactic: by_cases hi' : i ≥ p.length - 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
pos : ∀ (hi' : i ≥ p.length - 1), False
⊢ False
have neg : ∀ (hi' : ¬i ≥ p.length - 1), False
Tactic: by_cases hi' : i ≥ p.length - 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False
have h'₁ : i - 1 = 0 ∨ i - 1 = p.length
Tactic: rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'
Cleared hypotheses: h', hl, hi'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length - 1} (i - 1)
have simp : i ≤ p.length - 1 + 1
Tactic: simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ False
have this : i - 1 = i + 1
Tactic: have := hpc.getVert_injOn' (by simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]; lia)
    (by simp only [Set.mem_setOf_eq]; lia) h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length
have refine : p.tail.IsPath ∧ 3 ≤ p.length → ∀ (h₁ : p.tail.IsPath) (h₂ : 3 ≤ p.length), p.IsCycle
Tactic: refine ⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₁ : (cons h' p).tail.IsPath
h₂ : 3 ≤ (cons h' p).length
⊢ (cons h' p).IsCycle
have h₃ : p.IsPath
Tactic: simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
⊢ (cons h' p).IsCycle
have cons : ∀ (hh : s(u, v) ∈ p.edges), False
Tactic: refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
⊢ False
have this : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 sorry =
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) sorry
Tactic: have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
this :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯
⊢ False
have this₁ : (⟨0, sorry⟩ : Fin p.support.length) = ⟨p.length - 1, sorry⟩
Tactic: have := p.isPath_iff_injective_get_support.mp h₁ this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.tail.IsPath ∧ 3 ≤ p.length
h₁ : p.tail.IsPath
h₂ : 3 ≤ p.length
⊢ p.IsCycle
have nil : IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) nil) (tail nil) ∧
    3 ≤ length.{u} (V := V) (G := G) (u := u) nil →
  ∀ (h₁ : IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) nil) (tail nil))
    (h₂ : 3 ≤ length.{u} (V := V) (G := G) (u := u) nil), IsCycle.{u} (V := V) (G := G) (u := u) nil
Tactic: cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia
Cleared hypotheses: p, h, h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.tail.IsPath ∧ 3 ≤ p.length
h₁ : p.tail.IsPath
h₂ : 3 ≤ p.length
nil :
  IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil) ∧
      3 ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil →
    ∀ (h₁ : IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil))
      (h₂ : 3 ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil), IsCycle.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ p.IsCycle
have cons : ∀ {v : V} (h' : G.Adj u v) (p : G.Walk v u),
  (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length →
    ∀ (h₁ : (cons h' p).tail.IsPath) (h₂ : 3 ≤ (cons h' p).length), (cons h' p).IsCycle
Tactic: cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia
Cleared hypotheses: p, h, h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
have rwa : ∀ (hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail), ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
Tactic: rwa [← take_spec _ h] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
have rwa : ∀ (hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsPath), ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
Tactic: rwa [← take_spec _ h] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail
have rw : (c.rotate u hu).edges.Nodup ↔ c.IsTrail
Tactic: rw [isTrail_def, isTrail_def, (c.rotate_edges u hu).perm.nodup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
rw : (c.rotate u hu).edges.Nodup ↔ c.IsTrail
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail
have rw₁ : (c.rotate u hu).edges.Nodup ↔ c.edges.Nodup
Tactic: rw [isTrail_def, isTrail_def, (c.rotate_edges u hu).perm.nodup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
rw : (c.rotate u hu).edges.Nodup ↔ c.IsTrail
rw₁ : (c.rotate u hu).edges.Nodup ↔ c.edges.Nodup
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail
have rw₂ : c.edges.Nodup ↔ c.edges.Nodup
Tactic: rw [isTrail_def, isTrail_def, (c.rotate_edges u hu).perm.nodup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
⊢ (c.takeUntil w h).IsPath
have pos : ∀ (hvw : v = w), (c.takeUntil w h).IsPath
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
pos : ∀ (hvw : v = w), (c.takeUntil w h).IsPath
⊢ (c.takeUntil w h).IsPath
have neg : ∀ (hvw : ¬v = w), (c.takeUntil w h).IsPath
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath
have pos : ∀ (h : v ∈ c.support), (c.takeUntil v h).IsPath
Tactic: subst hvw
Cleared hypotheses: w, h, hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
h₁ : w ∈ c.support
⊢ (c.takeUntil w h).IsPath
have hc₁ : ((c.dropUntil w h₁).reverse.append (c.takeUntil w h₁).reverse).IsCycle
Tactic: rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc
Cleared hypotheses: hc, h, hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
⊢ List.count v c.support = 2
have this : List.count v c.support.tail = 1
Tactic: have := List.count_eq_one_of_mem hc.support_nodup <| c.end_mem_tail_support hc.not_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
this : List.count v c.support.tail = 1
⊢ List.count v c.support = 2
have this₁ : c.support.head? = some v
Tactic: have := c.head_support ▸ List.head?_eq_some_head c.support_ne_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
⊢ List.count u c.support = 1
have this : u = c.support.head sorry ∨ u ∈ c.support.tail
Tactic: have := List.eq_or_mem_of_mem_cons <| List.cons_head_tail c.support_ne_nil ▸ hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this : u = c.support.head ⋯ ∨ u ∈ c.support.tail
⊢ List.count u c.support = 1
have this₁ : List.count u c.support.tail = 1
Tactic: have := List.count_eq_one_of_mem hc.support_nodup <| this.resolve_left <| head_support _ ▸ hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this_1 : u = c.support.head ⋯ ∨ u ∈ c.support.tail
this : List.count u c.support.tail = 1
⊢ List.count u c.support = 1
have this₁ : c.support.head? = some v
Tactic: have := c.head_support ▸ List.head?_eq_some_head c.support_ne_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : v ∈ (p.takeUntil w hw).support
⊢ False
have hv₁ : ∃ (n : ℕ), (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
Tactic: rw [Walk.mem_support_iff_exists_getVert] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : ∃ (n : ℕ), (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
⊢ False
have obtain : ∀ (n : ℕ) (hn : (p.takeUntil w hw).getVert n = v) (hnl : n ≤ (p.takeUntil w hw).length), False
Tactic: obtain ⟨n, ⟨hn, hnl⟩⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : (p.takeUntil w hw).getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ False
have hn₁ : p.getVert n = v
Tactic: rw [getVert_takeUntil hw hnl] at hn
Cleared hypotheses: hn, hnl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ False
have this : (p.takeUntil w hw).length < p.length
Tactic: have := p.length_takeUntil_lt hw h.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ False
have this₁ : n = p.length
Tactic: have : n = p.length := hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by simp)
    (hn.symm ▸ p.getVert_length.symm)
-- 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
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
have refine_1 : ∀ (hp : p.IsPath) (v_1 : V) (w : G.Walk v_1 v_1) (hwp : w.IsSubwalk p), w.Nil
Tactic: refine ⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩
-- 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
refine_1 : ∀ (hp : p.IsPath) (v_1 : V) (w : G.Walk v_1 v_1) (hwp : w.IsSubwalk p), w.Nil
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
have refine_2 : ∀ (h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil), p.support.Nodup
Tactic: refine ⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩
-- 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
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
⊢ p.support.Nodup
have refine_2 : ∀ (i j : ℕ) (x : i < p.support.length) (x_1 : j < p.support.length),
  i < j →
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i x =
        getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j x_1 →
      False
Tactic: refine List.pairwise_iff_getElem.mpr fun i j _ _ _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
⊢ False
have this : ¬p'.Nil
Tactic: have : ¬p'.Nil := by grind [nil_drop_iff, take_length]