[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = if e ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
unfold incMatrix Set.indicator
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (if e ∈ incidenceSet G a then OfNat.ofNat 1 e else 0) = if e ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
simp only [Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
[PROOFSTEP]
classical simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one, Set.mem_inter_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
[PROOFSTEP]
simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one, Set.mem_inter_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ incMatrix R G a e * incMatrix R G b e = 0
[PROOFSTEP]
rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_not_mem]
[GOAL]
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ incidenceSet G a ∩ incidenceSet G b
[PROOFSTEP]
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
[GOAL]
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ ∅
[PROOFSTEP]
exact Set.not_mem_empty e
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
h : ¬e ∈ incidenceSet G a
⊢ incMatrix R G a e = 0
[PROOFSTEP]
rw [incMatrix_apply, Set.indicator_of_not_mem h]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
h : e ∈ incidenceSet G a
⊢ incMatrix R G a e = 1
[PROOFSTEP]
rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 0 ↔ ¬e ∈ incidenceSet G a
[PROOFSTEP]
simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
unfold incMatrix Set.indicator
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then OfNat.ofNat 1 e else 0) = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
simp only [Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 → e ∈ incidenceSet G a
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ e ∈ incidenceSet G a → (if e ∈ incidenceSet G a then 1 else 0) = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : (if e ∈ incidenceSet G a then 1 else 0) = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
split at h 
[GOAL]
case mp.inl
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h✝ : e ∈ incidenceSet G a
h : 1 = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
simp_all only [zero_ne_one]
[GOAL]
case mp.inr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h✝ : ¬e ∈ incidenceSet G a
h : 0 = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
simp_all only [zero_ne_one]
[GOAL]
case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : e ∈ incidenceSet G a
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1
[PROOFSTEP]
simp_all only [ite_true]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ ∑ e : Sym2 α, incMatrix R G a e = ↑(degree G a)
[PROOFSTEP]
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(degree G a)
[PROOFSTEP]
rw [← sum_incMatrix_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e
[PROOFSTEP]
simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (∑ x : Sym2 α, if x ∈ incidenceSet G a then if x ∈ incidenceSet G a then 1 else 0 else 0) =
    ∑ x : Sym2 α, if x ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
simp_all only [ite_true, sum_boole]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
[PROOFSTEP]
refine' e.ind _
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [mem_edgeSet] at h 
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [← Nat.cast_two, ← card_doubleton h.ne]
[GOAL]
R : Type u_1
α : Type u_2
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})
[PROOFSTEP]
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
[GOAL]
R : Type u_1
α : Type u_2
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})
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_s
R : Type u_1
α : Type u_2
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}
[PROOFSTEP]
ext e
[GOAL]
case e_a.e_s.a
R : Type u_1
α : Type u_2
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}
[PROOFSTEP]
simp only [mem_filter, mem_univ, true_and_iff, mem_insert, mem_singleton]
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
classical
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul, sum_boole, and_self_iff]
split_ifs with h
· revert h
  refine' e.ind _
  intro v w h
  rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
  simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
  congr 2
  ext u
  simp
· revert h
  refine' e.ind _
  intro v w h
  simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul, sum_boole, and_self_iff]
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
revert h
[GOAL]
case pos
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' e.ind _
[GOAL]
case pos
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
intro v w h
[GOAL]
case pos
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
[GOAL]
case pos
R : Type u_1
α : Type u_2
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})
[PROOFSTEP]
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
[GOAL]
case pos
R : Type u_1
α : Type u_2
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})
[PROOFSTEP]
congr 2
[GOAL]
case pos.e_a.e_s
R : Type u_1
α : Type u_2
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}
[PROOFSTEP]
ext u
[GOAL]
case pos.e_a.e_s.a
R : Type u_1
α : Type u_2
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}
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
revert h
[GOAL]
case neg
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' e.ind _
[GOAL]
case neg
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
intro v w h
[GOAL]
case neg
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
[PROOFSTEP]
classical
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply, Set.indicator_apply,
  Pi.one_apply, sum_boole]
convert @Nat.cast_one R _
convert card_singleton ⟦(a, b)⟧
rw [← coe_eq_singleton, coe_filter_univ]
exact G.incidenceSet_inter_incidenceSet_of_adj h
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
[PROOFSTEP]
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply, Set.indicator_apply,
  Pi.one_apply, sum_boole]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ ↑(card (filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ)) = 1
[PROOFSTEP]
convert @Nat.cast_one R _
[GOAL]
case h.e'_2.h.e'_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ card (filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ) = 1
[PROOFSTEP]
convert card_singleton ⟦(a, b)⟧
[GOAL]
case h.e'_2.h.e'_2.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
e_1✝ : Sym2 α = Quotient (Rel.setoid α)
⊢ filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ = {Quotient.mk (Rel.setoid α) (a, b)}
[PROOFSTEP]
rw [← coe_eq_singleton, coe_filter_univ]
[GOAL]
case h.e'_2.h.e'_2.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
e_1✝ : Sym2 α = Quotient (Rel.setoid α)
⊢ {x | x ∈ incidenceSet G a ∩ incidenceSet G b} = {Quotient.mk (Rel.setoid α) (a, b)}
[PROOFSTEP]
exact G.incidenceSet_inter_incidenceSet_of_adj h
[GOAL]
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
ext a b
[GOAL]
case a.h
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
R : Type u_1
α : Type u_2
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)
[PROOFSTEP]
subst b
[GOAL]
case pos
R : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rename Semiring R => sr
[GOAL]
case pos
R : Type u_1
α : Type u_2
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)
[PROOFSTEP]
convert @incMatrix_mul_transpose_diag _ _ _ _ sr.toNonAssocSemiring _ _ _
[GOAL]
case pos
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact G.incMatrix_mul_transpose_apply_of_adj h'
[GOAL]
case neg
R : Type u_1
α : Type u_2
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
[PROOFSTEP]
simp only [Matrix.mul_apply, Matrix.transpose_apply, G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h',
  sum_const_zero]
