awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
⊢ ∃ (H' : SimpleGraph V), H ≤ H' ∧ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) H'

Tactic:
zorn_le_nonempty₀ {H | H ≤ G ∧ H.IsAcyclic} (fun c hcs hc y hy ↦ ?_) _ ⟨hHG, hH⟩

Premises used: Set.Mem, SimpleGraph.IsAcyclic, setOf, LE.le, And, And.intro, zorn_le_nonempty₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
refine :
  ∀ (c : Set (SimpleGraph V)) (hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic})
    (hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c) (y : SimpleGraph V) (hy : y ∈ c),
    ∃ (ub : SimpleGraph V),
      Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (H' : SimpleGraph V), H ≤ H' ∧ Maximal (fun (H : SimpleGraph V) ↦ H ≤ G ∧ H.IsAcyclic) H'

Tactic:
refine zorn_le_nonempty₀ {H | H ≤ G ∧ H.IsAcyclic} (fun c hcs hc y hy ↦ ?_) _ ⟨hHG, hH⟩

Premises used: SimpleGraph.IsAcyclic, setOf, LE.le, And, And.intro, zorn_le_nonempty₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ ∃ (ub : SimpleGraph V),
    Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
⟨sSup c, ⟨?_, ?_⟩, fun _ ↦ le_sSup⟩

Premises used: And.intro, Exists.intro, le_sSup, SupSet.sSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
refine_1 : sSup c ≤ G
refine_2 : (sSup c).IsAcyclic
⊢ ∃ (ub : SimpleGraph V),
    Membership.mem (γ := Set (SimpleGraph V)) {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨sSup c, ⟨?_, ?_⟩, fun _ ↦ le_sSup⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ sSup c ≤ G

Tactic:
grind [sSup_le_iff]

Premises used: sSup_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ ∀ H ∈ c, H.IsAcyclic

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ (sSup c).IsAcyclic

Tactic:
exact isAcyclic_sSup_of_isAcyclic_directedOn c (by grind) hc.directedOn

Premises used: IsChain.directedOn, SimpleGraph.isAcyclic_sSup_of_isAcyclic_directedOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
c : G.ConnectedComponent
⊢ Function.Injective (α := ↥c) (β := V) (⇑c.toSimpleGraph_hom : (a : ↥c) → V)

Tactic:
simp [ConnectedComponent.toSimpleGraph_hom]

Premises used: SimpleGraph.ConnectedComponent.toSimpleGraph_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ 3 ≤ p.length

Tactic:
have := hp.three_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this : 3 ≤ p.length
⊢ p.support.tail.length ≤ 2

Tactic:
have := Nat.cast_le.mp <| hp.support_nodup.length_le_enatCard.trans h
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this_1 : 3 ≤ p.length
this : p.support.tail.length ≤ 2
⊢ p.length + 1 - 1 ≤ 2

Tactic:
rw [List.length_tail, p.length_support] at this

Premises used: SimpleGraph.Walk.length_support, List.length_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this_1 : 3 ≤ p.length
this : p.length + 1 - 1 ≤ 2
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
inst : Subsingleton V
G : SimpleGraph V
⊢ G.IsAcyclic

Tactic:
.of_card_le_two <| ENat.card_le_one.trans one_le_two

Premises used: SimpleGraph.IsAcyclic.of_card_le_two, one_le_two, LE.le.trans, ENat.card_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ IsAcyclic.{u_1} (V := (↑(verts (G := G) ⊥) : Type u_1)) (Subgraph.coe ⊥)

Tactic:
@IsAcyclic.of_subsingleton _ (Set.isEmpty_coe_sort.mpr rfl).instSubsingleton _

Premises used: SimpleGraph.IsAcyclic.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
inst : Nonempty V
inst_1 : Subsingleton V
G : SimpleGraph V
⊢ G.IsTree

Tactic:
⟨.of_subsingleton, .of_subsingleton⟩

Premises used: SimpleGraph.IsAcyclic.of_subsingleton, SimpleGraph.Connected.of_subsingleton, SimpleGraph.IsTree.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).coe.IsTree

Tactic:
.of_subsingleton

Premises used: SimpleGraph.IsTree.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).coe.IsTree

