no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ : V
⊢ length (bypass nil) ≤ length nil
rfl
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ≤
    length (cons h✝ p✝)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (bypass (cons h✝ p✝)) ≤ length (cons h✝ p✝)
simp only [bypass]
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ length (cons h✝¹ p✝)

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (cons h✝¹ (bypass p✝)) ≤ length (cons h✝¹ p✝)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ≤
    length (cons h✝ p✝)
split_ifs
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ ?m.279260

V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ?m.279260 ≤ length (cons h✝¹ p✝)

V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ length (cons h✝¹ p✝)
trans
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length (cons h✝¹ p✝)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (dropUntil (bypass p✝) u✝ h✝) ≤ ?m.279260

V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ?m.279260 ≤ length (cons h✝¹ p✝)

V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ
apply length_dropUntil_le
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length (cons h✝¹ p✝)
rw [length_cons]
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1
exact le_add_right ih
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) + 1 ≤ length p✝ + 1
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (cons h✝¹ (bypass p✝)) ≤ length (cons h✝¹ p✝)
rw [length_cons, length_cons]
no goals
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) + 1 ≤ length p✝ + 1
exact add_le_add_right ih 1