awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset

Tactic:
mem_edgeFinset.mpr ?_

Premises used: Iff.mpr, SimpleGraph.mem_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
refine : e ∈ G.edgeSet
⊢ e ∈ G.edgeFinset

Tactic:
refine mem_edgeFinset.mpr ?_

Premises used: Iff.mpr, SimpleGraph.mem_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
a : e ∈ w.edges
⊢ e ∈ G.edgeSet

Tactic:
apply w.edges_subset_edgeSet

Premises used: SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ w.edges

Tactic:
simpa [edges] using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges ⊆ G.edgeFinset

Tactic:
have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this_1 : edges.card = w.length
this : edges ⊆ G.edgeFinset
⊢ edges.card ≤ G.edgeFinset.card

Tactic:
Finset.card_le_card this

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this_1 : edges.card = w.length
this : edges ⊆ G.edgeFinset
⊢ edges.card ≤ G.edgeFinset.card

Tactic:
exact Finset.card_le_card this

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
let let₁ let₂ : w.length ≤ G.edgeFinset.card
let₃ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length), w.length ≤ G.edgeFinset.card
let₄ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length), edges.card ≤ G.edgeFinset.card
let₅ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length) (this : edges ⊆ G.edgeFinset), edges.card ≤ G.edgeFinset.card
⊢ w.length ≤ G.edgeFinset.card

Tactic:
classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
isTrail : IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
support_nodup : List.Nodup.{u} (α := V) (support (G := G) (u := u) Walk.nil)
⊢ IsPath.{u} (V := V) (G := G) (u := u) Walk.nil

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ List.Nodup.{u} (α := V) (support (G := G) (u := u) Walk.nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath

Tactic:
simp [isPath_def]

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
mp : (cons h p).IsPath → p.IsPath ∧ u ∉ p.support
mpr : p.IsPath ∧ u ∉ p.support → (cons h p).IsPath
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath ∧ u ∉ p.support

Tactic:
simp +contextual [isPath_def]

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ p.IsPath ∧ u ∉ p.support → (cons h p).IsPath

Tactic:
simp +contextual [isPath_def]

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hp : p.IsPath
hu : u ∉ p.support
h : G.Adj u v
⊢ (cons h p).IsPath

Tactic:
(cons_isPath_iff _ _).2 ⟨hp, hu⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
nil : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil ↔ Eq.{u + 1} (α := G.Walk u u) Walk.nil Walk.nil
cons : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v u), (Walk.cons h p).IsPath ↔ Walk.cons h p = Walk.nil
⊢ p.IsPath ↔ p = Walk.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ IsPath.{u} (V := V) (G := G) (u := u) nil ↔ Eq.{u + 1} (α := G.Walk u u) nil nil

Tactic:
simp [IsPath.nil]

Premises used: SimpleGraph.Walk.IsPath.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
p : G.Walk v u
⊢ (cons h p).IsPath ↔ cons h p = nil

Tactic:
simp [IsPath.nil]

Premises used: SimpleGraph.Walk.IsPath.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
simpa [isPath_def] using h

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
mp : p.reverse.IsPath → p.IsPath
mpr : p.IsPath → p.reverse.IsPath
⊢ p.reverse.IsPath ↔ p.IsPath

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p.reverse.reverse.IsPath

Tactic:
h.reverse

Premises used: SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
h₁ : p = p.reverse.reverse
⊢ p.IsPath

Tactic:
convert! h.reverse

Premises used: SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
h.reverse

Premises used: SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
convert! h.reverse

Premises used: SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
simp : (p.support ++ q.support.tail).Nodup → p.support.Nodup
⊢ (p.append q).IsPath → p.IsPath

Tactic:
simp only [isPath_def, support_append]

Premises used: SimpleGraph.Walk.isPath_def, SimpleGraph.Walk.support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.support ++ q.support.tail).Nodup → p.support.Nodup

Tactic:
List.Nodup.of_append_left

Premises used: List.Nodup.of_append_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.support ++ q.support.tail).Nodup → p.support.Nodup

Tactic:
exact List.Nodup.of_append_left

Premises used: List.Nodup.of_append_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).IsPath
rw : ∀ (h : (p.append q).reverse.IsPath), q.reverse.IsPath
⊢ q.IsPath

Tactic:
rw [← isPath_reverse_iff] at h ⊢

Premises used: SimpleGraph.Walk.isPath_reverse_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ (q.reverse.append p.reverse).IsPath

Tactic:
rw [reverse_append] at h

