internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case nil.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝ u' v' : V
p : Walk G u✝¹ v✝
f : G →g G'
hinj : Injective ↑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case nil.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ u✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝
Tactic:
simp at h
Proof state after:
no goals
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
p' : Walk G u✝ w✝
h : Walk.map f (cons h✝ p✝) = Walk.map f p'
⊢ cons h✝ p✝ = p'
Tactic:
cases p' with
| nil => simp at h
| cons _ _ =>
  simp only [map_cons, cons.injEq] at h
  cases hinj h.1
  simp only [cons.injEq, heq_iff_eq, true_and_iff]
  apply ih
  simpa using h.2
Proof state after:
no goals
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ u✝
ih : ∀ ⦃p' : Walk G v✝ u✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
h : Walk.map f (cons h✝ p✝) = Walk.map f nil
⊢ cons h✝ p✝ = nil
Tactic:
simp at h
Proof state after:
no goals
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝² u' v' : V
p : Walk G u✝¹ v✝²
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ ⦃p' : Walk G v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : Walk.map f (cons h✝¹ p✝¹) = Walk.map f (cons h✝ p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Tactic:
simp only [map_cons, cons.injEq] at h
Proof state after:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝² u' v' : V
p : Walk G u✝¹ v✝²
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ ⦃p' : Walk G v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝¹ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝² u' v' : V
p : Walk G u✝¹ v✝²
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : Walk G v✝¹ w✝
ih : ∀ ⦃p' : Walk G v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝¹ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Tactic:
cases hinj h.1
Proof state after:
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
Tactic:
simp only [cons.injEq, heq_iff_eq, true_and_iff]
Proof state after:
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ p✝¹ = p✝
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ p✝¹ = p✝
Tactic:
apply ih
Proof state after:
case cons.cons.refl.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ Walk.map f p✝¹ = Walk.map f p✝
Theorem: Digraph.Walk.map_injective_of_injective
Proof state before:
case cons.cons.refl.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ Walk.map f p✝¹ = Walk.map f p✝
Tactic:
simpa using h.2
Proof state after:
no goals
Theorem: Digraph.Path.map_injective
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
⊢ Injective (Path.map f hinj)
Tactic:
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h
Proof state after:
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Path.map f hinj { val := p, property := hp } = Path.map f hinj { val := p', property := hp' }
⊢ { val := p, property := hp } = { val := p', property := hp' }
Theorem: Digraph.Path.map_injective
Proof state before:
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Path.map f hinj { val := p, property := hp } = Path.map f hinj { val := p', property := hp' }
⊢ { val := p, property := hp } = { val := p', property := hp' }
Tactic:
simp only [Path.map, Subtype.coe_mk, Subtype.mk.injEq] at h
Proof state after:
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Walk.map f p = Walk.map f p'
⊢ { val := p, property := hp } = { val := p', property := hp' }
Theorem: Digraph.Path.map_injective
Proof state before:
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Walk.map f p = Walk.map f p'
⊢ { val := p, property := hp } = { val := p', property := hp' }
Tactic:
simp [Walk.map_injective_of_injective hinj u v h]
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_self
Proof 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
⊢ Walk.transfer p G (_ : ∀ ⦃e : V × V⦄, e ∈ edges p → e ∈ edgeSet G) = p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_eq_map_of_le
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
GH : G ≤ H
⊢ Walk.transfer p H hp = Walk.map (Hom.mapSpanningSubgraphs GH) p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.edges_transfer
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
⊢ edges (Walk.transfer p H hp) = edges p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.support_transfer
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
⊢ support (Walk.transfer p H hp) = support p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.length_transfer
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
⊢ length (Walk.transfer p H hp) = length p
Tactic:
induction p <;> simp [*]
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.transfer
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
pp : IsPath p
⊢ IsPath (Walk.transfer p H hp)
Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  simp only [Walk.transfer, cons_isPath_iff, support_transfer _ ] at pp ⊢
  exact ⟨ih _ pp.1, pp.2⟩
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.transfer
Proof 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
u✝ : V
hp : ∀ (e : V × V), e ∈ edges Walk.nil → e ∈ edgeSet H
pp : IsPath Walk.nil
⊢ IsPath (Walk.transfer Walk.nil H hp)
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.IsPath.transfer
Proof 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
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H), IsPath p✝ → IsPath (Walk.transfer p✝ H hp)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
pp : IsPath (cons h✝ p✝)
⊢ IsPath (Walk.transfer (cons h✝ p✝) H hp)
Tactic:
simp only [Walk.transfer, cons_isPath_iff, support_transfer _ ] at pp ⊢
Proof 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
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H), IsPath p✝ → IsPath (Walk.transfer p✝ H hp)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
pp : IsPath p✝ ∧ ¬u✝ ∈ support p✝
⊢ IsPath (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) ∧ ¬u✝ ∈ support p✝
Theorem: Digraph.Walk.IsPath.transfer
Proof 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
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H), IsPath p✝ → IsPath (Walk.transfer p✝ H hp)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
pp : IsPath p✝ ∧ ¬u✝ ∈ support p✝
⊢ IsPath (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) ∧ ¬u✝ ∈ support p✝
Tactic:
exact ⟨ih _ pp.1, pp.2⟩
Proof state after:
no goals
Theorem: Digraph.Walk.IsCycle.transfer
Proof 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⟩
Proof state after:
no goals
Theorem: Digraph.Walk.IsCycle.transfer
Proof 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
Proof state after:
no goals
Theorem: Digraph.Walk.IsCycle.transfer
Proof 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
Proof 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✝)
Theorem: Digraph.Walk.IsCycle.transfer
Proof 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 ⊢
Proof 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
Theorem: Digraph.Walk.IsCycle.transfer
Proof 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⟩
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_transfer
Proof 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
hp : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H
K : Digraph V
hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer p H hp) → e ∈ edgeSet K
⊢ Walk.transfer (Walk.transfer p H hp) K hp' = Walk.transfer p K (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet K)
Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  simp only [Walk.transfer, cons.injEq, heq_eq_eq, true_and]
  apply ih
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_transfer
Proof 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 K : Digraph V
u✝ : V
hp : ∀ (e : V × V), e ∈ edges nil → e ∈ edgeSet H
hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer nil H hp) → e ∈ edgeSet K
⊢ Walk.transfer (Walk.transfer nil H hp) K hp' = Walk.transfer nil K (_ : ∀ (e : V × V), e ∈ edges nil → e ∈ edgeSet K)
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_transfer
Proof 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 K : Digraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih :
  ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)
    (hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer p✝ H hp) → e ∈ edgeSet K),
    Walk.transfer (Walk.transfer p✝ H hp) K hp' = Walk.transfer p✝ K (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet K)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer (cons h✝ p✝) H hp) → e ∈ edgeSet K
