V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ Adj G v w →
    (¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
      ∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w)) ↔
    Adj G v w ∧ ∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [isBridge_iff, and_congr_right_iff]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ ¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ Adj G v w →
    (¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
      ∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p)
intro h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ ¬¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ¬∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ ¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [← not_iff_not]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    Exists fun ⦃u⦄ => ∃ p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ ¬¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ¬∀ ⦃u : V⦄ (p : Walk G u u), Walk.IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
push_neg
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    Adj G v w ∧ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    Exists fun ⦃u⦄ => ∃ p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [← adj_and_reachable_delete_edges_iff_exists_cycle]
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
⊢ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    Adj G v w ∧ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w
simp only [h, true_and_iff]