R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = if e ∈ edgeSet G then 2 else 0
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ((incMatrix R G)ᵀ ⬝ incMatrix R G) e e = if e ∈ edgeSet G then 2 else 0
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul,
  sum_boole, and_self_iff]
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2

case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : ¬e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = if e ∈ edgeSet G then 2 else 0
split_ifs with h
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2
revert h
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 2
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2
refine' e.ind _
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 2
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 2
intro v w h
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) =
    ↑(card {(v, w).fst, (v, w).snd})
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 2
rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => x = v ∨ x = w) univ)) = ↑(card {v, w})
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) =
    ↑(card {(v, w).fst, (v, w).snd})
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
case inl.e_a.e_s
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ filter (fun x => x = v ∨ x = w) univ = {v, w}
case inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => x = v ∨ x = w) univ)) = ↑(card {v, w})
congr 2
case inl.e_a.e_s.a
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
u : α
⊢ u ∈ filter (fun x => x = v ∨ x = w) univ ↔ u ∈ {v, w}
case inl.e_a.e_s
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ filter (fun x => x = v ∨ x = w) univ = {v, w}
ext u
no goals
case inl.e_a.e_s.a
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
u : α
⊢ u ∈ filter (fun x => x = v ∨ x = w) univ ↔ u ∈ {v, w}
simp
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ¬e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : ¬e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
revert h
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    ¬Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 0
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ¬e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
refine' e.ind _
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : ¬Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 0
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    ¬Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 0
intro v w h
no goals
case inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : ¬Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 0
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]