Theorem: Digraph.Walk.List.count_prod_eq (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ List.count e xs = List.count e xs
Tactic:
congr!
State after:
case h.e'_2
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ instBEqProd = instBEq

State before:
case h.e'_2
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ instBEqProd = instBEq
Tactic:
ext p q
State after:
case h.e'_2.beq.h.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e p q : V × V
⊢ (p == q) = (p == q)

State before:
case h.e'_2.beq.h.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e p q : V × V
⊢ (p == q) = (p == q)
Tactic:
cases p
State after:
case h.e'_2.beq.h.h.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e q : V × V
fst✝ snd✝ : V
⊢ ((fst✝, snd✝) == q) = ((fst✝, snd✝) == q)

State before:
case h.e'_2.beq.h.h.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e q : V × V
fst✝ snd✝ : V
⊢ ((fst✝, snd✝) == q) = ((fst✝, snd✝) == q)
Tactic:
cases q
State after:
case h.e'_2.beq.h.h.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
fst✝¹ snd✝¹ fst✝ snd✝ : V
⊢ ((fst✝¹, snd✝¹) == (fst✝, snd✝)) = ((fst✝¹, snd✝¹) == (fst✝, snd✝))

State before:
case h.e'_2.beq.h.h.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
fst✝¹ snd✝¹ fst✝ snd✝ : V
⊢ ((fst✝¹, snd✝¹) == (fst✝, snd✝)) = ((fst✝¹, snd✝¹) == (fst✝, snd✝))
Tactic:
simp [BEq.beq]
State after:
no goals