R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (let x := e;
    if x ∈ incidenceSet G a then OfNat.ofNat 1 x else 0) =
    if e ∈ incidenceSet G a then 1 else 0
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = if e ∈ incidenceSet G a then 1 else 0
unfold incMatrix Set.indicator
no goals
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (let x := e;
    if x ∈ incidenceSet G a then OfNat.ofNat 1 x else 0) =
    if e ∈ incidenceSet G a then 1 else 0
simp only [Pi.one_apply]