awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
nil : ∀ {u : V} (hp : IsPath.{u_1} (V := V) (G := G) (u := u) Walk.nil) (q : G.Walk u u) (hq : q.IsPath), Walk.nil = q
cons :
  ∀ {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
⊢ p = q

Tactic:
induction p with
  | nil =>
    cases (Walk.isPath_iff_eq_nil _).mp hq
    rfl
  | cons ph p ih =>
    rw [isAcyclic_iff_forall_adj_isBridge] at h
    specialize h ph
    rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
    replace h := h.2 (q.append p.reverse)
    simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
    rcases h with h | h
    · 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
    · rw [Walk.cons_isPath_iff] at hp
      exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge, SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges, List.mem_reverse, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, List.mem_append, Sym2.eq_iff, SimpleGraph.Walk.nil, Iff.mp, SimpleGraph.Walk.edges_append, SimpleGraph.Walk.edges_reverse, SimpleGraph.Walk.cons_isPath_iff, List.mem_cons, SimpleGraph.Walk.isPath_iff_eq_nil, rfl, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ c.IsTrail ∧ ¬c = nil ∧ c.support.tail.Nodup

Tactic:
simp only [Walk.isCycle_def, Ne] at hc

Premises used: SimpleGraph.Walk.isCycle_def, Ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
hc :
  IsTrail.{u_1} (V := V) (G := G) (u := v) nil ∧
    ¬Eq.{u_1 + 1} (α := G.Walk v v) nil nil ∧ List.Nodup.{u_1} (α := V) (List.tail (Walk.support (G := G) (u := v) nil))
⊢ False

Tactic:
cases hc.2.1 rfl

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v_1 : V
ha : G.Adj v v_1
c' : G.Walk v_1 v
hc : (cons ha c').IsTrail ∧ ¬cons ha c' = nil ∧ (cons ha c').support.tail.Nodup
⊢ (c'.IsTrail ∧ s(v, v_1) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup

Tactic:
simp only [Walk.isTrail_cons, Walk.support_cons, List.tail_cons] at hc

Premises used: SimpleGraph.Walk.support_cons, List.tail_cons, SimpleGraph.Walk.isTrail_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v_1 : V
ha : G.Adj v v_1
c' : G.Walk v_1 v
hc : (c'.IsTrail ∧ s(v, v_1) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
⊢ c'.IsPath

Tactic:
simp only [Walk.isPath_def, hc.2]

Premises used: SimpleGraph.Walk.isPath_def, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v_1 : V
ha : G.Adj v v_1
c' : G.Walk v_1 v
hc : (c'.IsTrail ∧ s(v, v_1) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
⊢ Subtype.mk (p := fun (p : G.Walk v_1 v) ↦ p.IsPath) c' ⋯ = Path.singleton ⋯

Tactic:
specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)

Premises used: SimpleGraph.Adj.symm, Subtype.mk, SimpleGraph.Path.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v v_1 : V
ha : G.Adj v v_1
c' : G.Walk v_1 v
hc : (c'.IsTrail ∧ s(v, v_1) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : Subtype.mk (p := fun (p : G.Walk v_1 v) ↦ p.IsPath) c' ⋯ = Path.singleton ⋯
⊢ c' = cons ⋯ nil

Tactic:
rw [Path.singleton, Subtype.mk.injEq] at h

Premises used: SimpleGraph.Path.singleton, Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
v v_1 : V
ha : G.Adj v v_1
c' : G.Walk v_1 v
hc : (c'.IsTrail ∧ s(v, v_1) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : c' = cons ⋯ nil
⊢ False

Tactic:
simp [h] at hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsTrail ∧ ¬c = Walk.nil ∧ c.support.tail.Nodup
nil :
  ∀
    (hc :
      IsTrail.{u_1} (V := V) (G := G) (u := v) Walk.nil ∧
        ¬Eq.{u_1 + 1} (α := G.Walk v v) Walk.nil Walk.nil ∧
          List.Nodup.{u_1} (α := V) (List.tail (Walk.support (G := G) (u := v) Walk.nil))),
    False
cons :
  ∀ {v_1 : V} (ha : G.Adj v v_1) (c' : G.Walk v_1 v)
    (hc : (Walk.cons ha c').IsTrail ∧ ¬Walk.cons ha c' = Walk.nil ∧ (Walk.cons ha c').support.tail.Nodup), False
⊢ False

Tactic:
cases c with
  | nil => cases hc.2.1 rfl
  | cons ha c' =>
    simp only [Walk.isTrail_cons, Walk.support_cons, List.tail_cons] at hc
    specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
    rw [Path.singleton, Subtype.mk.injEq] at h
    simp [h] at hc

Premises used: SimpleGraph.Walk.support_cons, List.tail_cons, SimpleGraph.Path.singleton, SimpleGraph.Walk.cons, And.right, And.left, SimpleGraph.Walk.nil, Subtype.mk.injEq, SimpleGraph.Walk.isTrail_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
⟨IsAcyclic.path_unique, isAcyclic_of_path_unique⟩

Premises used: SimpleGraph.isAcyclic_of_path_unique, SimpleGraph.IsAcyclic.path_unique, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃u v : V⦄, Subsingleton.{u_1 + 1} (G.Path u v)

Tactic:
simp [isAcyclic_iff_path_unique, subsingleton_iff]

Premises used: subsingleton_iff, SimpleGraph.isAcyclic_iff_path_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj u w
hsupp : w ∈ p.support
⊢ Subtype.mk (p := fun (p : G.Walk u w) ↦ p.IsPath) (p.takeUntil w hsupp) ⋯ = Path.singleton hadj

Tactic:
have := isAcyclic_iff_path_unique.mp h ⟨_, hp.takeUntil hsupp⟩ <| .singleton hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj u w
hsupp : w ∈ p.support
this : Subtype.mk (p := fun (p : G.Walk u w) ↦ p.IsPath) (p.takeUntil w hsupp) ⋯ = Path.singleton hadj
⊢ w = p.snd

Tactic:
grind [p.getVert_length_takeUntil hsupp, Path.singleton_coe, length]

Premises used: SimpleGraph.Path.singleton_coe, SimpleGraph.Walk.length, SimpleGraph.Walk.getVert_length_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj u w
hsupp : w ∈ p.support
have have₁ have₂ :
  ∀ (this : Subtype.mk (p := fun (p : G.Walk u w) ↦ p.IsPath) (p.takeUntil w hsupp) ⋯ = Path.singleton hadj), w = p.snd
⊢ w = p.snd

Tactic:
classical
  have := isAcyclic_iff_path_unique.mp h ⟨_, hp.takeUntil hsupp⟩ <| .singleton hadj
  grind [p.getVert_length_takeUntil hsupp, Path.singleton_coe, length]

Premises used: SimpleGraph.Path.singleton_coe, SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
rw : w = p.reverse.snd
⊢ w = p.penultimate

Tactic:
rw [← snd_reverse]

Premises used: SimpleGraph.Walk.snd_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
apply : w ∈ p.reverse.support
⊢ w = p.reverse.snd

Tactic:
apply h.eq_snd_of_adj_start hp.reverse hadj

Premises used: SimpleGraph.IsAcyclic.eq_snd_of_adj_start, SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w ∈ p.reverse.support

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
rw : w ∈ (q.concat ⋯).support
⊢ w ∈ p.support

Tactic:
rw [Subtype.mk.inj <| isAcyclic_iff_path_unique.mp hG ⟨p, hp⟩ ⟨_, hq.concat hv hadj.symm⟩]

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.IsPath.concat, Subtype.mk.inj, Subtype.mk, Iff.mp, SimpleGraph.isAcyclic_iff_path_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support

Tactic:
q.support_subset_support_concat _ q.end_mem_support

Premises used: SimpleGraph.Walk.end_mem_support, SimpleGraph.Walk.support_subset_support_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support

Tactic:
exact q.support_subset_support_concat _ q.end_mem_support

Premises used: SimpleGraph.Walk.end_mem_support, SimpleGraph.Walk.support_subset_support_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
obtain :
  ∀ (p₀ : G.Walk u w) (p₁ : G.Walk w v) (hp₀ : p₀.IsPath) (hp₁ : p₁.IsPath) (happend : p = p₀.append p₁), v ∉ q.support
⊢ v ∉ q.support

Tactic:
obtain ⟨p₀, p₁, hp₀, hp₁, happend⟩ := hp.mem_support_iff_exists_append.mp hw

Premises used: SimpleGraph.Walk.IsPath.mem_support_iff_exists_append, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
rw : v ∉ p₀.support
⊢ v ∉ q.support

Tactic:
rw [← Subtype.mk.inj <| hG.path_unique ⟨p₀, hp₀⟩ ⟨q, hq⟩]

Premises used: SimpleGraph.IsAcyclic.path_unique, Subtype.mk.inj, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support

Tactic:
fun hxp => (happend ▸ hp).ne_of_mem_support_of_append hadj.symm.ne' hxp
    (p₁.end_mem_support) rfl

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support

Tactic:
exact fun hxp => (happend ▸ hp).ne_of_mem_support_of_append hadj.symm.ne' hxp
    (p₁.end_mem_support) rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
⊢ w ∉ p.support

Tactic:
have hw : w ∉ p.support := hG.ne_mem_support_of_support_of_adj_of_isPath hq hp hadj.symm hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
hw : w ∉ p.support
⊢ q = p.concat hadj

Tactic:
Subtype.mk.inj <| isAcyclic_iff_path_unique.mp hG ⟨q, hq⟩ ⟨_, hp.concat hw hadj⟩

Premises used: SimpleGraph.Walk.IsPath.concat, Subtype.mk.inj, Subtype.mk, Iff.mp, SimpleGraph.isAcyclic_iff_path_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
hw : w ∉ p.support
⊢ q = p.concat hadj

Tactic:
exact Subtype.mk.inj <| isAcyclic_iff_path_unique.mp hG ⟨q, hq⟩ ⟨_, hp.concat hw hadj⟩

Premises used: SimpleGraph.Walk.IsPath.concat, Subtype.mk.inj, Subtype.mk, Iff.mp, SimpleGraph.isAcyclic_iff_path_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
rw : (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
rw [isTree_iff, isAcyclic_iff_path_unique]

Premises used: SimpleGraph.isTree_iff, SimpleGraph.isAcyclic_iff_path_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
mp : (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
mpr : (Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath) → G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
⟨hc.nonempty, ?_⟩

Premises used: SimpleGraph.Connected.nonempty, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
mp : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
refine ⟨hc.nonempty, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
h :
  (fun (p : G.Walk v w) ↦ p.IsPath) (↑q : G.Walk v w) ∧
    ∀ (y : G.Walk v w), (fun (p : G.Walk v w) ↦ p.IsPath) y → y = (↑q : G.Walk v w)
⊢ ∃! p : G.Walk v w, p.IsPath

Tactic:
use q
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
h : ∀ (y : G.Walk v w), y.IsPath → y = (↑q : G.Walk v w)
⊢ (fun (p : G.Walk v w) ↦ p.IsPath) (↑q : G.Walk v w) ∧
    ∀ (y : G.Walk v w), (fun (p : G.Walk v w) ↦ p.IsPath) y → y = (↑q : G.Walk v w)

Tactic:
simp only [true_and, Path.isPath]

Premises used: SimpleGraph.Path.isPath, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
⊢ Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q

Tactic:
specialize hu ⟨p, hp⟩ q

Premises used: Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
⊢ p = (↑q : G.Walk v w)

Tactic:
Subtype.ext_iff.mp hu

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
⊢ p = (↑q : G.Walk v w)

Tactic:
exact Subtype.ext_iff.mp hu

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
⊢ G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
⟨Connected.mk ?_, ?_⟩

Premises used: SimpleGraph.Connected.mk, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
mpr : G.Preconnected
mpr₁ : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
refine ⟨Connected.mk ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
v w : V
mpr :
  ∀ (p : G.Walk v w),
    ((fun (p : G.Walk v w) ↦ p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun (p : G.Walk v w) ↦ p.IsPath) y → y = p) →
      G.Reachable v w
⊢ G.Reachable v w

Tactic:
obtain ⟨p, _⟩ := h v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
v w : V
p : G.Walk v w
h_1 : (fun (p : G.Walk v w) ↦ p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun (p : G.Walk v w) ↦ p.IsPath) y → y = p
⊢ G.Reachable v w

Tactic:
p.reachable

Premises used: SimpleGraph.Walk.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
v w : V
p : G.Walk v w
h_1 : (fun (p : G.Walk v w) ↦ p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun (p : G.Walk v w) ↦ p.IsPath) y → y = p
⊢ G.Reachable v w

Tactic:
exact p.reachable

Premises used: SimpleGraph.Walk.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
v w : V
p : G.Walk v w
hp : p.IsPath
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

Tactic:
simp only [ExistsUnique.unique (h v w) hp hq]

Premises used: ExistsUnique.unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
rw : G.Connected ∧ G.IsAcyclic ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
rw₁ rw₂ rw₃ :
  (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
mp : (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
mpr mpr₁ : (Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath) → G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
classical
  rw [isTree_iff, isAcyclic_iff_path_unique]
  constructor
  · rintro ⟨hc, hu⟩
    refine ⟨hc.nonempty, ?_⟩
    intro v w
    let q := (hc v w).some.toPath
    use q
    simp only [true_and, Path.isPath]
    intro p hp
    specialize hu ⟨p, hp⟩ q
    exact Subtype.ext_iff.mp hu
  · rintro ⟨hV, h⟩
    refine ⟨Connected.mk ?_, ?_⟩
    · intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable
    · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
      simp only [ExistsUnique.unique (h v w) hp hq]

Premises used: SimpleGraph.isTree_iff, SimpleGraph.Path.isPath, SimpleGraph.isAcyclic_iff_path_unique, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
⊢ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

Tactic:
(isTree_iff_existsUnique_path.1 hG).2

Premises used: SimpleGraph.isTree_iff_existsUnique_path, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges

Tactic:
⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩

Premises used: SimpleGraph.Walk.edges_nodup_of_support_nodup, SimpleGraph.Walk.isPath_def, Iff.intro, Iff.mp, List.Pairwise.isChain
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
refine : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges), p.IsPath
⊢ p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges

Tactic:
refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u : V
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (edges (G := G) (u := u) nil)
⊢ IsPath.{u_1} (V := V) (G := G) (u := u) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (cons head tail).edges
⊢ (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges

Tactic:
have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
⊢ (cons head tail).IsPath

Tactic:
cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩

Premises used: Iff.mpr, And.right, And.intro, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (Walk.cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
cons : u' ∉ tail.support
⊢ (Walk.cons head tail).IsPath

Tactic:
refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩

Premises used: Iff.mpr, And.right, And.intro, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (Walk.cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
cons : ∀ (h' : tail.length = 0), u' ∉ tail.support
cons₁ : ∀ (h' : tail.length > 0), u' ∉ tail.support
⊢ u' ∉ tail.support

Tactic:
rcases tail.length.eq_zero_or_pos with h' | h'

Premises used: SimpleGraph.Walk.length, Nat.eq_zero_or_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
h' : tail.length = 0
⊢ u' ∉ tail.support

Tactic:
simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]

Premises used: SimpleGraph.Walk.nil_iff_support_eq, SimpleGraph.Adj.ne, Iff.mp, SimpleGraph.Walk.length_eq_zero_iff