-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma bypass_eq_self_of_length_le {u v : V} (p : G.Walk u v) (h : p.length ≤ p.bypass.length) :
    p.bypass = p

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u✝ ⋯).length
⊢ False

Tactic:
apply Nat.not_succ_le_self p.length

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u✝ ⋯).length
⊢ p.length.succ ≤ p.length

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∈ p.bypass.support
⊢ False

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

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u✝ ⋯).length
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
⊢ (cons h✝ p).bypass = cons h✝ p

Tactic:
simp only [Walk.bypass]

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
⊢ (if hs : u✝ ∈ p.bypass.support then p.bypass.dropUntil u✝ hs else cons h✝ p.bypass) = cons h✝ p

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u✝ ⋯).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 _

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
⊢ (if hs : u✝ ∈ p.bypass.support then p.bypass.dropUntil u✝ hs else cons h✝ p.bypass) = cons h✝ p

Tactic:
split_ifs with hb

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∈ p.bypass.support
⊢ p.bypass.dropUntil u✝ hb = cons h✝ p

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∉ p.bypass.support
⊢ cons h✝ p.bypass = cons h✝ p

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ : V
h : nil.length ≤ nil.bypass.length
⊢ nil.bypass = nil

Tactic:
rfl

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∉ p.bypass.support
h : p.length ≤ p.bypass.length
⊢ cons h✝ p.bypass = cons h✝ p

Tactic:
rw [ih h]

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∈ p.bypass.support
⊢ p.bypass.dropUntil u✝ hb = cons h✝ p

Tactic:
exfalso

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∈ p.bypass.support
⊢ False

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
h : (cons h✝ p).length ≤ (cons h✝ p).bypass.length
hb : u✝ ∉ p.bypass.support
⊢ cons h✝ p.bypass = cons h✝ p

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

Result:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.length ≤ p.bypass.length → p.bypass = p
hb : u✝ ∉ p.bypass.support
h : p.length ≤ p.bypass.length
⊢ cons h✝ p.bypass = cons h✝ p