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

State before:
V : Type u_1
G G' : Digraph V
⊢ G < G' ↔ ∃ s, Set.Nonempty 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, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s

case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, Set.Nonempty 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, Set.Nonempty 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, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s

State before:
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ ∃ s, Set.Nonempty 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'
⊢ Set.Nonempty (edgeSet G' \ edgeSet 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'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G) ∧
    edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
constructor
State after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G)

case mp.right
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.right
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:
constructor
State after:
case mp.right.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G'

case mp.right.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)

State before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G)
Tactic:
by_contra hn
State after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False

State before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False
Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.diff_eq_empty, edgeSet_subset_edgeSet] at hn
State after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : G' ≤ G
⊢ False

State before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : G' ≤ G
⊢ False
Tactic:
exact lt_irrefl _ (trans h hn)
State after:
no goals

State before:
case mp.right.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G'
Tactic:
apply Set.diff_subset
State after:
no goals

State before:
case mp.right.right
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.right.right.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.right.right.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.right.right.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.right.right.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:
have : G.Adj v w → G'.Adj v w := fun e => h.le e
State after:
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
this : G.Adj v w → G'.Adj v w
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)

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

State before:
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G < G'
Tactic:
rintro ⟨s, ⟨⟨v, w⟩, h⟩, hs, rfl⟩
State after:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s < G'

State before:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s < G'
Tactic:
rw [lt_iff_le_and_ne]
State after:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G' ∧ deleteEdges G' s ≠ G'

State before:
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G' ∧ deleteEdges G' s ≠ G'
Tactic:
constructor
State after:
case mpr.intro.intro.intro.mk.intro.left
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'

case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≠ G'

State before:
case mpr.intro.intro.intro.mk.intro.left
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'
Tactic:
apply deleteEdges_le
State after:
no goals

State before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≠ G'
Tactic:
intro hd
State after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : deleteEdges G' s = G'
⊢ False

State before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
⊢ False
Tactic:
have := hs h
State after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : (v, w) ∈ edgeSet G'
⊢ False

State before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : (v, w) ∈ edgeSet G'
⊢ False
Tactic:
rw [mem_edgeSet] at this
State after:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : G'.Adj v w
⊢ False

State before:
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : G'.Adj v w
⊢ False
Tactic:
simp [this, h] at hd
State after:
no goals