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
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
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
⊢ ∀ 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
have case₂ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
  ∃ (a : V) (h : ¬a = default), ((f a).firstDart sorry).edge = s(x, y)
Tactic: case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
case₂ case₃ :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
⊢ ∀ 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
have refine_1 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ¬y = default
Tactic: case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
case₂ case₃ :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
refine_1 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ¬y = default
⊢ ∀ 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
have refine_2 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((f y).firstDart sorry).toProd = (y, x)
Tactic: case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
case₂ case₃ :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
refine_1 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ¬y = default
refine_2 refine_2₁ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((f y).firstDart ⋯).toProd = (y, x)
⊢ ∀ 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
have refine_2₂ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((cons sorry (f x)).firstDart sorry).toProd = (y, x)
Tactic: case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
case case₁ : ∀ (x y : V) (h : G.Adj x y), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
inr :
  ∀ (x y : V) (h : G.Adj x y)
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
case₂ case₃ :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
refine_1 : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ¬y = default
refine_2 refine_2₁ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((f y).firstDart ⋯).toProd = (y, x)
refine_2₂ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length), ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)
⊢ ∀ 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
have case₄ : ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length) (hy : y ∈ (f x).support), False
Tactic: case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
⊢ G.edgeFinset.card + 1 = Fintype.card V
have have : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
Tactic: 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_bij
          (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 =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge 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 (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
have : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
⊢ G.edgeFinset.card + 1 = Fintype.card V
have have₁ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card + 1 = Fintype.card V
Tactic: 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_bij
          (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 =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge 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 (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
have : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have₁ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card + 1 = Fintype.card V
have₂ : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have₃ have₄ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card + 1 = Fintype.card V
⊢ G.edgeFinset.card + 1 = Fintype.card V
have have₅ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
Tactic: 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_bij
          (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 =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge 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 (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- 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
have : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have₁ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card + 1 = Fintype.card V
have₂ : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
have₃ have₄ : ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card + 1 = Fintype.card V
have₅ :
  ∀ (this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V), G.edgeFinset.card = Finset.card (α := V) {default}ᶜ
⊢ G.edgeFinset.card + 1 = Fintype.card V
have have₆ : ∀ (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: 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_bij
          (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 =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge 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 (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro 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_ge 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 at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ G.IsTree
have rw : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
Tactic: rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Minimal Connected G
have refine : ∀ (htree : G.IsTree) (G' : SimpleGraph V) (h' : G'.Connected) (hle : G' ≤ G) (u v : V) (hadj : G.Adj u v), G'.Adj u v
Tactic: refine ⟨fun htree ↦ ⟨htree.connected, fun G' h' hle u v hadj ↦ ?_⟩, isTree_of_minimal_connected⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
⊢ G'.Adj u v
have have : ∀ (p : G'.Walk u v) (hp : p.IsPath), G'.Adj u v
Tactic: have ⟨p, hp⟩ := h'.exists_isPath u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
⊢ G'.Adj u v
have this : (↑(Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) (mapLe hle p) sorry) : G.Walk u v).edges =
  (↑(Path.singleton hadj) : G.Walk u v).edges
Tactic: have := congrArg Walk.edges <| congrArg Subtype.val <|
    htree.isAcyclic.path_unique ⟨p.mapLe hle, hp.mapLe hle⟩ <| Path.singleton hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this :
  (↑(Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) (mapLe hle p) ⋯) : G.Walk u v).edges =
    (↑(Path.singleton hadj) : G.Walk u v).edges
⊢ G'.Adj u v
have this₁ : p.edges = (↑(Path.singleton hadj) : G.Walk u v).edges
Tactic: simp only [edges_map, Hom.coe_ofLE, Sym2.map_id, List.map_id_fun, id_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
have pos : ∀ (huv : u = v), (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Tactic: by_cases huv : u = v