awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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.IsTree ↔ 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: 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
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges
have refine : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges), p.IsPath
Tactic: refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ (cons head tail).IsPath
have hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
Tactic: have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
⊢ (cons head tail).IsPath
have cons : u' ∉ tail.support
Tactic: refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ u' ∉ tail.support
have cons : ∀ (h' : tail.length = 0), u' ∉ tail.support
Tactic: rcases tail.length.eq_zero_or_pos with h' | h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w_1 : V
head : G.Adj u' v'
tail : G.Walk v' w_1
ih : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges), tail.IsPath
h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (Walk.cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) tail.edges
cons : ∀ (h' : tail.length = 0), u' ∉ tail.support
⊢ u' ∉ tail.support
have cons₁ : ∀ (h' : tail.length > 0), u' ∉ tail.support
Tactic: rcases tail.length.eq_zero_or_pos with h' | h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ False
have cons : (cons head (tail.takeUntil u' hh)).IsCycle
Tactic: apply hG <| cons head (tail.takeUntil u' hh)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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)).IsCycle
have cons : (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup
have this : (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]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have cons : s(u', v') ∉ (tail.takeUntil u' hh).edges
Tactic: refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have cons : s(u', v') ∈ tail.edges.head?
Tactic: refine hcc.1 s(u', v') ?_ rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ s(u', v') ∈ tail.edges.head?
have cons : s(u', v') ∈ (cons sorry tail.tail).edges.head?
Tactic: rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ s(u', v') ∈ (cons ⋯ tail.tail).edges.head?
have this₁ : u' = (tail.takeUntil u' hh).snd
Tactic: have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p.IsPath
have nil : ∀ {u : V} (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) (edges (G := G) (u := u) nil)),
  IsPath.{u_1} (V := V) (G := G) (u := u) nil
Tactic: 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]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p.IsPath
have 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) (cons head tail).edges), (cons head tail).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]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges
have refine : ∀ (h : List.IsChain (fun (x1 x2 : Sym2 V) ↦ x1 ≠ x2) p.edges), p.IsPath
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
⊢ G.edgeFinset.card + 1 = Fintype.card V
have this : Nonempty V
Tactic: have := hG.connected.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.edgeFinset.card + 1 = Fintype.card V
have inhabit : ∀ (inhabited_h : Inhabited V), G.edgeFinset.card + 1 = Fintype.card V
Tactic: inhabit V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have rw : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have rw₁ : Fintype.card V - 1 + 1 = Fintype.card V
Tactic: rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have rw₂ : Fintype.card V = Fintype.card V
Tactic: rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ G.edgeFinset.card + 1 = Fintype.card V
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.edgeFinset.card + 1 = Fintype.card V
have rw : G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
Tactic: rw [← this, add_left_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
have 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}ᶜ
Tactic: choose f hf hf' using (hG.existsUnique_path · default)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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}ᶜ
have refine : ∀ (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w), ¬(f w).Nil
Tactic: refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
have refine₁ : ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a),
  (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart sorry).edge) a ha ∈ G.edgeFinset
Tactic: refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
have 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 sorry).edge) a₁ ha₁)
      ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart sorry).edge) a₂ ha₂) →
    a₁ = a₂
Tactic: refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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₂
⊢ G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
have 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 sorry).edge) a ha = b
Tactic: refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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)
⊢ a = b
have 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 sorry).edge) a ha)
          ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart sorry).edge) b hb))
      (h' : (f a).length ≤ (f b).length), a = b)
  (h' : ¬(f a).length ≤ (f b).length), a = b
Tactic: wlog h' : (f a).length ≤ (f b).length generalizing a b