[GOAL]
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))
[PROOFSTEP]
simp_rw [isBridge_iff_adj_and_forall_cycle_not_mem]
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
constructor
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
intro ha v w hvw
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
apply And.intro hvw
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
intro u p hp
[GOAL]
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 : IsCycle p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
[PROOFSTEP]
cases ha p hp
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p) →
    IsAcyclic G
[PROOFSTEP]
rintro hb v (_ | ⟨ha, p⟩) hp
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v : V
hp : IsCycle nil
⊢ False
[PROOFSTEP]
exact hp.not_of_nil
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ False
[PROOFSTEP]
apply (hb ha).2 _ hp
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges (cons ha p)
[PROOFSTEP]
rw [Walk.edges_cons]
[GOAL]
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), IsCycle p → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edges p
v v✝ : V
ha : Adj G v v✝
p : Walk G v✝ v
hp : IsCycle (cons ha p)
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝) :: edges p
[PROOFSTEP]
apply List.mem_cons_self
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsAcyclic G ↔ ∀ ⦃e : Sym2 V⦄, e ∈ edgeSet G → IsBridge G e
[PROOFSTEP]
simp [isAcyclic_iff_forall_adj_isBridge, Sym2.forall]
[GOAL]
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p q : Path G v w
⊢ p = q
[PROOFSTEP]
obtain ⟨p, hp⟩ := p
[GOAL]
case mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
q : Path G v w
p : Walk G v w
hp : IsPath p
⊢ { val := p, property := hp } = q
[PROOFSTEP]
obtain ⟨q, hq⟩ := q
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
[PROOFSTEP]
rw [Subtype.mk.injEq]
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ p = q
[PROOFSTEP]
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 
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] 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
[GOAL]
case mk.mk
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ p = q
[PROOFSTEP]
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 
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] 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
[GOAL]
case mk.mk.nil
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp : IsPath nil
q : Walk G u✝ u✝
hq : IsPath q
⊢ nil = q
[PROOFSTEP]

| nil =>
  cases (Walk.isPath_iff_eq_nil _).mp hq
  rfl
[GOAL]
case mk.mk.nil
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp : IsPath nil
q : Walk G u✝ u✝
hq : IsPath q
⊢ nil = q
[PROOFSTEP]
cases (Walk.isPath_iff_eq_nil _).mp hq
[GOAL]
case mk.mk.nil.refl
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ : V
hp hq : IsPath nil
⊢ nil = nil
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]

| 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 
  cases' h with h h
  ·
    cases q with
    | nil => simp [Walk.isPath_def] 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
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : IsAcyclic G
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]
rw [isAcyclic_iff_forall_adj_isBridge] at h 
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
h : ∀ ⦃v w : V⦄, Adj G v w → IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w))
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
⊢ cons ph p = q
[PROOFSTEP]
specialize h ph
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝))
⊢ cons ph p = q
[PROOFSTEP]
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h 
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Adj G u✝ v✝ ∧ ∀ (p : Walk G u✝ v✝), Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
replace h := h.2 (q.append p.reverse)
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges (append q (reverse p))
⊢ cons ph p = q
[PROOFSTEP]
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h 
[GOAL]
case mk.mk.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
cases' h with h h
[GOAL]
case mk.mk.cons.inl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q
⊢ cons ph p = q
[PROOFSTEP]
cases q with
| nil => simp [Walk.isPath_def] 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
[GOAL]
case mk.mk.cons.inl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges q
⊢ cons ph p = q
[PROOFSTEP]
cases q with
| nil => simp [Walk.isPath_def] 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
[GOAL]
case mk.mk.cons.inl.nil
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ u✝
ih : IsPath p → ∀ (q : Walk G v✝ u✝), IsPath q → p = q
hp : IsPath (cons ph p)
hq : IsPath nil
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges nil
⊢ cons ph p = nil
[PROOFSTEP]

| nil => simp [Walk.isPath_def] at hp 
[GOAL]
case mk.mk.cons.inl.nil
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ u✝
ih : IsPath p → ∀ (q : Walk G v✝ u✝), IsPath q → p = q
hp : IsPath (cons ph p)
hq : IsPath nil
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges nil
⊢ cons ph p = nil
[PROOFSTEP]
simp [Walk.isPath_def] at hp 
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath (cons h✝ q)
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]

