-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_coe_eq (s : Set (Sym2 G'.verts)) :
    G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map (↑) '' s)).coe

Proof state:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
⊢ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Tactic:
refine Sym2.ind ?_

Result:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
⊢ ∀ (x y : ↑G'.verts), s(x, y) ∈ s → ¬Sym2.map Subtype.val s(x, y) = s(v, w)

Proof state:
case Adj.h.mk.h.mk.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∈ s
⊢ False

Tactic:
exact h' _ hs rfl

Result:
no goals

Proof state:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Tactic:
constructor

Result:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s → ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

case Adj.h.mk.h.mk.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Proof state:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ (G'.coe.deleteEdges s).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simp only [SimpleGraph.deleteEdges_adj, coe_adj, deleteEdges_adj, Set.mem_image, not_exists,
  not_and, and_congr_right_iff]

Result:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ G'.Adj v w → (s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w))

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Result:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ (G'.coe.deleteEdges s).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s → ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Tactic:
intro hs

Result:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
⊢ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Proof state:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(⟨v', hv'⟩, ⟨w', hw'⟩) ∈ s → ¬Sym2.Rel V (v', w') (v, w)

Tactic:
contrapose!

Result:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Sym2.Rel V (v', w') (v, w) → s(⟨v', hv'⟩, ⟨w', hw'⟩) ∉ s

Proof state:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ G'.Adj v w → (s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w))

Tactic:
intro

Result:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Proof state:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(⟨v', hv'⟩, ⟨w', hw'⟩) ∈ s → ¬Sym2.map Subtype.val s(⟨v', hv'⟩, ⟨w', hw'⟩) = s(v, w)

Tactic:
simp only [Sym2.map_pair_eq, Sym2.eq]

Result:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(⟨v', hv'⟩, ⟨w', hw'⟩) ∈ s → ¬Sym2.Rel V (v', w') (v, w)

Proof state:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Sym2.Rel V (v', w') (v, w) → s(⟨v', hv'⟩, ⟨w', hw'⟩) ∉ s

Tactic:
rintro (_ | _) <;> simpa only [Sym2.eq_swap]

Result:
no goals

Proof state:
case Adj.h.mk.h.mk.a.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
⊢ ∀ (x y : ↑G'.verts), s(x, y) ∈ s → ¬Sym2.map Subtype.val s(x, y) = s(v, w)

Tactic:
rintro ⟨v', hv'⟩ ⟨w', hw'⟩

Result:
case Adj.h.mk.h.mk.a.mp.mk.mk
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(⟨v', hv'⟩, ⟨w', hw'⟩) ∈ s → ¬Sym2.map Subtype.val s(⟨v', hv'⟩, ⟨w', hw'⟩) = s(v, w)

Proof state:
case Adj.h.mk.h.mk.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
intro h' hs

Result:
case Adj.h.mk.h.mk.a.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∈ s
⊢ False