Theorem: Digraph.Walk.length_bypass_le (GraphProjects/DigraphConnectivity.lean)

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ : V
⊢ length (bypass nil) ≤ length nil
Tactic:
rfl
State after:
no goals

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
⊢ length (bypass (cons h✝ p✝)) ≤ length (cons h✝ p✝)
Tactic:
simp only [bypass]
State after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj 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✝)

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj 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✝)
Tactic:
split_ifs
State after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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 : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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✝)

State before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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✝)
Tactic:
trans
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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.249227

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

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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.249227

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

V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ ℕ
Tactic:
apply length_dropUntil_le
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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✝)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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✝)
Tactic:
rw [length_cons]
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : length (bypass p✝) ≤ length p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ length (bypass p✝) ≤ length p✝ + 1
Tactic:
exact le_add_right ih
State after:
no goals

State before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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✝)
Tactic:
rw [length_cons, length_cons]
State after:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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

State before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj 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
Tactic:
exact add_le_add_right ih 1
State after:
no goals