Theorem: SimpleGraph.merge_edge_adapted (Untitled/Graphs/Contraction.lean)

State before:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
⊢ Adapted G (merge_edge e)
Tactic:
rintro x y hxy
State after:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x✝ y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
x y : V
hxy : merge_edge e x = merge_edge e y
⊢ ∃ p, ∀ z ∈ Walk.support p, merge_edge e z = merge_edge e y

State before:
V : Type u_1
V' : Type u_2
V'' : Type u_3
x✝ y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
x y : V
hxy : merge_edge e x = merge_edge e y
⊢ ∃ p, ∀ z ∈ Walk.support p, merge_edge e z = merge_edge e y
Tactic:
by_cases hx : x = e.snd <;> by_cases hy : y = e.snd <;>
  simp [merge_edge, Function.update, hx, hy] at hxy ⊢ <;> subst_vars
State after:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1

case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1

case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1

case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = y

State before:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
use Walk.nil
State after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∀ z ∈ Walk.support Walk.nil, ¬z = e.toProd.2 → z = e.toProd.1

State before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hxy : True
⊢ ∀ z ∈ Walk.support Walk.nil, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
simp
State after:
no goals

State before:
case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1
Tactic:
use Walk.nil.cons e.symm.is_adj
State after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G (Dart.symm e).toProd.1 (Dart.symm e).toProd.2) Walk.nil),
    (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1

State before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hy : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G (Dart.symm e).toProd.1 (Dart.symm e).toProd.2) Walk.nil),
    (if z = e.toProd.2 then e.toProd.1 else z) = e.toProd.1
Tactic:
simp
State after:
no goals

State before:
case pos
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
use Walk.nil.cons e.is_adj
State after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G e.toProd.1 e.toProd.2) Walk.nil), ¬z = e.toProd.2 → z = e.toProd.1

State before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
hx : ¬e.toProd.1 = e.toProd.2
⊢ ∀ z ∈ Walk.support (Walk.cons (_ : Adj G e.toProd.1 e.toProd.2) Walk.nil), ¬z = e.toProd.2 → z = e.toProd.1
Tactic:
simp
State after:
no goals

State before:
case neg
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∃ p, ∀ z ∈ Walk.support p, (if z = e.toProd.2 then e.toProd.1 else z) = y
Tactic:
use Walk.nil
State after:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∀ z ∈ Walk.support Walk.nil, (if z = e.toProd.2 then e.toProd.1 else z) = y

State before:
case h
V : Type u_1
V' : Type u_2
V'' : Type u_3
x y✝ z : V
x' y' z' : V'
f : V → V'
g : V' → V''
G H : SimpleGraph V
G' H' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
e : Dart G
y : V
hy hx : ¬y = e.toProd.2
⊢ ∀ z ∈ Walk.support Walk.nil, (if z = e.toProd.2 then e.toProd.1 else z) = y
Tactic:
simp [hy]
State after:
no goals