awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h' : tail.length > 0
cons : ∀ (hh : u' ∈ tail.support), False
⊢ u' ∉ tail.support

Tactic:
by_contra hh
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
cons : (Walk.cons head (tail.takeUntil u' hh)).IsCycle
⊢ False

Tactic:
apply hG <| cons head (tail.takeUntil u' hh)

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.takeUntil
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
cons :
  (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup
⊢ (Walk.cons head (tail.takeUntil u' hh)).IsCycle

Tactic:
simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
        not_false_eq_true, support_cons, List.tail_cons, true_and]

Premises used: reduceCtorEq, SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.support_cons, SimpleGraph.Walk.isTrail_def, List.tail_cons, ne_eq, List.nodup_cons, SimpleGraph.Walk.edges_cons, not_false_eq_true, true_and
-- 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
hh : u' ∈ tail.support
⊢ [] ++ (cons head (tail.takeUntil u' hh)).support.tail ++ (tail.dropUntil u' hh).support.tail = tail.support

Tactic:
simp [← support_append]

Premises used: SimpleGraph.Walk.support_append
-- 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
hh : u' ∈ tail.support
⊢ (cons head (tail.takeUntil u' hh)).support.tail.Nodup

Tactic:
have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
-- 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
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
⊢ (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup

Tactic:
⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩

Premises used: SimpleGraph.Walk.edges_nodup_of_support_nodup, And.intro
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
this : (Walk.cons head (tail.takeUntil u' hh)).support.tail.Nodup
cons : s(u', v') ∉ (tail.takeUntil u' hh).edges
⊢ (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup

Tactic:
refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
this : (Walk.cons head (tail.takeUntil u' hh)).support.tail.Nodup
cons : ∀ (hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges), False
⊢ s(u', v') ∉ (tail.takeUntil u' hh).edges

Tactic:
by_contra hhh
-- 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
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ False

Tactic:
hcc.1 s(u', v') ?_ rfl

Premises used: Sym2.mk, And.left, rfl
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
this : (Walk.cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
cons : s(u', v') ∈ tail.edges.head?
⊢ False

Tactic:
refine hcc.1 s(u', v') ?_ rfl

Premises used: Sym2.mk, And.left, rfl
-- 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
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ ¬tail.Nil

Tactic:
simp [not_nil_iff_lt_length, h']

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length
-- 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
h' : tail.length > 0
hh : u' ∈ tail.support
this : (Walk.cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
cons : s(u', v') ∈ (Walk.cons ⋯ tail.tail).edges.head?
⊢ s(u', v') ∈ tail.edges.head?

Tactic:
rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]

Premises used: SimpleGraph.Walk.cons_tail_eq
-- 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
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ u' = (tail.takeUntil u' hh).snd

Tactic:
have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
-- 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
hh : u' ∈ tail.support
this_1 : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
this : u' = (tail.takeUntil u' hh).snd
⊢ s(u', v') ∈ (cons ⋯ tail.tail).edges.head?

Tactic:
simp [this, snd_takeUntil head.ne]

Premises used: SimpleGraph.Walk.snd_takeUntil, SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges
nil :
  ∀ {u : V} (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (edges (G := G) (u := u) Walk.nil)),
    IsPath.{u_1} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u' v' w : V} (head : G.Adj u' v') (tail : G.Walk v' w)
    (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), (Walk.cons head tail).IsPath
⊢ p.IsPath

Tactic:
induction p with
  | nil => simp
  | @cons u' v' _ head tail ih =>
    have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
    refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
    rcases tail.length.eq_zero_or_pos with h' | h'
    · simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]
    · by_contra hh
      apply hG <| cons head (tail.takeUntil u' hh)
      simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
        not_false_eq_true, support_cons, List.tail_cons, true_and]
      have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
      refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
      by_contra hhh
      refine hcc.1 s(u', v') ?_ rfl
      rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
      have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
      simp [this, snd_takeUntil head.ne]

Premises used: reduceCtorEq, SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.support_cons, SimpleGraph.Walk.isTrail_def, List.tail_cons, ne_eq, List.nodup_cons, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.tail, not_false_eq_true, true_and
-- 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:
classical
  refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
  induction p with
  | nil => simp
  | @cons u' v' _ head tail ih =>
    have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
    refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
    rcases tail.length.eq_zero_or_pos with h' | h'
    · simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]
    · by_contra hh
      apply hG <| cons head (tail.takeUntil u' hh)
      simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
        not_false_eq_true, support_cons, List.tail_cons, true_and]
      have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
      refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
      by_contra hhh
      refine hcc.1 s(u', v') ?_ rfl
      rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
      have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
      simp [this, snd_takeUntil head.ne]

Premises used: reduceCtorEq, SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.support_cons, SimpleGraph.Walk.isTrail_def, List.tail_cons, ne_eq, List.nodup_cons, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.tail, not_false_eq_true, true_and
-- 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 ↔ p.IsTrail

Tactic:
⟨IsPath.isTrail, fun h ↦ hG.isPath_iff_isChain p |>.mpr <| p.isTrail_def.mp h |>.isChain⟩

Premises used: Iff.mpr, SimpleGraph.Walk.IsPath.isTrail, SimpleGraph.IsAcyclic.isPath_iff_isChain, SimpleGraph.Walk.isTrail_def, Iff.intro, Iff.mp, List.Pairwise.isChain
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
⊢ Nonempty V

Tactic:
have := hG.connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this : Nonempty V
inhabit : ∀ (inhabited_h : Inhabited V), G.edgeFinset.card + 1 = Fintype.card V
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
inhabit V
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
rw : Fintype.card V - Finset.card (α := V) {default} + 1 = Fintype.card V
rw₁ : Fintype.card V - 1 + 1 = Fintype.card V
rw₂ rw₃ : Fintype.card V = Fintype.card V
⊢ Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V

Tactic:
rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]

Premises used: Finset.card_compl, Nat.sub_add_cancel, Fintype.card_pos, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V

Tactic:
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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
rw : G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
rw [← this, add_left_inj]

Premises used: add_left_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
choose :
  ∀ (f : (x : V) → G.Walk x default) (hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x))
    (hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x),
    G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ

Tactic:
choose f hf hf' using (hG.existsUnique_path · default)

Premises used: Inhabited.default, SimpleGraph.IsTree.existsUnique_path
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ

Tactic:
Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj

Premises used: Finset.card_bij, SimpleGraph.Dart.edge, SimpleGraph.Walk.firstDart, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
refine : ∀ (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w), ¬(f w).Nil
refine₁ :
  ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a),
    (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha ∈ G.edgeFinset
refine₂ :
  ∀ (a₁ : V) (ha₁ : Membership.mem (γ := Finset V) {default}ᶜ a₁) (a₂ : V)
    (ha₂ : Membership.mem (γ := Finset V) {default}ᶜ a₂),
    Eq.{u_1 + 1} (α := Sym2 V)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a₁ ha₁)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a₂ ha₂) →
      a₁ = a₂
refine₃ :
  ∀ b ∈ G.edgeFinset,
    ∃ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a),
      (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha = b
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ

Tactic:
refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj

Premises used: Finset.card_bij, SimpleGraph.Dart.edge, SimpleGraph.Walk.firstDart, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
w : V
hw : Membership.mem (γ := Finset V) {default}ᶜ w
⊢ w ≠ default

Tactic:
simpa using hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
w : V
hw : Membership.mem (γ := Finset V) {default}ᶜ w
⊢ ¬(f w).Nil

Tactic:
exact not_nil_of_ne (by simpa using hw)

Premises used: SimpleGraph.Walk.not_nil_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
w : V
hw : Membership.mem (γ := Finset V) {default}ᶜ w
⊢ ¬(f w).Nil

Tactic:
case notNil => exact not_nil_of_ne (by simpa using hw)

Premises used: SimpleGraph.Walk.not_nil_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
⊢ (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha ∈ G.edgeFinset

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
⊢ (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha ∈ G.edgeFinset

Tactic:
case memEdges => simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h :
  Eq.{u_1 + 1} (α := Sym2 V)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb)
inr :
  ∀
    (this :
      ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a) (b : V)
        (hb : Membership.mem (γ := Finset V) {default}ᶜ b)
        (h :
          Eq.{u_1 + 1} (α := Sym2 V)
            ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
            ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb))
        (h' : (f a).length ≤ (f b).length), a = b)
    (h' : ¬(f a).length ≤ (f b).length), a = b
wlog :
  ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a) (b : V)
    (hb : Membership.mem (γ := Finset V) {default}ᶜ b)
    (h :
      Eq.{u_1 + 1} (α := Sym2 V)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb))
    (h' : (f a).length ≤ (f b).length), a = b
⊢ a = b

Tactic:
wlog h' : (f a).length ≤ (f b).length generalizing a b

Premises used: SimpleGraph.Walk.length