Tactic:
⟨Subgraph.subgraphOfAdj_connected h, fun w p hp ↦ ?_⟩

Premises used: SimpleGraph.Subgraph.subgraphOfAdj_connected, SimpleGraph.IsTree.mk, SimpleGraph.Subgraph.Connected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
refine : ∀ (w : (↑(G.subgraphOfAdj h).verts : Type u_1)) (p : (G.subgraphOfAdj h).coe.Walk w w) (hp : p.IsCycle), False
⊢ (G.subgraphOfAdj h).coe.IsTree

Tactic:
refine ⟨Subgraph.subgraphOfAdj_connected h, fun w p hp ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
⊢ s(u, v) = s((↑w : V), (↑p.snd : V))

Tactic:
have : _ = _ := p.adj_snd hp.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this : s(u, v) = s((↑w : V), (↑p.snd : V))
⊢ s(u, v) = s((↑p.penultimate : V), (↑w : V))

Tactic:
have : _ = _ := p.adj_penultimate hp.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
⊢ p.IsCycle

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
hp₁ : p.IsCycle
⊢ (↑p.penultimate : V) = (↑w : V) ∧ (↑w : V) = (↑p.snd : V) ∨ (↑p.penultimate : V) = (↑p.snd : V)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : s(u, v) = s((↑w : V), (↑p.snd : V))
this : s(u, v) = s((↑p.penultimate : V), (↑w : V))
hp₁ : p.IsCycle
this₁ : (↑p.penultimate : V) = (↑w : V) ∧ (↑w : V) = (↑p.snd : V) ∨ (↑p.penultimate : V) = (↑p.snd : V)
⊢ u = (↑p.penultimate : V) ∧ v = (↑w : V) ∨ u = (↑w : V) ∧ v = (↑p.penultimate : V)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : (↑(G.subgraphOfAdj h).verts : Type u_1)
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this_1 : (↑p.penultimate : V) = (↑w : V) ∧ (↑w : V) = (↑p.snd : V) ∨ (↑p.penultimate : V) = (↑p.snd : V)
this : u = (↑p.penultimate : V) ∧ v = (↑w : V) ∨ u = (↑w : V) ∧ v = (↑p.penultimate : V)
⊢ False

Tactic:
grind [IsCycle.snd_ne_penultimate]

Premises used: SimpleGraph.Walk.IsCycle.snd_ne_penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
simp_rw : 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
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

Tactic:
simp_rw [isBridge_iff_adj_and_forall_cycle_notMem]

Premises used: SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
mp : 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
mpr : (∀ ⦃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
⊢ 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
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
ha : G.IsAcyclic
v w : V
hvw : G.Adj v w
mp : ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
⊢ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
apply And.intro hvw

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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 : IsCycle.{u_1} (V := V) (G := G) (u := v) nil
⊢ False

Tactic:
hp.not_of_nil

Premises used: SimpleGraph.Walk.IsCycle.not_of_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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 : IsCycle.{u_1} (V := V) (G := G) (u := v) nil
⊢ False

Tactic:
exact hp.not_of_nil

Premises used: SimpleGraph.Walk.IsCycle.not_of_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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_1 : V
ha : G.Adj v v_1
p : G.Walk v_1 v
hp : (cons ha p).IsCycle
mpr : s(v, v_1) ∈ (cons ha p).edges
⊢ False

Tactic:
apply (hb ha).2 _ hp

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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_1 : V
ha : G.Adj v v_1
p : G.Walk v_1 v
hp : (cons ha p).IsCycle
mpr : s(v, v_1) ∈ s(v, v_1) :: p.edges
⊢ s(v, v_1) ∈ (cons ha p).edges

Tactic:
rw [Walk.edges_cons]

Premises used: SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
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_1 : V
ha : G.Adj v v_1
p : G.Walk v_1 v
hp : (cons ha p).IsCycle
⊢ s(v, v_1) ∈ s(v, v_1) :: p.edges

Tactic:
apply List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

Tactic:
simp [isAcyclic_iff_forall_adj_isBridge, Sym2.forall]

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge, Sym2.forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p q : G.Path v w
obtain : ∀ (p : G.Walk v w) (hp : p.IsPath), Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
⊢ p = q

Tactic:
obtain ⟨p, hp⟩ := p
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
q : G.Path v w
p : G.Walk v w
hp : p.IsPath
obtain :
  ∀ (q : G.Walk v w) (hq : q.IsPath),
    Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) q hq
