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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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'

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
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'

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
State after:
no goals

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
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
⊢ Set.toFinset (edgeSet G') ⊂ Set.toFinset (edgeSet G)
Tactic:
simpa using hG
State after:
no goals