case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ Reachable G u v → ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)

case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)) → Reachable G u v
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ Reachable G u v ↔ ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
constructor
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
⊢ ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ Reachable G u v → ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
intro r
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
p : Path G u v
⊢ ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
⊢ ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
refine r.elim_path fun p => ?_
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
p : Path G u v
⊢ ↑p ∈ finsetWalkLength G (↑{ val := Walk.length ↑p, isLt := (_ : Walk.length ↑p < Fintype.card V) }) u v
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
p : Path G u v
⊢ ∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)
refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
no goals
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : Reachable G u v
p : Path G u v
⊢ ↑p ∈ finsetWalkLength G (↑{ val := Walk.length ↑p, isLt := (_ : Walk.length ↑p < Fintype.card V) }) u v
simp [Walk.mem_finsetWalkLength_iff_length_eq]
case mpr.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
w✝ : Fin (Fintype.card V)
p : Walk G u v
h✝ : p ∈ finsetWalkLength G (↑w✝) u v
⊢ Reachable G u v
case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, Finset.Nonempty (finsetWalkLength G (↑n) u v)) → Reachable G u v
rintro ⟨_, p, _⟩
no goals
case mpr.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
w✝ : Fin (Fintype.card V)
p : Walk G u v
h✝ : p ∈ finsetWalkLength G (↑w✝) u v
⊢ Reachable G u v
exact ⟨p⟩