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 v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
inr₈ inr₉ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₁₀ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
inr₈ inr₉ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₁₀ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₁₁ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.edges.Nodup
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
inr₈ inr₉ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₁₀ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → s(u, v) ∉ p.edges
inr₁₁ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₁₂ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → cons h p ≠ nil
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
inr₈ inr₉ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₁₀ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → s(u, v) ∉ p.edges
inr₁₁ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.edges.Nodup
inr₁₂ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → cons h p ≠ nil
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₁₃ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.support.Nodup
Tactic: tauto
Cleared hypotheses: 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.IsCycle
⊢ p.reverse.IsCycle
have simp : ∀ (h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup), p.reverse.IsTrail ∧ p.reverse ≠ nil ∧ p.support.tail.Nodup
Tactic: simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢
Cleared hypotheses: h
-- 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
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
⊢ q.IsPath
have this : (p.append q).support.tail.Nodup
Tactic: have := hcyc.2
-- 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
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : (p.append q).support.tail.Nodup
⊢ q.IsPath
have this₁ : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
Tactic: rw [tail_support_append, List.nodup_append'] at this
Cleared hypotheses: 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
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath
have rw : v ∉ q.support.tail ∧ q.support.tail.Nodup
Tactic: rw [isPath_def, ← cons_tail_support, List.nodup_cons]
-- 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
⊢ p.tail.IsPath
have nil : ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil),
  IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
Tactic: cases p with
  | nil => simp
  | cons hadj p =>
    simp_all [Walk.isPath_def]
Cleared hypotheses: v, p, hp
-- 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
nil :
  ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil),
    IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
⊢ p.tail.IsPath
have cons : ∀ {v_1 : V} (hadj : G.Adj u v_1) (p : G.Walk v_1 v) (hp : (cons hadj p).IsPath), (cons hadj p).tail.IsPath
Tactic: cases p with
  | nil => simp
  | cons hadj p =>
    simp_all [Walk.isPath_def]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
have have : ∀ (this : Fintype (↑G.edgeSet : Type u)),
  ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Tactic: have := Fintype.ofFinite G.edgeSet
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
have this₁ : s.Finite
Tactic: have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
have obtain : ∀ (x : V),
  ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Tactic: obtain ⟨x⟩ := N
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
have obtain : ∀ (w : ℕ) (hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w) (u v : V) (p : G.Walk u v) (hp : p.IsTrail),
  p.length = w →
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Tactic: obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
have refine : ∀ (u' v' : V) (p' : G.Walk u' v') (hp' : p'.IsTrail), p'.length ≤ p.length
Tactic: refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsTrail
⊢ p'.length ≤ p.length
have this₁ : w ≤ p'.length → p'.length ≤ w
Tactic: have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
have have : ∀ (this : Fintype (↑G.edgeSet : Type u)),
  ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
Tactic: have := Fintype.ofFinite G.edgeSet
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
have this₁ : s.Finite
Tactic: have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.isTrail.length_le_card_edgeFinset
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
have obtain : ∀ (x : V),
  ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
Tactic: obtain ⟨x⟩ := N
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
have obtain : ∀ (w : ℕ) (hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w) (u v : V) (p : G.Walk u v) (hp : p.IsPath),
  p.length = w →
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
Tactic: obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
have refine : ∀ (u' v' : V) (p' : G.Walk u' v') (hp' : p'.IsPath), p'.length ≤ p.length
Tactic: refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsPath
⊢ p'.length ≤ p.length
have this₁ : w ≤ p'.length → p'.length ≤ w
Tactic: have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-- 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 u' v_1 w : V
p_1 : G.Walk u_1 v_1
f : G →g G'
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.IsPath
have rw : Decidable p.support.Nodup
Tactic: rw [isPath_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.length < Fintype.card V
have rw : p.support.length ≤ Fintype.card V
Tactic: rw [Nat.lt_iff_add_one_le, ← length_support]
-- 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
⊢ n = m
have pos : ∀ (hn0 : n = 0), n = m
Tactic: by_cases hn0 : n = 0
-- 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
pos : ∀ (hn0 : n = 0), n = m
⊢ n = m
have neg : ∀ (hn0 : ¬n = 0), n = m
Tactic: by_cases hn0 : n = 0
-- 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
⊢ n = m
have pos : ∀ (hm0 : m = 0), n = m
Tactic: by_cases hm0 : m = 0
-- 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 (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
⊢ n = m
have pos : ∀ (hm0 : m = 0), n = m
Tactic: by_cases hm0 : m = 0