Theorem: Digraph.le_iff_eq_deleteEdges (GraphProjects/DigraphExtra.lean)

State before:
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' ↔ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
constructor
State after:
case mp
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' → ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s

case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'

State before:
case mp
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' → ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
intro h
State after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s

State before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
use G'.edgeSet \ G.edgeSet
State after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)

State before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
refine ⟨Set.diff_subset _ _, ?_⟩
State after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)

State before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
ext v w
State after:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w

State before:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w
Tactic:
simp only [deleteEdges_adj, Set.mem_diff, mem_edgeSet, not_and, not_not]
State after:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)

State before:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Tactic:
constructor <;> simp (config := {contextual := true}) [@h v w]
State after:
no goals

State before:
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'
Tactic:
rintro ⟨s, _, rfl⟩
State after:
case mpr.intro.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
left✝ : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'

State before:
case mpr.intro.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
left✝ : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'
Tactic:
apply deleteEdges_le
State after:
no goals