Theorem: Digraph.deleteEdges_induction (GraphProjects/DigraphInduction.lean)

State before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
⊢ motive G
Tactic:
have : Fintype V := Fintype.ofFinite V
State after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
⊢ motive G

State before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
⊢ motive G
Tactic:
generalize hs : G.edgeSet.toFinset = s
State after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
G : Digraph V
this : Fintype V
s : Finset (V × V)
hs : Set.toFinset (edgeSet G) = s
⊢ motive G

State before:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs : Set.toFinset (edgeSet G) = ∅
⊢ motive G
Tactic:
rw [← Set.toFinset_empty, Set.toFinset_inj, ← edgeSet_bot, edgeSet_inj] at hs
State after:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs✝ : Set.toFinset (edgeSet G) = ∅
hs : G = ⊥
⊢ motive G

State before:
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs✝ : Set.toFinset (edgeSet G) = ∅
hs : G = ⊥
⊢ motive G
Tactic:
rwa [hs]
State after:
no goals

State before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ motive G
Tactic:
have : e ∈ G.edgeSet
State after:
case this
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ e ∈ edgeSet G

case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive G

State before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive G
Tactic:
apply hdelete G e.1 e.2 this
State after:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive (deleteEdges G {(e.fst, e.snd)})

State before:
case insert
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ motive (deleteEdges G {(e.fst, e.snd)})
Tactic:
apply ih
State after:
case insert.hs
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) = s

State before:
case insert.hs
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
⊢ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) = s
Tactic:
ext ⟨v, w⟩
State after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ (v, w) ∈ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) ↔ (v, w) ∈ s

State before:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ (v, w) ∈ Set.toFinset (edgeSet (deleteEdges G {(e.fst, e.snd)})) ↔ (v, w) ∈ s
Tactic:
simp only [Prod.mk.eta, Set.mem_toFinset, mem_edgeSet, deleteEdges_adj, Set.mem_singleton_iff]
State after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
this : e ∈ edgeSet G
v w : V
⊢ G.Adj v w ∧ ¬(v, w) = e ↔ (v, w) ∈ s

State before:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : ((v, w) ∈ Set.toFinset (edgeSet G)) = ((v, w) ∈ insert e s)
⊢ G.Adj v w ∧ ¬(v, w) = e ↔ (v, w) ∈ s
Tactic:
simp only [Set.mem_toFinset, mem_edgeSet, Finset.mem_insert, eq_iff_iff] at hs
State after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ G.Adj v w ∧ ¬(v, w) = e ↔ (v, w) ∈ s

State before:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ G.Adj v w ∧ ¬(v, w) = e ↔ (v, w) ∈ s
Tactic:
rw [hs]
State after:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e ↔ (v, w) ∈ s

State before:
case insert.hs.a.mk
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e ↔ (v, w) ∈ s
Tactic:
constructor
State after:
case insert.hs.a.mk.mp
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e → (v, w) ∈ s

case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ (v, w) ∈ s → ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e

State before:
case this
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ e ∈ edgeSet G
Tactic:
rw [← Set.mem_toFinset, hs]
State after:
case this
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ e ∈ insert e s

State before:
case this
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = insert e s
⊢ e ∈ insert e s
Tactic:
exact Finset.mem_insert_self e s
State after:
no goals

State before:
case insert.hs.a.mk.mp
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e → (v, w) ∈ s
Tactic:
rintro ⟨(rfl | ha), hne⟩
State after:
case insert.hs.a.mk.mp.intro.inl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
s : Finset (V × V)
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
v w : V
he : ¬(v, w) ∈ s
this : (v, w) ∈ edgeSet G
hs : G.Adj v w ↔ (v, w) = (v, w) ∨ (v, w) ∈ s
hne : ¬(v, w) = (v, w)
⊢ (v, w) ∈ s

case insert.hs.a.mk.mp.intro.inr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
hne : ¬(v, w) = e
ha : (v, w) ∈ s
⊢ (v, w) ∈ s

State before:
case insert.hs.a.mk.mp.intro.inl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
s : Finset (V × V)
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
v w : V
he : ¬(v, w) ∈ s
this : (v, w) ∈ edgeSet G
hs : G.Adj v w ↔ (v, w) = (v, w) ∨ (v, w) ∈ s
hne : ¬(v, w) = (v, w)
⊢ (v, w) ∈ s
Tactic:
simp at hne
State after:
no goals

State before:
case insert.hs.a.mk.mp.intro.inr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
hne : ¬(v, w) = e
ha : (v, w) ∈ s
⊢ (v, w) ∈ s
Tactic:
assumption
State after:
no goals

State before:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ (v, w) ∈ s → ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e
Tactic:
intro h
State after:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
h : (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e

State before:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
h : (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e
Tactic:
simp only [h, or_true, true_and]
State after:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
h : (v, w) ∈ s
⊢ ¬(v, w) = e

State before:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
h : (v, w) ∈ s
⊢ ¬(v, w) = e
Tactic:
rintro rfl
State after:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
s : Finset (V × V)
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
v w : V
h : (v, w) ∈ s
he : ¬(v, w) ∈ s
this : (v, w) ∈ edgeSet G
hs : G.Adj v w ↔ (v, w) = (v, w) ∨ (v, w) ∈ s
⊢ False

State before:
case insert.hs.a.mk.mpr
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
s : Finset (V × V)
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
v w : V
h : (v, w) ∈ s
he : ¬(v, w) ∈ s
this : (v, w) ∈ edgeSet G
hs : G.Adj v w ↔ (v, w) = (v, w) ∨ (v, w) ∈ s
⊢ False
Tactic:
exact absurd h he
State after:
no goals