no goals
R : Type u_2
α : Type u_1
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
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
R : Type u_2
α : Type u_1
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
R : Type u_2
α : Type u_1
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
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
  Set.indicator_apply, Pi.one_apply, sum_boole]
case h.e'_2.h.e'_3
R : Type u_2
α : Type u_1
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
R : Type u_2
α : Type u_1
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
convert @Nat.cast_one R _
case h.e'_2.h.e'_2.h
R : Type u_2
α : Type u_1
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)}
case h.e'_2.h.e'_3
R : Type u_2
α : Type u_1
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
convert card_singleton ⟦(a, b)⟧
case h.e'_2.h.e'_2.h
R : Type u_2
α : Type u_1
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)}
case h.e'_2.h.e'_2.h
R : Type u_2
α : Type u_1
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)}
rw [← coe_eq_singleton, coe_filter_univ]
no goals
case h.e'_2.h.e'_2.h
R : Type u_2
α : Type u_1
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)}
exact G.incidenceSet_inter_incidenceSet_of_adj h