-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_pow_apply_eq_card_walk [DecidableEq V] [Semiring α] (n : ℕ) (u v : V) :
    (G.adjMatrix α ^ n) u v = Fintype.card { p : G.Walk u v | p.length = n }

Proof state:
case succ.mk.mk
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ Disjoint (Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨x, hx⟩) v))
    (Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨y, hy⟩) v))

Tactic:
rw [disjoint_iff_inf_le]

Result:
case succ.mk.mk
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨x, hx⟩) v) ⊓
      Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨y, hy⟩) v) ≤
    ⊥

Proof state:
case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(#(univ.biUnion fun w => Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)))

Tactic:
rw [Finset.card_biUnion]

Result:
case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(∑ u_1 : ↑(G.neighborSet u),
        #(Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∀ x ∈ univ,
    ∀ y ∈ univ,
      x ≠ y →
        Disjoint (Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑x) v))
          (Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑y) v))

Proof state:
case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ (G.neighborSet u).toFinset, ↑(#(G.finsetWalkLength n x v)) =
    ∑ x : ↑(G.neighborSet u), ↑(#(G.finsetWalkLength n (↑x) v))

Tactic:
apply Finset.sum_toFinset_eq_subtype

Result:
no goals

Proof state:
case succ.mk.mk.intro.intro.intro.intro.intro
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
px : G.Walk x v
left✝ : px ∈ G.finsetWalkLength n x v
py : G.Walk y v
hpy : py ∈ G.finsetWalkLength n y v
hp : Walk.cons ⋯ py = Walk.cons ⋯ px
⊢ Walk.cons ⋯ px ∈ ⊥

Tactic:
cases hp

Result:
case succ.mk.mk.intro.intro.intro.intro.intro.refl
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
px : G.Walk x v
left✝ : px ∈ G.finsetWalkLength n x v
hy : x ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨x, hy⟩
hpy : px ∈ G.finsetWalkLength n x v
⊢ Walk.cons ⋯ px ∈ ⊥

Proof state:
case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(∑ u_1 : ↑(G.neighborSet u),
        #(Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

Tactic:
norm_cast

Result:
case succ
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) =
    ↑(∑ u_1 : ↑(G.neighborSet u),
        #(Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))