awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
⊢ p.IsPath → ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle

Tactic:
grind [isPath_iff_isSubwalk_imp_nil, IsCycle.not_nil]

Premises used: SimpleGraph.Walk.isPath_iff_isSubwalk_imp_nil, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
refine : ∀ (h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle), p.IsPath
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle

Tactic:
refine ⟨by grind [isPath_iff_isSubwalk_imp_nil, IsCycle.not_nil], fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
h : ∀ (v : V) (w : G.Walk v v), w.IsSubwalk (u₂ := u) Walk.nil → ¬w.IsCycle
⊢ IsPath.{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_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
⊢ p.IsPath

Tactic:
have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
⊢ (cons hadj p).IsPath

Tactic:
cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons, And.intro, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
refine_1 : ∀ (hup : u ∈ p.support), (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)
refine_2 : ∀ (hup : u ∈ p.support), (cons hadj (p.takeUntil u hup)).IsCycle
⊢ (cons hadj p).IsPath

Tactic:
refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons, And.intro, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
refine_1 : u :: (p.takeUntil u hup).support <:+: u :: p.support
⊢ (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)

Tactic:
rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]

Premises used: SimpleGraph.Walk.support_cons, SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: u :: p.support

Tactic:
(List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix

Premises used: Iff.mpr, SimpleGraph.Walk.support_takeUntil_prefix_support, List.IsPrefix.isInfix, List.prefix_cons_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: u :: p.support

Tactic:
exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix

Premises used: Iff.mpr, SimpleGraph.Walk.support_takeUntil_prefix_support, List.IsPrefix.isInfix, List.prefix_cons_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle

Tactic:
cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons_isCycle_iff, And.intro, SimpleGraph.Walk.IsPath.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
refine_2 : ∀ (he : s(u, v_2) ∈ (p.takeUntil u hup).edges), False
⊢ (cons hadj (p.takeUntil u hup)).IsCycle

Tactic:
refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons_isCycle_iff, And.intro, SimpleGraph.Walk.IsPath.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
he : s(u, v_2) ∈ (p.takeUntil u hup).edges
⊢ False

Tactic:
ht.edges_nodup.notMem <| p.edges_takeUntil_subset hup he

Premises used: SimpleGraph.Walk.IsTrail.edges_nodup, SimpleGraph.Walk.edges_takeUntil_subset, List.Nodup.notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
he : s(u, v_2) ∈ (p.takeUntil u hup).edges
⊢ False

Tactic:
exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset hup he

Premises used: SimpleGraph.Walk.IsTrail.edges_nodup, SimpleGraph.Walk.edges_takeUntil_subset, List.Nodup.notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
⊢ p.IsPath

Tactic:
match p with
  | .nil => simp
  | .cons hadj p =>
    have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
    refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
    · rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix
    · refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset hup he
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
⊢ p.IsPath

Tactic:
classical
  match p with
  | .nil => simp
  | .cons hadj p =>
    have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
    refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
    · rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix
    · refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset hup he
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Path u v
⊢ (↑p : G.Walk u v).IsPath

Tactic:
p.property

Premises used: Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Path u v
⊢ (↑p : G.Walk u v).IsTrail

Tactic:
p.property.isTrail

Premises used: SimpleGraph.Walk.IsPath.isTrail, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
h : G.Adj u v
⊢ (Walk.cons h Walk.nil).IsPath

Tactic:
simp [h.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ s(u, v) ∈ (↑(singleton h) : G.Walk u v).edges

Tactic:
simp [singleton]

Premises used: SimpleGraph.Path.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Path u v
hw : w ∈ (↑p : G.Walk u v).support
⊢ List.count w (↑p : G.Walk u v).support = 1

Tactic:
List.count_eq_one_of_mem p.property.support_nodup hw

Premises used: List.count_eq_one_of_mem, SimpleGraph.Walk.IsPath.support_nodup, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Path u v
e : Sym2 V
hw : e ∈ (↑p : G.Walk u v).edges
⊢ List.count e (↑p : G.Walk u v).edges = 1

Tactic:
List.count_eq_one_of_mem p.property.isTrail.edges_nodup hw

Premises used: SimpleGraph.Walk.IsPath.isTrail, SimpleGraph.Walk.IsTrail.edges_nodup, List.count_eq_one_of_mem, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Path u v
⊢ (↑p : G.Walk u v).support.Nodup

Tactic:
(Walk.isPath_def _).mp p.property

Premises used: SimpleGraph.Walk.isPath_def, Iff.mp, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
nil :
  ∀ (h : Walk.IsPath.{u} (V := V) (G := G) (u := v) Walk.nil),
    Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) Walk.nil h = Path.nil
cons :
  ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 v) (h_1 : (Walk.cons h p).IsPath),
    Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) (Walk.cons h p) h_1 = Path.nil
