-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem dart_fst_fiber [DecidableEq V] (v : V) :
    ({d : G.Dart | d.fst = v} : Finset _) = univ.image (G.dartOfNeighborSet v)

Proof state:
case h.mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
rintro ⟨e, he, rfl⟩

Result:
case h.mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v e : V
he : e ∈ G.neighborSet v
⊢ (G.dartOfNeighborSet v ⟨e, he⟩).toProd.1 = v

Proof state:
case h.mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v e : V
he : e ∈ G.neighborSet v
⊢ (G.dartOfNeighborSet v ⟨e, he⟩).toProd.1 = v

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ G.dartOfNeighborSet d.toProd.1 ⟨d.toProd.2, ⋯⟩ = d

Tactic:
ext <;> rfl

Result:
no goals

Proof state:
case h.mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v → ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

Tactic:
rintro rfl

Result:
case h.mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ ∃ x, ∃ (h : x ∈ G.neighborSet d.toProd.1), G.dartOfNeighborSet d.toProd.1 ⟨x, h⟩ = d

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d ∈ filter (fun d => d.toProd.1 = v) univ ↔ d ∈ image (G.dartOfNeighborSet v) univ

Tactic:
simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ, exists_prop_of_true]

Result:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v ↔ ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v ↔ ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

Tactic:
constructor

Result:
case h.mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v → ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d

case h.mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
⊢ filter (fun d => d.toProd.1 = v) univ = image (G.dartOfNeighborSet v) univ

Tactic:
ext d

Result:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d ∈ filter (fun d => d.toProd.1 = v) univ ↔ d ∈ image (G.dartOfNeighborSet v) univ

Proof state:
case h.mp
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d : G.Dart
⊢ ∃ x, ∃ (h : x ∈ G.neighborSet d.toProd.1), G.dartOfNeighborSet d.toProd.1 ⟨x, h⟩ = d

Tactic:
exact ⟨_, d.adj, by ext <;> rfl⟩

Result:
no goals