[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i : V
⊢ ¬A i i = 1
[PROOFSTEP]
simp [h.apply_diag i]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0
[PROOFSTEP]
obtain h | h := h.zero_or_one i j
[GOAL]
case inl
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
i j : V
h : A i j = 0
⊢ ¬A i j = 1 ↔ A i j = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
i j : V
h : A i j = 1
⊢ ¬A i j = 1 ↔ A i j = 0
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
⊢ ¬A i j = 0 ↔ A i j = 1
[PROOFSTEP]
rw [← apply_ne_one_iff h, Classical.not_not]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
hij : (fun i j => A i j = 1) i j
⊢ (fun i j => A i j = 1) j i
[PROOFSTEP]
simp only
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
hij : (fun i j => A i j = 1) i j
⊢ A j i = 1
[PROOFSTEP]
rwa [h.symm.apply i j]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i : V
⊢ ¬(fun i j => A i j = 1) i i
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
h : IsAdjMatrix A
⊢ DecidableRel (toGraph h).Adj
[PROOFSTEP]
simp only [toGraph]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
A : Matrix V V α
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
h : IsAdjMatrix A
⊢ DecidableRel fun i j => A i j = 1
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i : V
⊢ compl A i i = 0
[PROOFSTEP]
simp [compl]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ compl A i j = 0 ∨ compl A i j = 1
[PROOFSTEP]
unfold compl
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (if i = j then 0 else if A i j = 0 then 1 else 0) = 0 ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
h✝ : i = j
⊢ 0 = 0 ∨ 0 = 1
[PROOFSTEP]
simp
[GOAL]
case pos
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
h✝¹ : ¬i = j
h✝ : A i j = 0
⊢ 1 = 0 ∨ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case neg
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
h✝¹ : ¬i = j
h✝ : ¬A i j = 0
⊢ 0 = 0 ∨ 0 = 1
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
⊢ IsSymm (compl A)
[PROOFSTEP]
ext
[GOAL]
case a.h
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
i✝ x✝ : V
⊢ (compl A)ᵀ i✝ x✝ = compl A i✝ x✝
[PROOFSTEP]
simp [compl, h.apply, eq_comm]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
⊢ IsSymm (compl A)
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
⊢ toGraph (_ : IsAdjMatrix (Matrix.compl A)) = (toGraph h)ᶜ
[PROOFSTEP]
ext v w
[GOAL]
case Adj.h.h.a
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
v w : V
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h)ᶜ v w
[PROOFSTEP]
cases' h.zero_or_one v w with h h
[GOAL]
case Adj.h.h.a.inl
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 0
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
by_cases hvw : v = w
[GOAL]
case Adj.h.h.a.inr
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 1
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
by_cases hvw : v = w
[GOAL]
case pos
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 0
hvw : v = w
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
simp [Matrix.compl, h, hvw]
[GOAL]
case neg
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
simp [Matrix.compl, h, hvw]
[GOAL]
case pos
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 1
hvw : v = w
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
simp [Matrix.compl, h, hvw]
[GOAL]
case neg
V : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : IsAdjMatrix A
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph h✝)ᶜ v w
[PROOFSTEP]
simp [Matrix.compl, h, hvw]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G
[PROOFSTEP]
ext
[GOAL]
case a.h
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : V
⊢ (adjMatrix α G)ᵀ i✝ x✝ = adjMatrix α G i✝ x✝
[PROOFSTEP]
simp [adj_comm]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1
[PROOFSTEP]
by_cases G.Adj i j
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1
[PROOFSTEP]
by_cases G.Adj i j
[GOAL]
case pos
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i j : V
h : Adj G i j
⊢ adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1
[PROOFSTEP]
simp [h]
[GOAL]
case neg
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i j : V
h : ¬Adj G i j
⊢ adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ IsAdjMatrix.toGraph (_ : IsAdjMatrix (adjMatrix α G)) = G
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ Adj (IsAdjMatrix.toGraph (_ : IsAdjMatrix (adjMatrix α G))) x✝¹ x✝ ↔ Adj G x✝¹ x✝
[PROOFSTEP]
simp only [IsAdjMatrix.toGraph_Adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]
[GOAL]
case Adj.h.h.a
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬Adj G x✝¹ x✝ → False ↔ Adj G x✝¹ x✝
[PROOFSTEP]
apply Classical.not_not
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u in neighborFinset G v, vec u
[PROOFSTEP]
simp [neighborFinset_eq_filter, dotProduct, sum_filter]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vec ⬝ᵥ adjMatrix α G v = ∑ u in neighborFinset G v, vec u
[PROOFSTEP]
simp [neighborFinset_eq_filter, dotProduct, sum_filter, Finset.sum_apply]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ mulVec (adjMatrix α G) vec v = ∑ u in neighborFinset G v, vec u
[PROOFSTEP]
rw [mulVec, adjMatrix_dotProduct]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vecMul vec (adjMatrix α G) v = ∑ u in neighborFinset G v, vec u
[PROOFSTEP]
simp only [← dotProduct_adjMatrix, vecMul]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun i => adjMatrix α G i v) = (fun u => vec u) ⬝ᵥ adjMatrix α G v
[PROOFSTEP]
refine' congr rfl _
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i => adjMatrix α G i v) = adjMatrix α G v
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x
[PROOFSTEP]
rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (adjMatrix α G * M) v w = ∑ u in neighborFinset G v, M u w
[PROOFSTEP]
simp [mul_apply, neighborFinset_eq_filter, sum_filter]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (M * adjMatrix α G) v w = ∑ u in neighborFinset G w, M v u
[PROOFSTEP]
simp [mul_apply, neighborFinset_eq_filter, sum_filter, adj_comm]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : AddCommMonoid α
inst✝ : One α
⊢ trace (adjMatrix α G) = 0
[PROOFSTEP]
simp [Matrix.trace]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
i : V
⊢ (adjMatrix α G * adjMatrix α G) i i = ↑(degree G i)
[PROOFSTEP]
simp [degree]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : Semiring α
a : α
v : V
⊢ mulVec (adjMatrix α G) (Function.const V a) v = ↑(degree G v) * a
[PROOFSTEP]
simp [degree]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : Semiring α
d : ℕ
a : α
hd : IsRegularOfDegree G d
v : V
⊢ mulVec (adjMatrix α G) (Function.const V a) v = ↑d * a
[PROOFSTEP]
simp [hd v]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p | Walk.length p = n})
[PROOFSTEP]
rw [card_set_walk_length_eq]
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
[PROOFSTEP]
induction' n with n ih generalizing u v
[GOAL]
case zero
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ u v : V
⊢ (adjMatrix α G ^ Nat.zero) u v = ↑(card (finsetWalkLength G Nat.zero u v))
[PROOFSTEP]
obtain rfl | h := eq_or_ne u v
[GOAL]
case zero.inl
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v u : V
⊢ (adjMatrix α G ^ Nat.zero) u u = ↑(card (finsetWalkLength G Nat.zero u u))
[PROOFSTEP]
simp [finsetWalkLength, *]
[GOAL]
case zero.inr
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ u v : V
h : u ≠ v
⊢ (adjMatrix α G ^ Nat.zero) u v = ↑(card (finsetWalkLength G Nat.zero u v))
[PROOFSTEP]
simp [finsetWalkLength, *]
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ (adjMatrix α G ^ Nat.succ n) u v = ↑(card (finsetWalkLength G (Nat.succ n) u v))
[PROOFSTEP]
nth_rw 1 [Nat.succ_eq_one_add]
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ (adjMatrix α G ^ (1 + n)) u v = ↑(card (finsetWalkLength G (Nat.succ n) u v))
[PROOFSTEP]
simp only [pow_add, pow_one, finsetWalkLength, ih, adjMatrix_mul_apply]
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ ∑ x in neighborFinset G u, ↑(card (finsetWalkLength G n x v)) =
    ↑(card
        (Finset.biUnion univ fun w =>
          Finset.map
            { toFun := fun p => Walk.cons (_ : ↑w ∈ neighborSet G u) p,
              inj' :=
                (_ :
                  ∀ (x x_1 : Walk G (↑w) v),
                    Walk.cons (_ : ↑w ∈ neighborSet G u) x = Walk.cons (_ : ↑w ∈ neighborSet G u) x_1 → x = x_1) }
            (finsetWalkLength G n (↑w) v)))