| 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
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath (cons h✝ q)
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
rw [Walk.cons_isPath_iff] at hp hq 
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges (cons h✝ q)
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h 
[GOAL]
case mk.mk.cons.inl.cons
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
[GOAL]
case mk.mk.cons.inl.cons.inl.inl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
cases ih hp.1 q hq.1
[GOAL]
case mk.mk.cons.inl.cons.inl.inl.refl.refl
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
h✝ : Adj G u✝ v✝
hq : IsPath p ∧ ¬u✝ ∈ Walk.support p
⊢ cons ph p = cons h✝ p
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons.inl.cons.inl.inr.intro
V : Type u
G✝ G : SimpleGraph V
v w v✝ w✝ : V
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
ph : Adj G v✝ v✝
hp : IsPath p ∧ ¬v✝ ∈ Walk.support p
h✝ : Adj G v✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬v✝ ∈ Walk.support q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
simp at hq 
[GOAL]
case mk.mk.cons.inl.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : Adj G u✝ v✝¹
p : Walk G v✝¹ w✝
ih : IsPath p → ∀ (q : Walk G v✝¹ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
v✝ : V
h✝ : Adj G u✝ v✝
q : Walk G v✝ w✝
hq : IsPath q ∧ ¬u✝ ∈ Walk.support q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝¹) ∈ edges q
⊢ cons ph p = cons h✝ q
[PROOFSTEP]
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
[GOAL]
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath (cons ph p)
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
rw [Walk.cons_isPath_iff] at hp 
[GOAL]
case mk.mk.cons.inr
V : Type u
G✝ G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : IsPath p → ∀ (q : Walk G v✝ w✝), IsPath q → p = q
hp : IsPath p ∧ ¬u✝ ∈ Walk.support p
q : Walk G u✝ w✝
hq : IsPath q
h : Quotient.mk (Sym2.Rel.setoid V) (u✝, v✝) ∈ edges p
⊢ cons ph p = q
[PROOFSTEP]
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
⊢ IsAcyclic G
[PROOFSTEP]
intro v c hc
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsCycle c
⊢ False
[PROOFSTEP]
simp only [Walk.isCycle_def, Ne.def] at hc 
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsTrail c ∧ ¬c = nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
[PROOFSTEP]
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] 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 
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : IsTrail c ∧ ¬c = nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
[PROOFSTEP]
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] 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 
[GOAL]
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
hc : IsTrail nil ∧ ¬nil = nil ∧ List.Nodup (List.tail (Walk.support nil))
⊢ False
[PROOFSTEP]

