Theorem: Graph.SpanningSubtree.surroundEdge_cast (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v u' v' : V
huu' : u = u'
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u' v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
cases huu'
State after:
case refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v' : V
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'

State before:
case refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v' : V
hvv' : v = v'
e : EdgeBetween G u v
e' : EdgeBetween G u v'
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
cases hvv'
State after:
case refl.refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'

State before:
case refl.refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
Tactic:
congr
State after:
case refl.refl.e_e
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e = e'

State before:
case refl.refl.e_e
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e = e'
Tactic:
ext
State after:
case refl.refl.e_e.edge
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e.edge = e'.edge

State before:
case refl.refl.e_e.edge
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e.edge = e'.edge
Tactic:
exact hee'
State after:
no goals