[PROOFSTEP]
rw [Finset.card_biUnion]
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ ∑ x in neighborFinset G u, ↑(card (finsetWalkLength G n x v)) =
    ↑(∑ u_1 : ↑(neighborSet G u),
        card
          (Finset.map
            { toFun := fun p => Walk.cons (_ : ↑u_1 ∈ neighborSet G u) p,
              inj' :=
                (_ :
                  ∀ (x x_1 : Walk G (↑u_1) v),
                    Walk.cons (_ : ↑u_1 ∈ neighborSet G u) x = Walk.cons (_ : ↑u_1 ∈ neighborSet G u) x_1 → x = x_1) }
            (finsetWalkLength G n (↑u_1) v)))
[PROOFSTEP]
norm_cast
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ ↑(∑ x in neighborFinset G u, card (finsetWalkLength G n x v)) =
    ↑(∑ u_1 : ↑(neighborSet G u),
        card
          (Finset.map
            { toFun := fun p => Walk.cons (_ : ↑u_1 ∈ neighborSet G u) p,
              inj' :=
                (_ :
                  ∀ (x x_1 : Walk G (↑u_1) v),
                    Walk.cons (_ : ↑u_1 ∈ neighborSet G u) x = Walk.cons (_ : ↑u_1 ∈ neighborSet G u) x_1 → x = x_1) }
            (finsetWalkLength G n (↑u_1) v)))
