-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem sum_incMatrix_apply_of_mem_edgeSet [Fintype α] :
    e ∈ G.edgeSet → ∑ a, G.incMatrix R a e = 2

Proof state:
case e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ filter (fun x => True ∧ (x = a ∨ x = b)) univ = {a, b}

Tactic:
ext e

Result:
case e_a.e_s.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e✝ : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
e : α
⊢ e ∈ filter (fun x => True ∧ (x = a ∨ x = b)) univ ↔ e ∈ {a, b}

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ∑ a : α, incMatrix R G a s(x, y) = 2

Tactic:
intro a b h

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : s(a, b) ∈ G.edgeSet
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = 2

Proof state:
case e_a.e_s.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e✝ : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
e : α
⊢ e ∈ filter (fun x => True ∧ (x = a ∨ x = b)) univ ↔ e ∈ {a, b}

Tactic:
simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : s(a, b) ∈ G.edgeSet
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = 2

Tactic:
rw [mem_edgeSet] at h

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = 2

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
⊢ e ∈ G.edgeSet → ∑ a : α, incMatrix R G a e = 2

Tactic:
refine e.ind ?_

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ∑ a : α, incMatrix R G a s(x, y) = 2

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ↑(#(filter (fun x => True ∧ (x = a ∨ x = b)) univ)) = ↑(#{a, b})

Tactic:
congr 2

Result:
case e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ filter (fun x => True ∧ (x = a ∨ x = b)) univ = {a, b}

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = 2

Tactic:
rw [← Nat.cast_two, ← card_pair h.ne]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = ↑(#{a, b})

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
⊢ e ∈ G.edgeSet → ∑ a : α, incMatrix R G a e = 2

Tactic:
classical
  refine e.ind ?_
  intro a b h
  rw [mem_edgeSet] at h
  rw [← Nat.cast_two, ← card_pair h.ne]
  simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]
  congr 2
  ext e
  simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1 : α, incMatrix R G a_1 s(a, b) = ↑(#{a, b})

Tactic:
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : NonAssocSemiring R
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ↑(#(filter (fun x => True ∧ (x = a ∨ x = b)) univ)) = ↑(#{a, b})