⊢ p = Path.nil

Tactic:
obtain ⟨_ | _, h⟩ := p
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
h : Walk.IsPath.{u} (V := V) (G := G) (u := v) Walk.nil
⊢ Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) Walk.nil h = Path.nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v v_1 : V
h_1 : G.Adj v v_1
p : G.Walk v_1 v
h : (Walk.cons h_1 p).IsPath
⊢ Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) (Walk.cons h_1 p) h = Path.nil

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
p : G.Path v v
⊢ e ∉ (↑p : G.Walk v v).edges

Tactic:
simp [p.loop_eq]

Premises used: SimpleGraph.Path.loop_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Path v u
h : G.Adj u v
he : s(u, v) ∉ (↑p : G.Walk v u).edges
⊢ (Walk.cons h (↑p : G.Walk v u)).IsCycle

Tactic:
simp [Walk.isCycle_def, Walk.isTrail_cons, he]

Premises used: SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.isTrail_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u u' v v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
subst_vars : ∀ (p : G.Walk u' v'), (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯
⊢ (p.copy hu hv).bypass = p.bypass.copy hu hv

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 : V
⊢ IsPath.{u} (V := V) (G := G) (u := u_1) (bypass nil)

Tactic:
simp!
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
pos : ∀ (hs : u_1 ∈ p'.bypass.support), (p'.bypass.dropUntil u_1 hs).IsPath
neg : ∀ (hs : u_1 ∉ p'.bypass.support), (cons h p'.bypass).IsPath
⊢ IsPath.{u} (V := V) (G := G) (u := u_1) (v := w)
    (if hs : u_1 ∈ p'.bypass.support then p'.bypass.dropUntil u_1 hs else cons h p'.bypass)

Tactic:
split_ifs with hs
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
hs : u_1 ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u_1 hs).IsPath

Tactic:
ih.dropUntil hs

Premises used: SimpleGraph.Walk.IsPath.dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
hs : u_1 ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u_1 hs).IsPath

Tactic:
exact ih.dropUntil hs

Premises used: SimpleGraph.Walk.IsPath.dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
hs : u_1 ∉ p'.bypass.support
⊢ (cons h p'.bypass).IsPath

Tactic:
simp [*, cons_isPath_iff]

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, IsPath.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)
cons : ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w) (ih : p'.bypass.IsPath), (Walk.cons h p').bypass.IsPath
⊢ p.bypass.IsPath

Tactic:
induction p with
  | nil => simp!
  | cons _ p' ih =>
    simp only [bypass]
    split_ifs with hs
    · exact ih.dropUntil hs
    · simp [*, cons_isPath_iff]

Premises used: SimpleGraph.Walk.bypass, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 : V
⊢ length.{u} (V := V) (G := G) (u := u_1) (bypass nil) ≤ length.{u} (V := V) (G := G) (u := u_1) (bypass nil)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
pos : ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
neg : u_1 ∉ p.bypass.support → (cons h p.bypass).length ≤ (cons h p).length
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ≤
    (cons h p).length

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
trans : (p.bypass.dropUntil u_1 h_1).length ≤ p.bypass.length
trans₁ : p.bypass.length ≤ (cons h p).length
trans₂ : ℕ
⊢ (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length

Tactic:
trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
⊢ (p.bypass.dropUntil u_1 h_1).length ≤ p.bypass.length

Tactic:
apply length_dropUntil_le

Premises used: SimpleGraph.Walk.length_dropUntil_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
⊢ p.bypass.length ≤ p.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∉ p.bypass.support
⊢ p.bypass.length + 1 ≤ p.length + 1

Tactic:
Nat.add_le_add_right ih 1

Premises used: Nat.add_le_add_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∉ p.bypass.support
⊢ p.bypass.length + 1 ≤ p.length + 1

Tactic:
exact Nat.add_le_add_right ih 1

Premises used: Nat.add_le_add_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil) ≤ length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.length ≤ p.length),
    (Walk.cons h p).bypass.length ≤ (Walk.cons h p).length
⊢ p.bypass.length ≤ p.length

