Theorem: Digraph.set_walk_length_succ_eq (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
n : ℕ
⊢ {p | Walk.length p = Nat.succ n} = ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
ext p
State after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
p : Walk G u v
⊢ p ∈ {p | Walk.length p = Nat.succ n} ↔ p ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}

State before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
p : Walk G u v
⊢ p ∈ {p | Walk.length p = Nat.succ n} ↔ p ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
cases' p with _ _ w _ huw pwv
State after:
case h.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
n : ℕ
⊢ Walk.nil ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.nil ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}

case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.cons huw pwv ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.cons huw pwv ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}

State before:
case h.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
n : ℕ
⊢ Walk.nil ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.nil ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
simp [eq_comm]
State after:
no goals

State before:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.cons huw pwv ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.cons huw pwv ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
simp only [Nat.succ_eq_add_one, Set.mem_setOf_eq, Walk.length_cons, add_left_inj,
  Set.mem_iUnion, Set.mem_image, exists_prop]
State after:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n ↔ ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv

State before:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n ↔ ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
constructor
State after:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n → ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv

case h.cons.mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ (∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv) → Walk.length pwv = n

State before:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n → ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
rintro rfl
State after:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ ∃ i h x, Walk.length x = Walk.length pwv ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv

State before:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ ∃ i h x, Walk.length x = Walk.length pwv ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
exact ⟨w, huw, pwv, rfl, rfl⟩
State after:
no goals

State before:
case h.cons.mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ (∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv) → Walk.length pwv = n
Tactic:
rintro ⟨w, huw, pwv, rfl, rfl, rfl⟩
State after:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw✝ : G.Adj u w
pwv : Walk G w v
huw : G.Adj u w
⊢ Walk.length pwv = Walk.length pwv

State before:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw✝ : G.Adj u w
pwv : Walk G w v
huw : G.Adj u w
⊢ Walk.length pwv = Walk.length pwv
Tactic:
rfl
State after:
no goals