awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ cons ph p = q
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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.edges ∨ s(u, v_1) ∈ p.edges
⊢ cons ph p = q
have cons : ∀ (h : s(u, v_1) ∈ q.edges), cons ph p = q
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Walk.cons ph p = q
have cons₁ : ∀ (h : s(u, v_1) ∈ p.edges), Walk.cons ph p = q
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
v_2 : V
h_1 : G.Adj u v_2
q : G.Walk v_2 w_1
hq : (cons h_1 q).IsPath
h : s(u, v_1) ∈ (cons h_1 q).edges
⊢ cons ph p = cons h_1 q
have 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) ∈ (cons h q).edges), cons ph p = cons h q
Tactic: rw [Walk.cons_isPath_iff] at hp hq
Cleared hypotheses: hp, v_2, h_1, q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ cons ph p = cons h_1 q
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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 ph p = cons h_1 q
have cons : ∀ (h : G.Adj u v_1) (q : G.Walk v_1 w_1) (hq : q.IsPath ∧ u ∉ q.support), cons ph p = cons h q
Tactic: rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
Cleared hypotheses: v_2, h_1, q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Walk.cons ph p = Walk.cons h_1 q
have 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
Tactic: rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
Cleared hypotheses: u, ph, hp, v_2, h_1, q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Walk.cons ph p = Walk.cons h_1 q
have cons₂ : ∀ (h : s(u, v_1) ∈ q.edges), Walk.cons ph p = Walk.cons h_1 q
Tactic: rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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 ph p = cons h q
have cons : ∀ (hq : p.IsPath ∧ u ∉ p.support), cons ph p = cons h p
Tactic: cases ih hp.1 q hq.1
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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.edges
⊢ cons ph p = q
have cons : ∀ (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: 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
Cleared hypotheses: w_1, p, ih, hp, q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Walk.cons ph p = q
have 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
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
Cleared hypotheses: q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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) ∈ p.edges
⊢ cons ph p = q
have cons : ∀ (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: rw [Walk.cons_isPath_iff] at hp
Cleared hypotheses: hp, q, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p = q
have nil : ∀ {u : V} (hp : IsPath.{u_1} (V := V) (G := G) (u := u) nil) (q : G.Walk u u) (hq : q.IsPath), nil = 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
Cleared hypotheses: p, hp, q, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p = q
have 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 : (cons ph p).IsPath) (q : G.Walk u w) (hq : q.IsPath), cons ph 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
Cleared hypotheses: p, hp, q, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ False
have hc₁ : c.IsTrail ∧ ¬c = nil ∧ c.support.tail.Nodup
Tactic: simp only [Walk.isCycle_def, Ne] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ False
have hc₁ : (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
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ False
have h₁ : Subtype.mk (p := fun (p : G.Walk v_1 v) ↦ p.IsPath) c' sorry = Path.singleton sorry
Tactic: specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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 ⋯
⊢ False
have h₁ : c' = cons sorry nil
Tactic: rw [Path.singleton, Subtype.mk.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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 = nil ∧ c.support.tail.Nodup
⊢ False
have nil : ∀
  (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 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
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ False
have cons : ∀ {v_1 : V} (ha : G.Adj v v_1) (c' : G.Walk v_1 v)
  (hc : (cons ha c').IsTrail ∧ ¬cons ha c' = Walk.nil ∧ (cons ha c').support.tail.Nodup), 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
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ w = p.snd
have this : Subtype.mk (p := fun (p : G.Walk u w) ↦ p.IsPath) (p.takeUntil w hsupp) sorry = Path.singleton hadj
Tactic: have := isAcyclic_iff_path_unique.mp h ⟨_, hp.takeUntil hsupp⟩ <| .singleton hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ w = p.snd
have have : ∀ (this : Subtype.mk (p := fun (p : G.Walk u w) ↦ p.IsPath) (p.takeUntil w hsupp) sorry = Path.singleton hadj), 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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.penultimate
have rw : w = p.reverse.snd
Tactic: rw [← snd_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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.snd
have apply : w ∈ p.reverse.support
Tactic: apply h.eq_snd_of_adj_start hp.reverse hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have rw : w ∈ (q.concat sorry).support
Tactic: rw [Subtype.mk.inj <| isAcyclic_iff_path_unique.mp hG ⟨p, hp⟩ ⟨_, hq.concat hv hadj.symm⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ v ∉ q.support
have 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
Tactic: obtain ⟨p₀, p₁, hp₀, hp₁, happend⟩ := hp.mem_support_iff_exists_append.mp hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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 ∉ q.support
have rw : v ∉ p₀.support
Tactic: rw [← Subtype.mk.inj <| hG.path_unique ⟨p₀, hp₀⟩ ⟨q, hq⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ q = p.concat hadj
have hw : w ∉ p.support
Tactic: have hw : w ∉ p.support := hG.ne_mem_support_of_support_of_adj_of_isPath hq hp hadj.symm hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
have 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
Tactic: rw [isTree_iff, isAcyclic_iff_path_unique]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have mp : ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
Tactic: refine ⟨hc.nonempty, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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, p.IsPath
have 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)
Tactic: use q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ (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)
have h : ∀ (y : G.Walk v w), y.IsPath → y = (↑q : G.Walk v w)
Tactic: simp only [true_and, Path.isPath]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ p = (↑q : G.Walk v w)
have hu₁ : Subtype.mk (p := fun (p : G.Walk v w) ↦ p.IsPath) p hp = q
Tactic: specialize hu ⟨p, hp⟩ q
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have mpr : G.Preconnected
Tactic: refine ⟨Connected.mk ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
have mpr₁ : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
Tactic: refine ⟨Connected.mk ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.Reachable v w
have 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
Tactic: obtain ⟨p, _⟩ := h v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
have rw : G.Connected ∧ G.IsAcyclic ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
have 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
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]