no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
q : Walk G u u
qc : IsCycle q
hq : ∀ (e : Sym2 V), e ∈ edges q → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer q H hq)
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⟩
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
qc : IsCycle nil
hq : ∀ (e : Sym2 V), e ∈ edges nil → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer nil H hq)
simp at qc
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
v✝ : V
h✝ : Adj G u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq✝ : ∀ (e : Sym2 V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : Adj H u v✝ ∧ ∀ (a : Sym2 V), a ∈ edges q → a ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq✝)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
v✝ : V
h✝ : Adj G u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq : ∀ (e : Sym2 V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq)
simp only [edges_cons, List.find?, List.mem_cons, forall_eq_or_imp, mem_edgeSet] at hq
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
v✝ : V
h✝ : Adj G u v✝
q : Walk G v✝ u
hq✝ : ∀ (e : Sym2 V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : Adj H u v✝ ∧ ∀ (a : Sym2 V), a ∈ edges q → a ∈ edgeSet H
qc : IsPath q ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v✝) ∈ edges q
⊢ IsPath (Walk.transfer q H (_ : ∀ (e : Sym2 V), e ∈ edges q → e ∈ edgeSet H)) ∧
    ¬Quotient.mk (Sym2.Rel.setoid V) (u, v✝) ∈ edges q
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
v✝ : V
h✝ : Adj G u v✝
q : Walk G v✝ u
qc : IsCycle (cons h✝ q)
hq✝ : ∀ (e : Sym2 V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : Adj H u v✝ ∧ ∀ (a : Sym2 V), a ∈ edges q → a ∈ edgeSet H
⊢ IsCycle (Walk.transfer (cons h✝ q) H hq✝)
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
H : SimpleGraph V
v✝ : V
h✝ : Adj G u v✝
q : Walk G v✝ u
hq✝ : ∀ (e : Sym2 V), e ∈ edges (cons h✝ q) → e ∈ edgeSet H
hq : Adj H u v✝ ∧ ∀ (a : Sym2 V), a ∈ edges q → a ∈ edgeSet H
qc : IsPath q ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v✝) ∈ edges q
⊢ IsPath (Walk.transfer q H (_ : ∀ (e : Sym2 V), e ∈ edges q → e ∈ edgeSet H)) ∧
    ¬Quotient.mk (Sym2.Rel.setoid V) (u, v✝) ∈ edges q
exact ⟨qc.1.transfer hq.2, qc.2⟩