-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
    Finset.card G.edgeFinset + 1 = Fintype.card V

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩

Result:
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ¬y = default

case refine_2
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((f y).firstDart ⋯).toProd = (x, y).swap

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : 0 + 1 ≤ 0
⊢ False

Tactic:
simp [Nat.le_zero, Nat.one_ne_zero] at h'

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb
⊢ a = b

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

Result:
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb
this :
  ∀ (a : V) (ha : a ∈ {default}ᶜ) (b : V) (hb : b ∈ {default}ᶜ),
    (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb →
      (f a).length ≤ (f b).length → a = b
h' : ¬(f a).length ≤ (f b).length
⊢ a = b

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb
h' : (f a).length ≤ (f b).length
⊢ a = b

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ w ≠ default

Tactic:
simpa using hw

Result:
no goals

Proof state:
case inr
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb
this :
  ∀ (a : V) (ha : a ∈ {default}ᶜ) (b : V) (hb : b ∈ {default}ᶜ),
    (fun w hw => ((f w).firstDart ⋯).edge) a ha = (fun w hw => ((f w).firstDart ⋯).edge) b hb →
      (f a).length ≤ (f b).length → a = b
h' : ¬(f a).length ≤ (f b).length
⊢ a = b

Tactic:
exact Eq.symm (this _ hb _ ha h.symm (le_of_not_le h'))

Result:
no goals

Proof state:
case memEdges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ (fun w hw => ((f w).firstDart ⋯).edge) a ha ∈ G.edgeFinset

case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    (fun w hw => ((f w).firstDart ⋯).edge) a₁ ha₁ = (fun w hw => ((f w).firstDart ⋯).edge) a₂ ha₂ → a₁ = a₂

case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), (fun w hw => ((f w).firstDart ⋯).edge) a ha = b

Tactic:
case memEdges => simp

Result:
case inj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    (fun w hw => ((f w).firstDart ⋯).edge) a₁ ha₁ = (fun w hw => ((f w).firstDart ⋯).edge) a₂ ha₂ → a₁ = a₂

case surj
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p => p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p => p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), (fun w hw => ((f w).firstDart ⋯).edge) a ha = b