Theorem: SimpleGraph.push_append (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
q : Walk G b c
⊢ push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
Tactic:
induction p with
| nil => rfl
| cons h p ih =>
  rename_i u v w
  by_cases huv : f u = f v <;> simp [push_Walk, huv, ih q]
  rw [← Walk.append_copy_copy]
  congr
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
u✝ : V
q : Walk G u✝ c
⊢ push_Walk f (Walk.append Walk.nil q) = Walk.append (push_Walk f Walk.nil) (push_Walk f q)
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
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w✝ c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)
Tactic:
rename_i u v w
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
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)

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
u v w : V
h : Adj G u v
p : Walk G v w
ih : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
⊢ push_Walk f (Walk.append (Walk.cons h p) q) = Walk.append (push_Walk f (Walk.cons h p)) (push_Walk f q)
Tactic:
by_cases huv : f u = f v <;> simp [push_Walk, huv, ih q]
State after:
case pos
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.copy (Walk.append (push_Walk f p) (push_Walk f q)) (_ : f v = f u) (_ : f c = f c) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)

State before:
case pos
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.copy (Walk.append (push_Walk f p) (push_Walk f q)) (_ : f v = f u) (_ : f c = f c) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)
Tactic:
rw [← Walk.append_copy_copy]
State after:
case pos
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) ?pos.hv✝)
      (Walk.copy (push_Walk f q) ?pos.hv✝ (_ : f c = f c)) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)

case pos.hv
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ f w = ?m.63832

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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ V'

State before:
case pos
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) ?pos.hv✝)
      (Walk.copy (push_Walk f q) ?pos.hv✝ (_ : f c = f c)) =
    Walk.append (Walk.copy (push_Walk f p) (_ : f v = f u) (_ : f w = f w)) (push_Walk f q)

case pos.hv
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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ f w = ?m.63832

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 : ∀ (q : Walk G w c), push_Walk f (Walk.append p q) = Walk.append (push_Walk f p) (push_Walk f q)
q : Walk G w c
huv : f u = f v
⊢ V'
Tactic:
congr
State after:
no goals