internlm/Lean-Github huggingface dataset:
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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]
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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]
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction
Proof 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⟩
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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]
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof 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)}
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction'
Proof 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]
Proof 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
Theorem: Digraph.deleteEdges_induction'
Proof 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]
Proof 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)}
Theorem: Digraph.deleteEdges_induction'
Proof 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]
Proof 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
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof 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
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction'
Proof 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⟩)
Proof 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
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof state after:
no goals
Theorem: Digraph.deleteEdges_induction'
Proof 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
Proof state after:
no goals
Theorem: Digraph.strong_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
⊢ motive G
Tactic:
classical
have : Fintype V := Fintype.ofFinite V
generalize hs : G.edgeSet.toFinset = s
induction s using Finset.strongInduction generalizing G with
| _ s ih =>
  cases hs
  apply hind
  intros G' hG
  exact ih G'.edgeSet.toFinset (by simpa using hG) _ rfl
Proof state after:
no goals
Theorem: Digraph.strong_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
⊢ motive G
Tactic:
have : Fintype V := Fintype.ofFinite V
Proof state after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
this : Fintype V
⊢ motive G
Theorem: Digraph.strong_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
this : Fintype V
⊢ motive G
Tactic:
generalize hs : G.edgeSet.toFinset = s
Proof state after:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
this : Fintype V
s : Finset (V × V)
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
Theorem: Digraph.strong_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
this : Fintype V
s : Finset (V × V)
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
Tactic:
induction s using Finset.strongInduction generalizing G with
| _ s ih =>
  cases hs
  apply hind
  intros G' hG
  exact ih G'.edgeSet.toFinset (by simpa using hG) _ rfl
Proof state after:
no goals
Theorem: Digraph.strong_induction
Proof state before:
case H
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
s : Finset (V × V)
ih : ∀ (t : Finset (V × V)), t ⊂ s → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
Tactic:
cases hs
Proof state after:
case H.refl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
⊢ motive G
Theorem: Digraph.strong_induction
Proof state before:
case H.refl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
⊢ motive G
Tactic:
apply hind
Proof state after:
case H.refl.a
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
⊢ ∀ (G' : Digraph V), G' < G → motive G'
Theorem: Digraph.strong_induction
Proof state before:
case H.refl.a
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
⊢ ∀ (G' : Digraph V), G' < G → motive G'
Tactic:
intros G' hG
Proof state after:
case H.refl.a
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
G' : Digraph V
hG : G' < G
⊢ motive G'
Theorem: Digraph.strong_induction
Proof state before:
case H.refl.a
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
G' : Digraph V
hG : G' < G
⊢ motive G'
Tactic:
exact ih G'.edgeSet.toFinset (by simpa using hG) _ rfl
Proof state after:
no goals