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

State before:
case hbot
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
⊢ motive ⊥
Tactic:
exact hbot
State after:
no goals

State before:
case hdelete
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
⊢ motive G
Tactic:
convert hdelete (G.deleteEdges {(v, w)}) v w (by simp) ih
State after:
case h.e'_1
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
⊢ G = deleteEdges G {(v, w)} ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)}

State before:
case h.e'_1
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
⊢ G = deleteEdges G {(v, w)} ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)}
Tactic:
ext a b
State after:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ (deleteEdges G {(v, w)} ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)}).Adj a b

State before:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ (deleteEdges G {(v, w)} ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)}).Adj a b
Tactic:
simp only [Set.le_eq_subset, ge_iff_le, sup_adj, deleteEdges_adj, Set.mem_singleton_iff, Prod.mk.injEq, not_and]
State after:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (↑(OrderIso.symm (edgeSetIso V)) {(v, w)}).Adj a b

State before:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (↑(OrderIso.symm (edgeSetIso V)) {(v, w)}).Adj a b
Tactic:
rw [edgeSetIso_symm_adj]
State after:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (a, b) ∈ {(v, w)}

State before:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (a, b) ∈ {(v, w)}
Tactic:
simp only [Set.mem_singleton_iff, Prod.mk.injEq]
State after:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w

State before:
case h.e'_1.Adj.h.h.a
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w
Tactic:
constructor
State after:
case h.e'_1.Adj.h.h.a.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b → G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w

case h.e'_1.Adj.h.h.a.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w → G.Adj a b

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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
⊢ ¬(deleteEdges G {(v, w)}).Adj v w
Tactic:
simp
State after:
no goals

State before:
case h.e'_1.Adj.h.h.a.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b → G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w
Tactic:
tauto
State after:
no goals

State before:
case h.e'_1.Adj.h.h.a.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
⊢ G.Adj a b ∧ (a = v → ¬b = w) ∨ a = v ∧ b = w → G.Adj a b
Tactic:
rintro (h | ⟨rfl, rfl⟩)
State after:
case h.e'_1.Adj.h.h.a.mpr.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
h : G.Adj a b ∧ (a = v → ¬b = w)
⊢ G.Adj a b

case h.e'_1.Adj.h.h.a.mpr.inr.intro
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
a b : V
hvw : G.Adj a b
ih : motive (deleteEdges G {(a, b)})
⊢ G.Adj a b

State before:
case h.e'_1.Adj.h.h.a.mpr.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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
a b : V
h : G.Adj a b ∧ (a = v → ¬b = w)
⊢ G.Adj a b
Tactic:
exact h.1
State after:
no goals

State before:
case h.e'_1.Adj.h.h.a.mpr.inr.intro
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 G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
a b : V
hvw : G.Adj a b
ih : motive (deleteEdges G {(a, b)})
⊢ G.Adj a b
Tactic:
assumption
State after:
no goals