case a.h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = if a = b then ↑(degree G a) else if Adj G a b then 1 else 0
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ incMatrix R G ⬝ (incMatrix R G)ᵀ = fun a b => if a = b then ↑(degree G a) else if Adj G a b then 1 else 0
ext (a b)
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : a = b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = ↑(degree G a)

case a.h.inr.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : Adj G a b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = 1

case a.h.inr.inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : ¬Adj G a b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = 0
case a.h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = if a = b then ↑(degree G a) else if Adj G a b then 1 else 0
split_ifs with h h'
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a a = ↑(degree G a)
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : a = b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = ↑(degree G a)
subst b
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
sr : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a a = ↑(degree G a)
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a a = ↑(degree G a)
rename Semiring R => sr
no goals
case a.h.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
sr : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a a = ↑(degree G a)
convert @incMatrix_mul_transpose_diag _ _ _ _ sr.toNonAssocSemiring _ _ _
no goals
case a.h.inr.inl
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : Adj G a b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = 1
exact G.incMatrix_mul_transpose_apply_of_adj h'
no goals
case a.h.inr.inr
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : ¬Adj G a b
⊢ (incMatrix R G ⬝ (incMatrix R G)ᵀ) a b = 0
simp only [Matrix.mul_apply, Matrix.transpose_apply,
  G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h', sum_const_zero]