no goals
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
classical simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one,
  Set.mem_inter_iff]
no goals
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one,
Set.mem_inter_iff]