Premises used: SimpleGraph.Walk.reverse_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath

Tactic:
apply h.of_append_left

Premises used: SimpleGraph.Walk.IsPath.of_append_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsTrail
obtain : ∀ (w_1 : G.Walk v' v) (w_2 : G.Walk w w') (h : p₂ = (w_1.append p₁).append w_2), p₁.IsTrail
⊢ p₁.IsTrail

Tactic:
obtain ⟨_, _, h⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsTrail
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
⊢ ((w_1.append p₁).append w_2).IsTrail

Tactic:
rw [h] at h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsTrail
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
h₃ : ((w_1.append p₁).append w_2).IsTrail
⊢ p₂ = (w_1.append p₁).append w_2

Tactic:
rw [h] at h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h₂ : ((w_1.append p₁).append w_2).IsTrail
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsTrail

Tactic:
h₂.of_append_left.of_append_right

Premises used: SimpleGraph.Walk.IsTrail.of_append_left, SimpleGraph.Walk.IsTrail.of_append_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h₂ : ((w_1.append p₁).append w_2).IsTrail
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsTrail

Tactic:
exact h₂.of_append_left.of_append_right

Premises used: SimpleGraph.Walk.IsTrail.of_append_left, SimpleGraph.Walk.IsTrail.of_append_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsPath
obtain : ∀ (w_1 : G.Walk v' v) (w_2 : G.Walk w w') (h : p₂ = (w_1.append p₁).append w_2), p₁.IsPath
⊢ p₁.IsPath

Tactic:
obtain ⟨_, _, h⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsPath
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
⊢ ((w_1.append p₁).append w_2).IsPath

Tactic:
rw [h] at h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsPath
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
h₃ : ((w_1.append p₁).append w_2).IsPath
⊢ p₂ = (w_1.append p₁).append w_2

Tactic:
rw [h] at h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h₂ : ((w_1.append p₁).append w_2).IsPath
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsPath

Tactic:
h₂.of_append_left.of_append_right

Premises used: SimpleGraph.Walk.IsPath.of_append_right, SimpleGraph.Walk.IsPath.of_append_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h₂ : ((w_1.append p₁).append w_2).IsPath
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsPath

Tactic:
exact h₂.of_append_left.of_append_right

