case mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
q : Path G v w
p : Walk G v w
hp : Walk.IsPath p
⊢ { val := p, property := hp } = q
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p q : Path G v w
⊢ p = q
obtain ⟨p, hp⟩ := p
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : Walk.IsPath p
q : Walk G v w
hq : Walk.IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
case mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
q : Path G v w
p : Walk G v w
hp : Walk.IsPath p
⊢ { val := p, property := hp } = q
obtain ⟨q, hq⟩ := q
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : Walk.IsPath p
q : Walk G v w
hq : Walk.IsPath q
⊢ p = q
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : Walk.IsPath p
q : Walk G v w
hq : Walk.IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
rw [Subtype.mk.injEq]
case mk.mk.nil.refl
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp hq : Walk.IsPath Walk.nil
⊢ Walk.nil = Walk.nil
case mk.mk.nil
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp : Walk.IsPath Walk.nil
q : Walk G u✝ u✝
hq : Walk.IsPath q
⊢ Walk.nil = q
cases (Walk.isPath_iff_eq_nil _).mp hq
no goals
case mk.mk.nil.refl
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp hq : Walk.IsPath Walk.nil
⊢ Walk.nil = Walk.nil
rfl
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
⊢ Walk.cons ph p = q
rw [isAcyclic_iff_forall_adj_isBridge] at h
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝))
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
⊢ Walk.cons ph p = q
specialize h ph
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Adj G u✝ v✝ ∧ ∀ (p : Walk G u✝ v✝), Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝))
⊢ Walk.cons ph p = q
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges (Walk.append q (Walk.reverse p))
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Adj G u✝ v✝ ∧ ∀ (p : Walk G u✝ v✝), Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
replace h := h.2 (q.append p.reverse)
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges q ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges (Walk.append q (Walk.reverse p))
⊢ Walk.cons ph p = q
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse'] at h
case mk.mk.cons.inl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges q
⊢ Walk.cons ph p = q

case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges q ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
cases' h with h h
no goals
case mk.mk.cons.inl.nil
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ u✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ u✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
hq : Walk.IsPath Walk.nil
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges Walk.nil
⊢ Walk.cons ph p = Walk.nil
simp [Walk.isPath_def] at hp
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges (Walk.cons h✝ q)
⊢ Walk.cons ph p = Walk.cons h✝ q
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath (Walk.cons h✝ q)
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges (Walk.cons h✝ q)
⊢ Walk.cons ph p = Walk.cons h✝ q
rw [Walk.cons_isPath_iff] at hp hq
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges q
⊢ Walk.cons ph p = Walk.cons h✝ q
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges (Walk.cons h✝ q)
⊢ Walk.cons ph p = Walk.cons h✝ q
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
case mk.mk.cons.inl.cons.inl.inl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
⊢ Walk.cons ph p = Walk.cons h✝ q

case mk.mk.cons.inl.cons.inl.inr.intro
V : Type u
G✝ G : SimpleGraph V
v w v✝ w✝ : V
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
ph : Adj G v✝ v✝
hp : Walk.IsPath p ∧ ¬v✝ ∈ Walk.support p
h✝ : Adj G v✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬v✝ ∈ Walk.support q
⊢ Walk.cons ph p = Walk.cons h✝ q

case mk.mk.cons.inl.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges q
⊢ Walk.cons ph p = Walk.cons h✝ q
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges q
⊢ Walk.cons ph p = Walk.cons h✝ q
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
case mk.mk.cons.inl.cons.inl.inl.refl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
hq : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
⊢ Walk.cons ph p = Walk.cons h✝ p
case mk.mk.cons.inl.cons.inl.inl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
⊢ Walk.cons ph p = Walk.cons h✝ q
cases ih hp.1 q hq.1
no goals
case mk.mk.cons.inl.cons.inl.inl.refl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
hq : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
⊢ Walk.cons ph p = Walk.cons h✝ p
rfl
no goals
case mk.mk.cons.inl.cons.inl.inr.intro
V : Type u
G✝ G : SimpleGraph V
v w v✝ w✝ : V
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
ph : Adj G v✝ v✝
hp : Walk.IsPath p ∧ ¬v✝ ∈ Walk.support p
h✝ : Adj G v✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬v✝ ∈ Walk.support q
⊢ Walk.cons ph p = Walk.cons h✝ q
simp at hq
no goals
case mk.mk.cons.inl.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝¹ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : Walk.IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ Walk.edges q
⊢ Walk.cons ph p = Walk.cons h✝ q
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath (Walk.cons ph p)
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
rw [Walk.cons_isPath_iff] at hp
no goals
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.IsPath p → ∀ (q : Walk G v✝ w✝), Walk.IsPath q → p = q
hp : Walk.IsPath p ∧ ¬u✝ ∈ Walk.support p
q : Walk G u✝ w✝
hq : Walk.IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ Walk.edges p
⊢ Walk.cons ph p = q
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2