-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem length_bypass_le {u v : V} (p : G.Walk u v) : p.bypass.length ≤ p.length

Proof state:
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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.length ≤ (cons h✝¹ p✝).length

Tactic:
rw [length_cons]

Result:
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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.length ≤ p✝.length + 1

Proof state:
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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.length ≤ p✝.length + 1

Tactic:
omega

Result:
no goals

Proof state:
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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).length ≤ ?m.94641

Tactic:
apply length_dropUntil_le

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).length ≤ (cons h✝¹ p✝).length

Tactic:
trans

Result:
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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).length ≤ ?m.94641

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ ?m.94641 ≤ (cons h✝¹ p✝).length

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ ℕ

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

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).length ≤ (cons h✝¹ p✝).length

Tactic:
rw [length_cons, length_cons]

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∉ p✝.bypass.support
⊢ p✝.bypass.length + 1 ≤ p✝.length + 1

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✝.bypass.length ≤ p✝.length
⊢ (cons h✝ p✝).bypass.length ≤ (cons h✝ p✝).length

Tactic:
simp only [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✝.bypass.length ≤ p✝.length
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).length ≤ (cons h✝ p✝).length

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∉ p✝.bypass.support
⊢ p✝.bypass.length + 1 ≤ p✝.length + 1

Tactic:
exact Nat.add_le_add_right ih 1

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✝.bypass.length ≤ p✝.length
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).length ≤ (cons h✝ p✝).length

Tactic:
split_ifs

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).length ≤ (cons h✝¹ p✝).length

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✝.bypass.length ≤ p✝.length
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).length ≤ (cons h✝¹ p✝).length