[PROOFSTEP]
simp only [Nat.cast_sum, card_map, neighborFinset_def]
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ ∑ x in Set.toFinset (neighborSet G u), ↑(card (finsetWalkLength G n x v)) =
    ∑ x : ↑(neighborSet G u), ↑(card (finsetWalkLength G n (↑x) v))
[PROOFSTEP]
apply Finset.sum_toFinset_eq_subtype
[GOAL]
case succ
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v : V
⊢ ∀ (x : ↑(neighborSet G u)),
    x ∈ univ →
      ∀ (y : ↑(neighborSet G u)),
        y ∈ univ →
          x ≠ y →
            Disjoint
              (Finset.map
                { toFun := fun p => Walk.cons (_ : ↑x ∈ neighborSet G u) p,
                  inj' :=
                    (_ :
                      ∀ (x_1 x_2 : Walk G (↑x) v),
                        Walk.cons (_ : ↑x ∈ neighborSet G u) x_1 = Walk.cons (_ : ↑x ∈ neighborSet G u) x_2 →
                          x_1 = x_2) }
                (finsetWalkLength G n (↑x) v))
              (Finset.map
                { toFun := fun p => Walk.cons (_ : ↑y ∈ neighborSet G u) p,
                  inj' :=
                    (_ :
                      ∀ (x x_1 : Walk G (↑y) v),
                        Walk.cons (_ : ↑y ∈ neighborSet G u) x = Walk.cons (_ : ↑y ∈ neighborSet G u) x_1 → x = x_1) }
                (finsetWalkLength G n (↑y) v))