⊢ Walk.transfer (Walk.transfer (cons h✝ p✝) H hp) K hp' =
    Walk.transfer (cons h✝ p✝) K (_ : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet K)
Tactic:
simp only [Walk.transfer, cons.injEq, heq_eq_eq, true_and]
Proof 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 K : Digraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih :
  ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)
    (hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer p✝ H hp) → e ∈ edgeSet K),
    Walk.transfer (Walk.transfer p✝ H hp) K hp' = Walk.transfer p✝ K (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet K)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer (cons h✝ p✝) H hp) → e ∈ edgeSet K
⊢ Walk.transfer (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) K
      (_ :
        ∀ (e : V × V),
          e ∈ edges (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) → e ∈ edgeSet K) =
    Walk.transfer p✝ K (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet K)
Theorem: Digraph.Walk.transfer_transfer
Proof 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 K : Digraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih :
  ∀ (hp : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)
    (hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer p✝ H hp) → e ∈ edgeSet K),
    Walk.transfer (Walk.transfer p✝ H hp) K hp' = Walk.transfer p✝ K (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet K)
hp : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
hp' : ∀ (e : V × V), e ∈ edges (Walk.transfer (cons h✝ p✝) H hp) → e ∈ edgeSet K
⊢ Walk.transfer (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) K
      (_ :
        ∀ (e : V × V),
          e ∈ edges (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H)) → e ∈ edgeSet K) =
    Walk.transfer p✝ K (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet K)
Tactic:
apply ih
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_append
Proof 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
w : V
H : Digraph V
q : Walk G v w
hpq : ∀ (e : V × V), e ∈ edges (append p q) → e ∈ edgeSet H
e : V × V
he : e ∈ edges p
⊢ e ∈ edges (append p q)
Tactic:
simp [he]
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_append
Proof 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
w : V
H : Digraph V
q : Walk G v w
hpq : ∀ (e : V × V), e ∈ edges (append p q) → e ∈ edgeSet H
e : V × V
he : e ∈ edges q
⊢ e ∈ edges (append p q)
Tactic:
simp [he]
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_append
Proof 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
w : V
H : Digraph V
q : Walk G v w
hpq : ∀ (e : V × V), e ∈ edges (append p q) → e ∈ edgeSet H
⊢ Walk.transfer (append p q) H hpq =
    append (Walk.transfer p H (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet H))
      (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H))
Tactic:
induction p with
| nil => simp
| cons _ _ ih => simp only [Walk.transfer, cons_append, cons.injEq, heq_eq_eq, true_and, ih]
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_append
Proof 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
w : V
H : Digraph V
u✝ : V
q : Walk G u✝ w
hpq : ∀ (e : V × V), e ∈ edges (append nil q) → e ∈ edgeSet H
⊢ Walk.transfer (append nil q) H hpq =
    append (Walk.transfer nil H (_ : ∀ (e : V × V), e ∈ edges nil → e ∈ edgeSet H))
      (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H))
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.transfer_append
Proof 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
w : V
H : Digraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih :
  ∀ (q : Walk G w✝ w) (hpq : ∀ (e : V × V), e ∈ edges (append p✝ q) → e ∈ edgeSet H),
    Walk.transfer (append p✝ q) H hpq =
      append (Walk.transfer p✝ H (_ : ∀ (e : V × V), e ∈ edges p✝ → e ∈ edgeSet H))
        (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H))
q : Walk G w✝ w
hpq : ∀ (e : V × V), e ∈ edges (append (cons h✝ p✝) q) → e ∈ edgeSet H
⊢ Walk.transfer (append (cons h✝ p✝) q) H hpq =
    append (Walk.transfer (cons h✝ p✝) H (_ : ∀ (e : V × V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H))
      (Walk.transfer q H (_ : ∀ (e : V × V), e ∈ edges q → e ∈ edgeSet H))
Tactic:
simp only [Walk.transfer, cons_append, cons.injEq, heq_eq_eq, true_and, ih]
Proof state after:
no goals
Theorem: Digraph.Walk.map_toDeleteEdges_eq
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ Walk.map (Hom.mapSpanningSubgraphs (_ : deleteEdges G s ≤ G)) (toDeleteEdges s p hp) = p
Tactic:
rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]
Proof state after:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ ∀ (e : V × V),
    e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
      e ∈ edgeSet G

case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ ∀ (e : V × V),
    e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
      e ∈ edgeSet G
Theorem: Digraph.Walk.map_toDeleteEdges_eq
Proof state before:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ ∀ (e : V × V),
    e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
      e ∈ edgeSet G
Tactic:
intros e
Proof state after:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
e : V × V
⊢ e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
    e ∈ edgeSet G