Premises used: SimpleGraph.Walk.IsPath.of_append_right, SimpleGraph.Walk.IsPath.of_append_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.IsPath

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
rw : (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support
⊢ (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support

Tactic:
rw [← (p.concat h).isPath_reverse_iff, ← p.isPath_reverse_iff, reverse_concat, ← List.mem_reverse,
    ← support_reverse]

Premises used: List.mem_reverse, SimpleGraph.Walk.concat, SimpleGraph.Walk.isPath_reverse_iff, SimpleGraph.Walk.support_reverse, SimpleGraph.Walk.reverse_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support

Tactic:
cons_isPath_iff h.symm p.reverse

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.reverse, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support

Tactic:
exact cons_isPath_iff h.symm p.reverse

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.reverse, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∉ p.support
h : G.Adj v w
⊢ (p.concat h).IsPath

Tactic:
(concat_isPath_iff h).mpr ⟨hp, hw⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.Walk.concat_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : (p.take k).IsPath
hle : n ≤ k
⊢ (p.take n).IsPath

Tactic:
isPath_of_isSubwalk (p.take_isSubwalk_take hle) h

Premises used: SimpleGraph.Walk.isPath_of_isSubwalk, SimpleGraph.Walk.take_isSubwalk_take
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : (p.drop k).IsPath
hle : k ≤ n
⊢ (p.drop n).IsPath

Tactic:
isPath_of_isSubwalk (p.drop_isSubwalk_drop hle) h

Premises used: SimpleGraph.Walk.drop_isSubwalk_drop, SimpleGraph.Walk.isPath_of_isSubwalk
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
n : ℕ
⊢ (p.take n).IsPath

Tactic:
isPath_of_isSubwalk (p.isSubwalk_take n) h

Premises used: SimpleGraph.Walk.isSubwalk_take, SimpleGraph.Walk.isPath_of_isSubwalk
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
n : ℕ
⊢ (p.drop n).IsPath

Tactic:
isPath_of_isSubwalk (p.isSubwalk_drop n) h

Premises used: SimpleGraph.Walk.isSubwalk_drop, SimpleGraph.Walk.isPath_of_isSubwalk
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩

Premises used: Iff.mpr, SimpleGraph.Walk.support, Membership.mem, _private.0.SimpleGraph.Walk.IsPath.mem_support_iff_exists_append.match_1, SimpleGraph.Walk.mem_support_iff_exists_append, Iff.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
refine : ∀ (hw : w ∈ p.support), ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
refine ⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
obtain :
  ∀ (q : G.Walk u w) (r : G.Walk w v) (hqr : p = q.append r),
    ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
⊢ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw

Premises used: SimpleGraph.Walk.mem_support_iff_exists_append, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
q : G.Walk u w
r : G.Walk w v
hqr : p = q.append r
⊢ (q.append r).IsPath

Tactic:
have : (q.append r).IsPath := hqr ▸ hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
q : G.Walk u w
r : G.Walk w v
hqr : p = q.append r
this : (q.append r).IsPath
⊢ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
⟨q, r, this.of_append_left, this.of_append_right, hqr⟩

Premises used: SimpleGraph.Walk.IsPath.of_append_right, SimpleGraph.Walk.IsPath.of_append_left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
q : G.Walk u w
r : G.Walk w v
hqr : p = q.append r
this : (q.append r).IsPath
⊢ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
exact ⟨q, r, this.of_append_left, this.of_append_right, hqr⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
⊢ (p.append q).support.Nodup

Tactic:
have hpq' := hpq.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.append q).support.Nodup
⊢ (p.support ++ q.support.tail).Nodup

Tactic:
rw [support_append] at hpq'

Premises used: SimpleGraph.Walk.support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
rw : p.support.Disjoint q.support.tail
⊢ p.support.Disjoint q.tail.support

Tactic:
rw [support_tail_of_not_nil q hq]

Premises used: SimpleGraph.Walk.support_tail_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail

Tactic:
List.disjoint_of_nodup_append hpq'

Premises used: List.disjoint_of_nodup_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail

Tactic:
exact List.disjoint_of_nodup_append hpq'

Premises used: List.disjoint_of_nodup_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : q.Nil
⊢ False

Tactic:
simp [nil_iff_support_eq.mp hq, hyv] at hy

Premises used: SimpleGraph.Walk.nil_iff_support_eq, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
⊢ ¬q.Nil

Tactic:
have hq : ¬q.Nil := by
    intro hq
    simp [nil_iff_support_eq.mp hq, hyv] at hy
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
rw : x ∈ q.support.tail
⊢ x ∈ q.tail.support

Tactic:
rw [support_tail_of_not_nil q hq]

Premises used: SimpleGraph.Walk.support_tail_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x = v ∨ x ∈ q.support.tail

Tactic:
rw [mem_support_iff] at hy

Premises used: SimpleGraph.Walk.mem_support_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
hy₁ : x = v ∨ x ∈ q.support.tail
⊢ ¬q.Nil

Tactic:
rw [mem_support_iff] at hy

Premises used: SimpleGraph.Walk.mem_support_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
hy.resolve_left hyv

Premises used: Or.resolve_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
exact hy.resolve_left hyv

Premises used: Or.resolve_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.tail.support

Tactic:
have hx' : x ∈ q.tail.support := by
    rw [support_tail_of_not_nil q hq]
    rw [mem_support_iff] at hy
    exact hy.resolve_left hyv
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
hx' : x ∈ q.tail.support
⊢ False

Tactic:
IsPath.disjoint_support_of_append hpq hq hx hx'

Premises used: SimpleGraph.Walk.IsPath.disjoint_support_of_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
hx' : x ∈ q.tail.support
⊢ False

Tactic:
exact IsPath.disjoint_support_of_append hpq hq hx hx'

Premises used: SimpleGraph.Walk.IsPath.disjoint_support_of_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ ¬IsCycle.{u} (V := V) (G := G) (u := u) nil

Tactic:
fun h => h.ne_nil rfl

Premises used: SimpleGraph.Walk.IsCircuit.ne_nil, SimpleGraph.Walk.IsCycle.isCircuit, Not, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
hp : IsCycle.{u} (V := V) (G := G) (u := u) nil
⊢ G ≠ ⊥

Tactic:
cases hp.ne_nil rfl

Premises used: SimpleGraph.Walk.IsCircuit.ne_nil, SimpleGraph.Walk.IsCycle.isCircuit, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
u v : V
h : Adj ⊥ u v
p : Walk ⊥ v u
hp : (cons h p).IsCycle
⊢ False

Tactic:
h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
u v : V
h : Adj ⊥ u v
p : Walk ⊥ v u
hp : (cons h p).IsCycle
⊢ False

Tactic:
exact h