R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (let x := e;
      if x ∈ incidenceSet G a then OfNat.ofNat 1 x else 0) =
      1 ↔
    e ∈ incidenceSet G a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ incidenceSet G a
unfold incMatrix Set.indicator
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 ↔ e ∈ incidenceSet G a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (let x := e;
      if x ∈ incidenceSet G a then OfNat.ofNat 1 x else 0) =
      1 ↔
    e ∈ incidenceSet G a
simp only [Pi.one_apply]
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : (if e ∈ incidenceSet G a then 1 else 0) = 1
⊢ e ∈ incidenceSet G a

case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : e ∈ incidenceSet G a
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 ↔ e ∈ incidenceSet G a
apply Iff.intro <;> intro h
no goals
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : (if e ∈ incidenceSet G a then 1 else 0) = 1
⊢ e ∈ incidenceSet G a
split at h <;> simp_all only [zero_ne_one]
no goals
case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : e ∈ incidenceSet G a
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1
simp_all only [ite_true]