-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
theorem isAcyclic_iff_forall_adj_isBridge :
    G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

Proof state:
case mpr.nil
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v : V
hp : nil.IsCycle
⊢ False

Tactic:
exact hp.not_of_nil

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic → ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

case mpr
V : Type u
G : SimpleGraph V
⊢ (∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges) → G.IsAcyclic

Proof state:
case mpr
V : Type u
G : SimpleGraph V
⊢ (∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges) → G.IsAcyclic

Tactic:
rintro hb v (_ | ⟨ha, p⟩) hp

Result:
case mpr.nil
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v : V
hp : nil.IsCycle
⊢ False

case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

Tactic:
simp_rw [isBridge_iff_adj_and_forall_cycle_not_mem]

Result:
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Proof state:
case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ False

Tactic:
apply (hb ha).2 _ hp

Result:
case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ s(v, v✝) ∈ (cons ha p).edges

Proof state:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ s(v, w) ∉ p.edges

Tactic:
cases ha p hp

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic → ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
intro ha v w hvw

Result:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
⊢ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Proof state:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
⊢ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
apply And.intro hvw

Result:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
⊢ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Proof state:
case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ s(v, v✝) ∈ s(v, v✝) :: p.edges

Tactic:
apply List.mem_cons_self

Result:
no goals

Proof state:
case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ s(v, v✝) ∈ (cons ha p).edges

Tactic:
rw [Walk.edges_cons]

Result:
case mpr.cons
V : Type u
G : SimpleGraph V
hb : ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
v v✝ : V
ha : G.Adj v v✝
p : G.Walk v✝ v
hp : (cons ha p).IsCycle
⊢ s(v, v✝) ∈ s(v, v✝) :: p.edges

Proof state:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
⊢ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
intro u p hp

Result:
case mp
V : Type u
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ s(v, w) ∉ p.edges