⊢ Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q

Tactic:
obtain ⟨q, hq⟩ := q
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
rw : p = q
⊢ Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) q hq

Tactic:
rw [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w u : V
hp : IsPath.{u_1} (V := V) (G := G) (u := u) Walk.nil
q : G.Walk u u
hq : q.IsPath
nil : ∀ (hq : IsPath.{u_1} (V := V) (G := G) (u := u) Walk.nil), Eq.{u_1 + 1} (α := G.Walk u u) Walk.nil Walk.nil
⊢ Walk.nil = q

Tactic:
cases (Walk.isPath_iff_eq_nil _).mp hq

Premises used: Iff.mp, SimpleGraph.Walk.isPath_iff_eq_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w u : V
hp hq : IsPath.{u_1} (V := V) (G := G) (u := u) nil
⊢ Eq.{u_1 + 1} (α := G.Walk u u) nil nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (Walk.cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
cons :
  ∀ (h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)) {v w u v w : V} (ph : G.Adj u v) (p : G.Walk v w)
    (ih : ∀ (hp : p.IsPath) (q : G.Walk v w) (hq : q.IsPath), p = q) (hp : (Walk.cons ph p).IsPath) (q : G.Walk u w)
    (hq : q.IsPath), Walk.cons ph p = q
⊢ Walk.cons ph p = q

Tactic:
rw [isAcyclic_iff_forall_adj_isBridge] at h

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
⊢ G.IsBridge s(u, v_1)

Tactic:
specialize h ph
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : G.IsBridge s(u, v_1)
⊢ G.Adj u v_1 ∧ ∀ (p : G.Walk u v_1), s(u, v_1) ∈ p.edges

Tactic:
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h

Premises used: SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : G.Adj u v_1 ∧ ∀ (p : G.Walk u v_1), s(u, v_1) ∈ p.edges
⊢ s(u, v_1) ∈ (q.append p.reverse).edges

Tactic:
replace h := h.2 (q.append p.reverse)
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ (q.append p.reverse).edges
⊢ s(u, v_1) ∈ q.edges ∨ s(u, v_1) ∈ p.edges

Tactic:
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h

Premises used: List.mem_reverse, List.mem_append, SimpleGraph.Walk.edges_append, SimpleGraph.Walk.edges_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (Walk.cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ q.edges ∨ s(u, v_1) ∈ p.edges
cons : ∀ (h : s(u, v_1) ∈ q.edges), Walk.cons ph p = q
cons₁ : ∀ (h : s(u, v_1) ∈ p.edges), Walk.cons ph p = q
⊢ Walk.cons ph p = q

Tactic:
rcases h with h | h
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 u
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 u) (hq : q.IsPath), p = q
hp : (cons ph p).IsPath
hq : IsPath.{u_1} (V := V) (G := G) (u := u) nil
h : Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) s(u, v_1)
⊢ cons ph p = nil

Tactic:
simp at hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (Walk.cons ph p).IsPath
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : (Walk.cons h_1 q).IsPath
h : s(u, v_1) ∈ (Walk.cons h_1 q).edges
cons :
  ∀ (hp : p.IsPath ∧ u ∉ p.support) {v : V} (h : G.Adj u v) (q : G.Walk v w_1) (hq : q.IsPath ∧ u ∉ q.support)
    (h_2 : s(u, v_1) ∈ (Walk.cons h q).edges), Walk.cons ph p = Walk.cons h q
⊢ Walk.cons ph p = Walk.cons h_1 q

Tactic:
rw [Walk.cons_isPath_iff] at hp hq

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : q.IsPath ∧ u ∉ q.support
h : s(u, v_1) ∈ (cons h_1 q).edges
⊢ (v_1 = v_2 ∨ u = v_2 ∧ v_1 = u) ∨ s(u, v_1) ∈ q.edges

Tactic:
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h