Tactic:
induction p with
  | nil => rfl
  | cons _ _ ih =>
    simp only [bypass]
    split_ifs
    · trans
      · apply length_dropUntil_le
      rw [length_cons]
      lia
    · rw [length_cons, length_cons]
      exact Nat.add_le_add_right ih 1

Premises used: SimpleGraph.Walk.bypass, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_cons, SimpleGraph.Walk.length_dropUntil_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 : V
h : length.{u} (V := V) (G := G) (u := u_1) nil ≤ length.{u} (V := V) (G := G) (u := u_1) (bypass nil)
⊢ Eq.{u + 1} (α := G.Walk u_1 u_1) (bypass nil) nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
pos : ∀ (hb : u_1 ∈ p.bypass.support), p.bypass.dropUntil u_1 hb = cons h_1 p
neg : ∀ (hb : u_1 ∉ p.bypass.support), cons h_1 p.bypass = cons h_1 p
⊢ (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h_1 p.bypass) = cons h_1 p

Tactic:
split_ifs with hb
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∈ p.bypass.support
pos : False
⊢ p.bypass.dropUntil u_1 hb = cons h_1 p

Tactic:
exfalso
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∈ p.bypass.support
⊢ p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length

Tactic:
simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h

Premises used: dif_pos, SimpleGraph.Walk.bypass, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
pos : p.length.succ ≤ p.length
⊢ False

Tactic:
apply Nat.not_succ_le_self p.length

Premises used: SimpleGraph.Walk.length, Nat.not_succ_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
⊢ p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length

Tactic:
h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
⊢ (p.bypass.dropUntil u_1 ⋯).length ≤ p.bypass.length

Tactic:
Walk.length_dropUntil_le p.bypass hb

Premises used: SimpleGraph.Walk.bypass, SimpleGraph.Walk.length_dropUntil_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
⊢ p.bypass.length ≤ p.length

Tactic:
Walk.length_bypass_le _

Premises used: SimpleGraph.Walk.length_bypass_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
⊢ p.length.succ ≤ p.length

Tactic:
calc p.length + 1
        _ ≤ (p.bypass.dropUntil _ _).length := h
        _ ≤ p.bypass.length := Walk.length_dropUntil_le p.bypass hb
        _ ≤ p.length := Walk.length_bypass_le _

Premises used: SimpleGraph.Walk.length_bypass_le, SimpleGraph.Walk.length, SimpleGraph.Walk.bypass, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.length_dropUntil_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∉ p.bypass.support
⊢ p.length ≤ p.bypass.length

Tactic:
simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg,
        Nat.add_le_add_iff_right] at h

Premises used: Nat.add_le_add_iff_right, SimpleGraph.Walk.bypass, dif_neg, SimpleGraph.Walk.length_cons, not_false_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∉ p.bypass.support
h : p.length ≤ p.bypass.length
neg neg₁ : cons h_1 p = cons h_1 p
⊢ cons h_1 p.bypass = cons h_1 p

Tactic:
rw [ih h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.length ≤ p.bypass.length
nil :
  ∀ {u : V}
    (h : length.{u} (V := V) (G := G) (u := u) Walk.nil ≤ length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)),
    Eq.{u + 1} (α := G.Walk u u) (bypass Walk.nil) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p)
    (h_1 : (Walk.cons h p).length ≤ (Walk.cons h p).bypass.length), (Walk.cons h p).bypass = Walk.cons h p
⊢ p.bypass = p

Tactic:
induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [Walk.bypass]
    split_ifs with hb
    · exfalso
      simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h
      apply Nat.not_succ_le_self p.length
      calc p.length + 1
        _ ≤ (p.bypass.dropUntil _ _).length := h
        _ ≤ p.bypass.length := Walk.length_dropUntil_le p.bypass hb
        _ ≤ p.length := Walk.length_bypass_le _
    · simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg,
        Nat.add_le_add_iff_right] at h
      rw [ih h]

Premises used: Nat.add_le_add_iff_right, SimpleGraph.Walk.length_bypass_le, SimpleGraph.Walk.length, dif_pos, SimpleGraph.Walk.bypass, dif_neg, SimpleGraph.Walk.cons, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_cons, not_false_iff, Nat.not_succ_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 : V
⊢ Subset.{u} (α := List V) (support (G := G) (u := u_1) (bypass nil)) (support (G := G) (u := u_1) nil)

Tactic:
simp!