Theorem: Digraph.deleteEdges_sdiff_eq_of_le (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
H : Digraph V
h : H ≤ G
⊢ deleteEdges G (edgeSet G \ edgeSet H) = H
Tactic:
ext (v w)
State after:
case Adj.h.h.a
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
H : Digraph V
h : H ≤ G
v w : V
⊢ (deleteEdges G (edgeSet G \ edgeSet H)).Adj v w ↔ H.Adj v w

State before:
case Adj.h.h.a
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
H : Digraph V
h : H ≤ G
v w : V
⊢ (deleteEdges G (edgeSet G \ edgeSet H)).Adj v w ↔ H.Adj v w
Tactic:
constructor <;> simp (config := { contextual := true }) [@h v w]
State after:
no goals