-- 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 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
x y : V
h : G.Adj x y
this :
  ∀ (x y : V), G.Adj x y → (f x).length ≤ (f y).length → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
rw [Sym2.eq_swap]

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
x y : V
h : G.Adj x y
this :
  ∀ (x y : V), G.Adj x y → (f x).length ≤ (f y).length → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(y, x)

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
⊢ (cons h nil).IsPath

Tactic:
simp [h.ne]

Result:
no goals

Proof state:
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

Tactic:
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]

Result:
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
⊢ ((cons ⋯ (f x)).firstDart ⋯).toProd = (x, y).swap

case contra
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

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

Tactic:
intros x y 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
⊢ ∃ 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
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' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ a ≠ default

Tactic:
simpa using ha

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
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
this : (f x).takeUntil y hy = cons h nil
⊢ False

Tactic:
rw [← take_spec _ 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
hy : y ∈ (f x).support
h' : (((f x).takeUntil y hy).append ((f x).dropUntil y hy)).length ≤ (f y).length
this : (f x).takeUntil y hy = cons h nil
⊢ 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
w : V
hw : w ∈ {default}ᶜ
⊢ ¬(f w).Nil

Tactic:
exact not_nil_of_ne (by simpa using hw)

Result:
no goals

Proof state:
case contra
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:
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]

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
⊢ {default}ᶜ.card + 1 = Fintype.card V

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

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

Tactic:
simpa using h.ne

Result:
no goals