Theorem: Digraph.Walk.IsCycle.transfer (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
q : Walk G u u
qc : IsCycle q
hq : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer q H hq)
Tactic:
cases q with
| nil => simp at qc
| cons _ q =>
  simp only [edges_cons, List.find?, List.mem_cons, forall_eq_or_imp, mem_edgeSet] at hq
  simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
  exact ⟨qc.1.transfer hq.2, qc.2⟩
State after:
no goals

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
qc : IsCycle nil
hq : ∀ (e : V × V), e ∈ edges nil → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer nil H hq)
Tactic:
simp at qc
State after:
no goals

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
v✝ : V
h✝ : G.Adj u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq : ∀ (e : V × V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq)
Tactic:
simp only [edges_cons, List.find?, List.mem_cons, forall_eq_or_imp, mem_edgeSet] at hq
State after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
v✝ : V
h✝ : G.Adj u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq✝ : ∀ (e : V × V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : H.Adj u v✝ ∧ ∀ (a : V × V), a ∈ edges q → a ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq✝)

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
v✝ : V
h✝ : G.Adj u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq✝ : ∀ (e : V × V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : H.Adj u v✝ ∧ ∀ (a : V × V), a ∈ edges q → a ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq✝)
Tactic:
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
State after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
v✝ : V
h✝ : G.Adj u v✝
q : Walk G v✝ u
hq✝ : ∀ (e : V × V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : H.Adj u v✝ ∧ ∀ (a : V × V), a ∈ edges q → a ∈ edgeSet H
qc : IsPath q ∧ ¬(u, v✝) ∈ edges q
⊢ IsPath (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H)) ∧ ¬(u, v✝) ∈ edges q

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
H : Digraph V
v✝ : V
h✝ : G.Adj u v✝
q : Walk G v✝ u
hq✝ : ∀ (e : V × V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : H.Adj u v✝ ∧ ∀ (a : V × V), a ∈ edges q → a ∈ edgeSet H
qc : IsPath q ∧ ¬(u, v✝) ∈ edges q
⊢ IsPath (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H)) ∧ ¬(u, v✝) ∈ edges q
Tactic:
exact ⟨qc.1.transfer hq.2, qc.2⟩
State after:
no goals