| nil => cases hc.2.1 rfl
[GOAL]
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
hc : IsTrail nil ∧ ¬nil = nil ∧ List.Nodup (List.tail (Walk.support nil))
⊢ False
[PROOFSTEP]
cases hc.2.1 rfl
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : IsTrail (cons ha c') ∧ ¬cons ha c' = nil ∧ List.Nodup (List.tail (Walk.support (cons ha c')))
⊢ False
[PROOFSTEP]

| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] 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 
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : IsTrail (cons ha c') ∧ ¬cons ha c' = nil ∧ List.Nodup (List.tail (Walk.support (cons ha c')))
⊢ False
[PROOFSTEP]
simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc 
[GOAL]
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
⊢ False
[PROOFSTEP]
specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
[GOAL]
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
⊢ IsPath c'
[PROOFSTEP]
simp only [Walk.isPath_def, hc.2]
[GOAL]
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
h : { val := c', property := (_ : IsPath c') } = Path.singleton (_ : Adj G v✝ v)
⊢ False
[PROOFSTEP]
rw [Path.singleton, Subtype.mk.injEq] at h 
[GOAL]
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edges c') ∧ List.Nodup (Walk.support c')
h : c' = cons (_ : Adj G v✝ v) nil
⊢ False
[PROOFSTEP]
simp [h] at hc 
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsTree G ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
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_iff, 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]
[GOAL]
V : Type u
G : SimpleGraph V
⊢ IsTree G ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
rw [IsTree_iff, isAcyclic_iff_path_unique]
[GOAL]
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
rintro ⟨hc, hu⟩
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
refine ⟨hc.nonempty, ?_⟩
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ ∀ (v w : V), ∃! p, IsPath p
[PROOFSTEP]
intro v w
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
⊢ ∃! p, IsPath p
[PROOFSTEP]
let q := (hc v w).some.toPath
[GOAL]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∃! p, IsPath p
[PROOFSTEP]
use q
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ (fun p => IsPath p) ↑q ∧ ∀ (y : Walk G v w), (fun p => IsPath p) y → y = ↑q
[PROOFSTEP]
simp only [true_and_iff, Path.isPath]
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∀ (y : Walk G v w), IsPath y → y = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
intro p hp
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : IsPath p
⊢ p = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
specialize hu ⟨p, hp⟩ q
[GOAL]
case h
V : Type u
G : SimpleGraph V
hc : Connected G
v w : V
q : Path G v w := toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : IsPath p
hu : { val := p, property := hp } = q
⊢ p = ↑(toPath (Nonempty.some (_ : Reachable G v w)))
[PROOFSTEP]
exact Subtype.ext_iff.mp hu
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, IsPath p) → Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
rintro ⟨hV, h⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
refine ⟨Connected.mk ?_, ?_⟩
[GOAL]
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ Preconnected G
[PROOFSTEP]
intro v w
[GOAL]
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
⊢ Reachable G v w
[PROOFSTEP]
obtain ⟨p, _⟩ := h v w
[GOAL]
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
p : Walk G v w
h✝ : (fun p => IsPath p) p ∧ ∀ (y : Walk G v w), (fun p => IsPath p) y → y = p
⊢ Reachable G v w
[PROOFSTEP]
exact p.reachable
[GOAL]
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
⊢ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
[PROOFSTEP]
rintro v w ⟨p, hp⟩ ⟨q, hq⟩
[GOAL]
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, IsPath p
v w : V
p : Walk G v w
hp : IsPath p
q : Walk G v w
hq : IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
[PROOFSTEP]
simp only [ExistsUnique.unique (h v w) hp hq]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
have := hG.isConnected.nonempty
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
inhabit V
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
classical
have : Finset.card ({ default } : Finset V)ᶜ + 1 = Fintype.card V := by
  rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
rw [← this, add_left_inj]
choose f hf hf' using (hG.existsUnique_path · default)
refine Eq.symm <| Finset.card_congr (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj
case notNil => exact not_nil_of_ne (by simpa using hw)
case memEdges => simp
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h 
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3 
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h' 
    simp [le_zero_iff, Nat.one_ne_zero] at h' 
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h' 
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
have : Finset.card ({ default } : Finset V)ᶜ + 1 = Fintype.card V := by
  rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card {default}ᶜ + 1 = Fintype.card V
[PROOFSTEP]
rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
⊢ Finset.card (edgeFinset G) + 1 = Fintype.card V
[PROOFSTEP]
rw [← this, add_left_inj]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
⊢ Finset.card (edgeFinset G) = Finset.card {default}ᶜ
[PROOFSTEP]
choose f hf hf' using (hG.existsUnique_path · default)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ Finset.card (edgeFinset G) = Finset.card {default}ᶜ
[PROOFSTEP]
refine Eq.symm <| Finset.card_congr (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj
[GOAL]
case notNil
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
case memEdges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case notNil => exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
[PROOFSTEP]
case notNil => exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ ¬Nil (f w)
[PROOFSTEP]
exact not_nil_of_ne (by simpa using hw)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ w ≠ default
[PROOFSTEP]
simpa using hw
[GOAL]
case memEdges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case memEdges => simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
[PROOFSTEP]
case memEdges => simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha ∈ edgeFinset G
[PROOFSTEP]
simp
[GOAL]
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h 
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3 
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
[PROOFSTEP]
case inj =>
  intros a b ha hb h
  wlog h' : (f a).length ≤ (f b).length generalizing a b
  · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
  rw [dart_edge_eq_iff] at h 
  obtain (h | h) := h
  · exact (congrArg (·.fst) h)
  · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
    have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
    rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3 
    · exfalso
      linarith
    · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
      exact (hf _).tail _
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      a = b
[PROOFSTEP]
intros a b ha hb h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
⊢ a = b
[PROOFSTEP]
wlog h' : (f a).length ≤ (f b).length generalizing a b
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
this :
  ∀ (a b : V) (ha : a ∈ {default}ᶜ) (hb : b ∈ {default}ᶜ),
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
        (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb →
      length (f a) ≤ length (f b) → a = b
h' : ¬length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha =
    (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) b hb
h' : length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
rw [dart_edge_eq_iff] at h 
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h :
  firstDart (f a) (_ : ¬Nil (f a)) = firstDart (f b) (_ : ¬Nil (f b)) ∨
    firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h' : length (f a) ≤ length (f b)
⊢ a = b
[PROOFSTEP]
obtain (h | h) := h
[GOAL]
case inl
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = firstDart (f b) (_ : ¬Nil (f b))
⊢ a = b
[PROOFSTEP]
exact (congrArg (·.fst) h)
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
⊢ a = b
[PROOFSTEP]
have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b := congrArg (·.snd) h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
⊢ a ≠ default
[PROOFSTEP]
simpa using ha
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ a = b
[PROOFSTEP]
have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
[GOAL]
case inr.refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3 : length (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default)) = length (f b)
⊢ a = b
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ (fun p => IsPath p) (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default))
[PROOFSTEP]
rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3 
[GOAL]
case inr.refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3✝ : length (tail (f a) (_ : ¬Nil (f a))) = length (f b)
h3 : length (f a) = length (f b) + 1
⊢ a = b
[PROOFSTEP]
exfalso
[GOAL]
case inr.refine_2.h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
h3✝ : length (tail (f a) (_ : ¬Nil (f a))) = length (f b)
h3 : length (f a) = length (f b) + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ (fun p => IsPath p) (Walk.copy (tail (f a) (_ : ¬Nil (f a))) h1 (_ : default = default))
[PROOFSTEP]
simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
[GOAL]
case inr.refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
a b : V
ha : a ∈ {default}ᶜ
hb : b ∈ {default}ᶜ
h' : length (f a) ≤ length (f b)
h : firstDart (f a) (_ : ¬Nil (f a)) = Dart.symm (firstDart (f b) (_ : ¬Nil (f b)))
h1 : (firstDart (f a) (_ : ¬Nil (f a))).toProd.snd = b
⊢ IsPath (tail (f a) (_ : ¬Nil (f a)))
[PROOFSTEP]
exact (hf _).tail _
[GOAL]
case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h' 
    simp [le_zero_iff, Nat.one_ne_zero] at h' 
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h' 
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
case surj =>
  simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
  intros x y h
  wlog h' : (f x).length ≤ (f y).length generalizing x y
  · rw [Sym2.eq_swap]
    exact this y x h.symm (le_of_not_le h')
  refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
  · rintro rfl
    rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
      length_cons, length_nil] at h' 
    simp [le_zero_iff, Nat.one_ne_zero] at h' 
  rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
  rfl
  case contra =>
    suffices : (f x).takeUntil y hy = .cons h .nil
    · rw [← take_spec _ hy] at h' 
      simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
    refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
    simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (b : Sym2 V), b ∈ edgeFinset G → ∃ a ha, (fun w hw => Dart.edge (firstDart (f w) (_ : ¬Nil (f w)))) a ha = b
[PROOFSTEP]
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
⊢ ∀ (x y : V), Adj G x y → ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
intros x y h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
wlog h' : (f x).length ≤ (f y).length generalizing x y
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
this :
  ∀ (x y : V),
    Adj G x y →
      length (f x) ≤ length (f y) →
        ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
h' : ¬length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
this :
  ∀ (x y : V),
    Adj G x y →
      length (f x) ≤ length (f y) →
        ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
h' : ¬length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (y, x)
[PROOFSTEP]
exact this y x h.symm (le_of_not_le h')
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ ∃ a h, Dart.edge (firstDart (f a) (_ : ¬Nil (f a))) = Quotient.mk (Sym2.Rel.setoid V) (x, y)
[PROOFSTEP]
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ ¬y = default
[PROOFSTEP]
rintro rfl
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : length (f x) ≤ length (f default)
⊢ False
[PROOFSTEP]
rw [← hf' _ nil IsPath.nil, length_nil, ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne), length_cons,
  length_nil] at h' 
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : length (f x) ≤ 0
⊢ ¬x ∈ Walk.support nil
[PROOFSTEP]
simpa using h.ne
[GOAL]
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x : V
h : Adj G x default
h' : 0 + 1 ≤ 0
⊢ False
[PROOFSTEP]
simp [le_zero_iff, Nat.one_ne_zero] at h' 
[GOAL]
case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ (firstDart (f y) (_ : ¬Nil (f y))).toProd = Prod.swap (x, y)
[PROOFSTEP]
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
[GOAL]
case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
⊢ (firstDart (cons (_ : Adj G y x) (f x)) (_ : ¬Nil (cons (_ : Adj G y x) (f x)))).toProd = Prod.swap (x, y)
case contra
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case contra
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
case contra =>
  suffices : (f x).takeUntil y hy = .cons h .nil
  · rw [← take_spec _ hy] at h' 
    simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
  refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
  simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
case contra =>
  suffices : (f x).takeUntil y hy = .cons h .nil
  · rw [← take_spec _ hy] at h' 
    simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
  refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
  simp [h.ne]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ False
[PROOFSTEP]
suffices : (f x).takeUntil y hy = .cons h .nil
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
this : takeUntil (f x) y hy = cons h nil
⊢ False
[PROOFSTEP]
rw [← take_spec _ hy] at h' 
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
hy : y ∈ Walk.support (f x)
h' : length (append (takeUntil (f x) y hy) (dropUntil (f x) y hy)) ≤ length (f y)
this : takeUntil (f x) y hy = cons h nil
⊢ False
[PROOFSTEP]
simp [this, hf' _ _ ((hf _).dropUntil hy)] at h' 
[GOAL]
case this
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ takeUntil (f x) y hy = cons h nil
[PROOFSTEP]
refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
[GOAL]
case this
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑(edgeSet G)
hG : IsTree G
this✝ : Nonempty V
inhabited_h : Inhabited V
this : Finset.card {default}ᶜ + 1 = Fintype.card V
f : (x : V) → Walk G x default
hf : ∀ (x : V), (fun p => IsPath p) (f x)
hf' : ∀ (x : V) (y : Walk G x default), (fun p => IsPath p) y → y = f x
x y : V
h : Adj G x y
h' : length (f x) ≤ length (f y)
hy : y ∈ Walk.support (f x)
⊢ IsPath (cons h nil)
[PROOFSTEP]
simp [h.ne]
