V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = e) univ) = 2
refine' Sym2.ind (fun v w h => _) e h
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
let d : G.Dart := ⟨(v, w), h⟩
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ 2 = card {d, Dart.symm d}
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
convert congr_arg card d.edge_fiber
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d ∈ {Dart.symm d}
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ 2 = card {d, Dart.symm d}
rw [card_insert_of_not_mem, card_singleton]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d = Dart.symm d
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d ∈ {Dart.symm d}
rw [mem_singleton]
no goals
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d = Dart.symm d
exact d.symm_ne.symm