Theorem: Digraph.reachable_iff_reflTransGen (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v ↔ Relation.ReflTransGen G.Adj u v
Tactic:
constructor
State after:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v

case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v

State before:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v
Tactic:
rintro ⟨h⟩
State after:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v

State before:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v
Tactic:
induction h with
| nil => rfl
| cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
State after:
no goals

State before:
case mp.intro.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝
Tactic:
rfl
State after:
no goals

State before:
case mp.intro.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : Relation.ReflTransGen G.Adj v✝ w✝
⊢ Relation.ReflTransGen G.Adj u✝ w✝
Tactic:
exact (Relation.ReflTransGen.single h').trans ih
State after:
no goals

State before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v
Tactic:
intro h
State after:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v

State before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v
Tactic:
induction h with
| refl => rfl
| tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
State after:
no goals

State before:
case mpr.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u u
Tactic:
rfl
State after:
no goals

State before:
case mpr.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v b✝ c✝ : V
a✝ : Relation.ReflTransGen G.Adj u b✝
ha : G.Adj b✝ c✝
hr : Reachable G u b✝
⊢ Reachable G u c✝
Tactic:
exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
State after:
no goals