no goals
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
classical
  refine' e.ind _
  intro a b h
  rw [mem_edgeSet] at h
  rw [← Nat.cast_two, ← card_doubleton h.ne]
  simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
  congr 2
  ext e
  simp only [mem_filter, mem_univ, true_and_iff, mem_insert, mem_singleton]
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G → ∑ a : α, incMatrix R G a (Quotient.mk (Rel.setoid α) (x, y)) = 2
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
refine' e.ind _
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) ∈ edgeSet G
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G → ∑ a : α, incMatrix R G a (Quotient.mk (Rel.setoid α) (x, y)) = 2
intro a b h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) ∈ edgeSet G
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
rw [mem_edgeSet] at h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = ↑(card {a, b})
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
rw [← Nat.cast_two, ← card_doubleton h.ne]
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ↑(card (filter (fun x => x = a ∨ x = b) univ)) = ↑(card {a, b})
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = ↑(card {a, b})
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
case e_a.e_s
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ filter (fun x => x = a ∨ x = b) univ = {a, b}
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ↑(card (filter (fun x => x = a ∨ x = b) univ)) = ↑(card {a, b})
congr 2
case e_a.e_s.a
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e✝ : Sym2 α
a b : α
h : Adj G a b
e : α
⊢ e ∈ filter (fun x => x = a ∨ x = b) univ ↔ e ∈ {a, b}
case e_a.e_s
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ filter (fun x => x = a ∨ x = b) univ = {a, b}
ext e
no goals
case e_a.e_s.a
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e✝ : Sym2 α
a b : α
h : Adj G a b
e : α
⊢ e ∈ filter (fun x => x = a ∨ x = b) univ ↔ e ∈ {a, b}
simp only [mem_filter, mem_univ, true_and_iff, mem_insert, mem_singleton]