[PROOFSTEP]
rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
[GOAL]
case succ.mk.mk
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
y : V
hy : y ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := y, property := hy }
⊢ Disjoint
    (Finset.map
      { toFun := fun p => Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) p,
        inj' :=
          (_ :
            ∀ (x_1 x_2 : Walk G (↑{ val := x, property := hx }) v),
              Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_1 =
                  Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_2 →
                x_1 = x_2) }
      (finsetWalkLength G n (↑{ val := x, property := hx }) v))
    (Finset.map
      { toFun := fun p => Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) p,
        inj' :=
          (_ :
            ∀ (x x_1 : Walk G (↑{ val := y, property := hy }) v),
              Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x =
                  Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x_1 →
                x = x_1) }
      (finsetWalkLength G n (↑{ val := y, property := hy }) v))
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case succ.mk.mk
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
y : V
hy : y ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := y, property := hy }
⊢ Finset.map
        { toFun := fun p => Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) p,
          inj' :=
            (_ :
              ∀ (x_1 x_2 : Walk G (↑{ val := x, property := hx }) v),
                Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_1 =
                    Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_2 →
                  x_1 = x_2) }
        (finsetWalkLength G n (↑{ val := x, property := hx }) v) ⊓
      Finset.map
        { toFun := fun p => Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) p,
          inj' :=
            (_ :
              ∀ (x x_1 : Walk G (↑{ val := y, property := hy }) v),
                Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x =
                    Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x_1 →
                  x = x_1) }
        (finsetWalkLength G n (↑{ val := y, property := hy }) v) ≤
    ⊥
[PROOFSTEP]
intro p hp
[GOAL]
case succ.mk.mk
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
y : V
hy : y ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := y, property := hy }
p : Walk G u v
hp :
  p ∈
    Finset.map
        { toFun := fun p => Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) p,
          inj' :=
            (_ :
              ∀ (x_1 x_2 : Walk G (↑{ val := x, property := hx }) v),
                Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_1 =
                    Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) x_2 →
                  x_1 = x_2) }
        (finsetWalkLength G n (↑{ val := x, property := hx }) v) ⊓
      Finset.map
        { toFun := fun p => Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) p,
          inj' :=
            (_ :
              ∀ (x x_1 : Walk G (↑{ val := y, property := hy }) v),
                Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x =
                    Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) x_1 →
                  x = x_1) }
        (finsetWalkLength G n (↑{ val := y, property := hy }) v)
⊢ p ∈ ⊥
[PROOFSTEP]
simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk, exists_prop] at hp
[GOAL]
case succ.mk.mk
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
y : V
hy : y ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := y, property := hy }
p : Walk G u v
hp :
  (∃ a, a ∈ finsetWalkLength G n x v ∧ Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) a = p) ∧
    ∃ a, a ∈ finsetWalkLength G n y v ∧ Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) a = p
⊢ p ∈ ⊥
[PROOFSTEP]
obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
[GOAL]
case succ.mk.mk.intro.intro.intro.intro.intro
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
y : V
hy : y ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := y, property := hy }
px : Walk G x v
left✝ : px ∈ finsetWalkLength G n x v
py : Walk G y v
hpy : py ∈ finsetWalkLength G n y v
hp :
  Walk.cons (_ : ↑{ val := y, property := hy } ∈ neighborSet G u) py =
    Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) px
⊢ Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) px ∈ ⊥
[PROOFSTEP]
cases hp
[GOAL]
case succ.mk.mk.intro.intro.intro.intro.intro.refl
V : Type u_1
α : Type u_2
β : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(card (finsetWalkLength G n u v))
u v x : V
hx : x ∈ neighborSet G u
px : Walk G x v
left✝ : px ∈ finsetWalkLength G n x v
hy : x ∈ neighborSet G u
hxy : { val := x, property := hx } ≠ { val := x, property := hy }
hpy : px ∈ finsetWalkLength G n x v
⊢ Walk.cons (_ : ↑{ val := x, property := hx } ∈ neighborSet G u) px ∈ ⊥
[PROOFSTEP]
simp at hxy
[GOAL]
V : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
⊢ adjMatrix α (toGraph h) = A
[PROOFSTEP]
ext i j
[GOAL]
case a.h
V : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α (toGraph h) i j = A i j
[PROOFSTEP]
obtain h' | h' := h.zero_or_one i j
[GOAL]
case a.h.inl
V : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
i j : V
h' : A i j = 0
⊢ adjMatrix α (toGraph h) i j = A i j
[PROOFSTEP]
simp [h']
[GOAL]
case a.h.inr
V : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
i j : V
h' : A i j = 1
⊢ adjMatrix α (toGraph h) i j = A i j
[PROOFSTEP]
simp [h']