-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_transpose_mul_diag [Fintype α] [Decidable (e ∈ G.edgeSet)] :
    ((G.incMatrix R)ᵀ * G.incMatrix R) e e = if e ∈ G.edgeSet then 2 else 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = if e ∈ G.edgeSet then 2 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 2

case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0

Tactic:
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul,
  sum_boole, and_self_iff]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = if e ∈ G.edgeSet then 2 else 0

Proof state:
case pos.e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ filter (fun x => x = v ∨ x = w) univ = {v, w}

Tactic:
ext u

Result:
case pos.e_a.e_s.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
u : α
⊢ u ∈ filter (fun x => x = v ∨ x = w) univ ↔ u ∈ {v, w}

Proof state:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∉ G.edgeSet → ↑(#(filter (fun x_1 => s(x, y) ∈ G.incidenceSet x_1) univ)) = 0

Tactic:
intro v w h

Result:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∉ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = 0

Proof state:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∉ G.edgeSet → ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 0

Tactic:
refine e.ind ?_

Result:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∉ G.edgeSet → ↑(#(filter (fun x_1 => s(x, y) ∈ G.incidenceSet x_1) univ)) = 0

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∈ G.edgeSet → ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 2

Tactic:
refine e.ind ?_

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ↑(#(filter (fun x_1 => s(x, y) ∈ G.incidenceSet x_1) univ)) = 2

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => x = v ∨ x = w) univ)) = ↑(#{v, w})

Tactic:
congr 2

Result:
case pos.e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ filter (fun x => x = v ∨ x = w) univ = {v, w}

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = 2

Tactic:
rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = ↑(#{(v, w).1, (v, w).2})

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ↑(#(filter (fun x_1 => s(x, y) ∈ G.incidenceSet x_1) univ)) = 2

Tactic:
intro v w h

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = 2

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = ↑(#{(v, w).1, (v, w).2})

Tactic:
simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and, mem_univ, forall_true_left,
  forall_eq_or_imp, forall_eq, and_self, mem_singleton, ne_eq]

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#(filter (fun x => x = v ∨ x = w) univ)) = ↑(#{v, w})

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 2

Tactic:
revert h

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∈ G.edgeSet → ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 2

Proof state:
case pos.e_a.e_s.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
u : α
⊢ u ∈ filter (fun x => x = v ∨ x = w) univ ↔ u ∈ {v, w}

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 0

Tactic:
revert h

Result:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∉ G.edgeSet → ↑(#(filter (fun x => e ∈ G.incidenceSet x) univ)) = 0

Proof state:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∉ G.edgeSet
⊢ ↑(#(filter (fun x => s(v, w) ∈ G.incidenceSet x) univ)) = 0

Tactic:
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]

Result:
no goals