Theorem: SimpleGraph.push_eq_nil' (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
hp : ∀ z ∈ Walk.support p, f z = w
⊢ Walk.copy (push_Walk f p) (_ : f a = w) (_ : f b = w) = Walk.nil
Tactic:
induction p with
| nil => simp at hp ; subst hp ; rfl
| cons h p ih =>
  simp at hp ; obtain ⟨h1, hp⟩ := hp
  subst_vars
  simpa [push_Walk, hp _ (Walk.start_mem_support _)] using ih hp
State after:
no goals

State before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil
Tactic:
simp at hp
State after:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp✝ : ∀ z ∈ Walk.support Walk.nil, f z = w
hp : f u✝ = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil

State before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
w : V'
u✝ : V
hp✝ : ∀ z ∈ Walk.support Walk.nil, f z = w
hp : f u✝ = w
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = w) (_ : f u✝ = w) = Walk.nil
Tactic:
subst hp
State after:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = f u✝
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = f u✝) (_ : f u✝ = f u✝) = Walk.nil

State before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
hp : ∀ z ∈ Walk.support Walk.nil, f z = f u✝
⊢ Walk.copy (push_Walk f Walk.nil) (_ : f u✝ = f u✝) (_ : f u✝ = f u✝) = Walk.nil
Tactic:
rfl
State after:
no goals

State before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
simp at hp
State after:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
hp : f u✝ = w ∧ ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil

State before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
hp : f u✝ = w ∧ ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
obtain ⟨h1, hp⟩ := hp
State after:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
h1 : f u✝ = w
hp : ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil

State before:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
w : V'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = w), Walk.copy (push_Walk f p) (_ : f v✝ = w) (_ : f w✝ = w) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = w
h1 : f u✝ = w
hp : ∀ a ∈ Walk.support p, f a = w
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = w) (_ : f w✝ = w) = Walk.nil
Tactic:
subst_vars
State after:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = f u✝), Walk.copy (push_Walk f p) (_ : f v✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = f u✝
hp : ∀ a ∈ Walk.support p, f a = f u✝
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil

State before:
case cons.intro
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (hp : ∀ z ∈ Walk.support p, f z = f u✝), Walk.copy (push_Walk f p) (_ : f v✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
hp✝ : ∀ z ∈ Walk.support (Walk.cons h p), f z = f u✝
hp : ∀ a ∈ Walk.support p, f a = f u✝
⊢ Walk.copy (push_Walk f (Walk.cons h p)) (_ : f u✝ = f u✝) (_ : f w✝ = f u✝) = Walk.nil
Tactic:
simpa [push_Walk, hp _ (Walk.start_mem_support _)] using ih hp
State after:
no goals