Premises used: SimpleGraph.Walk.edges_cons, Sym2.eq_iff, List.mem_cons, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : q.IsPath ∧ u ∉ q.support
h : (v_1 = v_2 ∨ u = v_2 ∧ v_1 = u) ∨ s(u, v_1) ∈ q.edges
cons : ∀ (h : G.Adj u v_1) (q : G.Walk v_1 w_1) (hq : q.IsPath ∧ u ∉ q.support), Walk.cons ph p = Walk.cons h q
cons₁ :
  ∀ (ph : G.Adj v_1 v_1) (hp : p.IsPath ∧ v_1 ∉ p.support) (h : G.Adj v_1 v_1) (q : G.Walk v_1 w_1)
    (hq : q.IsPath ∧ v_1 ∉ q.support), Walk.cons ph p = Walk.cons h q
cons₂ : ∀ (h : s(u, v_1) ∈ q.edges), Walk.cons ph p = Walk.cons h_1 q
⊢ Walk.cons ph p = Walk.cons h_1 q

Tactic:
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
h : G.Adj u v_1
q : G.Walk v_1 w_1
hq : q.IsPath ∧ u ∉ q.support
cons : ∀ (hq : p.IsPath ∧ u ∉ p.support), Walk.cons ph p = Walk.cons h p
⊢ Walk.cons ph p = Walk.cons h q

Tactic:
cases ih hp.1 q hq.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
h : G.Adj u v_1
hq : p.IsPath ∧ u ∉ p.support
⊢ cons ph p = cons h p

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
ph : G.Adj v_1 v_1
hp : p.IsPath ∧ v_1 ∉ p.support
h : G.Adj v_1 v_1
q : G.Walk v_1 w_1
hq : q.IsPath ∧ v_1 ∉ q.support
⊢ cons ph p = cons h q

Tactic:
simp at hq
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : q.IsPath ∧ u ∉ q.support
h : s(u, v_1) ∈ q.edges
⊢ cons ph p = cons h_1 q

Tactic:
absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2

Premises used: absurd, And.right, SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : q.IsPath ∧ u ∉ q.support
h : s(u, v_1) ∈ q.edges
⊢ cons ph p = cons h_1 q

Tactic:
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2

Premises used: absurd, And.right, SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (Walk.cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ q.edges
cons :
  ∀ (p : G.Walk v_1 u) (ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 u) (hq : q.IsPath), p = q) (hp : (Walk.cons ph p).IsPath)
    (hq : IsPath.{u_1} (V := V) (G := G) (u := u) nil)
    (h : Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) s(u, v_1)), Walk.cons ph p = nil
cons₁ :
  ∀ {v : V} (h : G.Adj u v) (q : G.Walk v w_1) (hq : (Walk.cons h q).IsPath) (h_1 : s(u, v_1) ∈ (Walk.cons h q).edges),
    Walk.cons ph p = Walk.cons h q
⊢ Walk.cons ph p = q

Tactic:
cases q with
      | nil => simp at hp
      | cons _ q =>
        rw [Walk.cons_isPath_iff] at hp hq
        simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
        rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
        · cases ih hp.1 q hq.1
          rfl
        · simp at hq
        · exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, Sym2.eq_iff, SimpleGraph.Walk.nil, SimpleGraph.Walk.cons_isPath_iff, List.mem_cons, rfl, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : (Walk.cons ph p).IsPath
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ p.edges
cons :
  ∀ (hp : p.IsPath ∧ u ∉ p.support) (q : G.Walk u w_1) (hq : q.IsPath) (h : s(u, v_1) ∈ p.edges), Walk.cons ph p = q
⊢ Walk.cons ph p = q

Tactic:
rw [Walk.cons_isPath_iff] at hp

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ p.edges
⊢ cons ph p = q

Tactic:
absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2

Premises used: absurd, And.right, SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v w u v_1 w_1 : V
ph : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ (hp : p.IsPath) (q : G.Walk v_1 w_1) (hq : q.IsPath), p = q
hp : p.IsPath ∧ u ∉ p.support
q : G.Walk u w_1
hq : q.IsPath
h : s(u, v_1) ∈ p.edges
⊢ cons ph p = q

Tactic:
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2

Premises used: absurd, And.right, SimpleGraph.Walk.fst_mem_support_of_mem_edges