-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.length_le_card_edgeFinset [Fintype G.edgeSet] {u v : V}
    {w : G.Walk u v} (h : w.IsTrail) : w.length ≤ G.edgeFinset.card

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeSet

Tactic:
apply w.edges_subset_edgeSet

Result:
case a
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ w.edges

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges.card ≤ G.edgeFinset.card

Tactic:
have : edges ⊆ G.edgeFinset := by
  intro e h
  refine mem_edgeFinset.mpr ?_
  apply w.edges_subset_edgeSet
  simpa [edges] using h

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this✝ : edges.card = w.length
this : edges ⊆ G.edgeFinset
⊢ edges.card ≤ G.edgeFinset.card

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
⊢ w.length ≤ G.edgeFinset.card

Tactic:
let edges := w.edges.toFinset

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
⊢ w.length ≤ G.edgeFinset.card

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ w.length ≤ G.edgeFinset.card

Tactic:
rw [← this]

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges.card ≤ G.edgeFinset.card

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this✝ : edges.card = w.length
this : edges ⊆ G.edgeFinset
⊢ edges.card ≤ G.edgeFinset.card

Tactic:
exact Finset.card_le_card this

Result:
no goals

Proof state:
case a
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ w.edges

Tactic:
simpa [edges] using h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges ⊆ G.edgeFinset

Tactic:
intro e h

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
⊢ w.length ≤ G.edgeFinset.card

Tactic:
classical
let edges := w.edges.toFinset
have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
rw [← this]
have : edges ⊆ G.edgeFinset := by
  intro e h
  refine mem_edgeFinset.mpr ?_
  apply w.edges_subset_edgeSet
  simpa [edges] using h
exact Finset.card_le_card this

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset

Tactic:
refine mem_edgeFinset.mpr ?_

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
⊢ w.length ≤ G.edgeFinset.card

Tactic:
have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ w.length ≤ G.edgeFinset.card