V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔
    ∀ ⦃v w : V⦄,
      Adj G 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
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔ ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
simp_rw [isBridge_iff_adj_and_forall_cycle_not_mem]
case mp
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G →
    ∀ ⦃v w : V⦄,
      Adj G 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

case mpr
V : Type u
G : SimpleGraph V
⊢ (∀ ⦃v w : V⦄,
      Adj G 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) →
    IsAcyclic G
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔
    ∀ ⦃v w : V⦄,
      Adj G 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
constructor
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G 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
case mp
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G →
    ∀ ⦃v w : V⦄,
      Adj G 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
intro ha v w hvw
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : 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
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G 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
apply And.intro hvw
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G v w
u : V
p : Walk G u u
hp : Walk.IsCycle p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : 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
intro u p hp
no goals
case mp
V : Type u
G : SimpleGraph V
ha : IsAcyclic G
v w : V
hvw : Adj G v w
u : V
p : Walk G u u
hp : Walk.IsCycle p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
cases ha p hp
case mpr.nil
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v : V
hp : Walk.IsCycle Walk.nil
⊢ False

case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ False
case mpr
V : Type u
G : SimpleGraph V
⊢ (∀ ⦃v w : V⦄,
      Adj G 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) →
    IsAcyclic G
rintro hb v (_ | ⟨ha, p⟩) hp
no goals
case mpr.nil
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v : V
hp : Walk.IsCycle Walk.nil
⊢ False
exact hp.not_of_nil
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges (Walk.cons ha p)
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ False
apply (hb ha).2 _ hp
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) :: Walk.edges p
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges (Walk.cons ha p)
rw [Walk.edges_cons]
no goals
case mpr.cons
V : Type u
G : SimpleGraph V
hb :
  ∀ ⦃v w : V⦄,
    Adj G 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
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : Walk.IsCycle (Walk.cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) :: Walk.edges p
apply List.mem_cons_self