-- 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:
case notNil
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}ᶜ
⊢ ¬(f w).Nil

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 notNil => exact not_nil_of_ne (by simpa using hw)

Result:
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

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
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), (fun w hw => ((f w).firstDart ⋯).edge) a ha = b

Tactic:
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]

Result:
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), G.Adj x y → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
inhabit V

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ G.edgeFinset.card + 1 = Fintype.card V

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 y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ¬y = default

Tactic:
rintro rfl

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 : V
h : G.Adj x default
h' : (f x).length ≤ (f default).length
⊢ False

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
hy : y ∈ (f x).support
⊢ False

Tactic:
suffices (f x).takeUntil y hy = .cons h .nil by
  rw [← take_spec _ hy] at h'
  simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'

Result:
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
hy : y ∈ (f x).support
⊢ (f x).takeUntil y hy = cons h nil

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}ᶜ) (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₂

Tactic:
intros a ha b hb h

Result:
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

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
have := hG.isConnected.nonempty

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
⊢ G.edgeFinset.card + 1 = Fintype.card V