-- 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 zero
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))

Tactic:
obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]

Result:
no goals

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⟩
p : G.Walk u v
hp : (∃ a ∈ G.finsetWalkLength n x v, Walk.cons ⋯ a = p) ∧ ∃ a ∈ G.finsetWalkLength n y v, Walk.cons ⋯ a = p
⊢ p ∈ ⊥

Tactic:
obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp

Result:
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 ∈ ⊥

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
⊢ (adjMatrix α G ^ (n + 1)) u v = ↑(#(G.finsetWalkLength (n + 1) u v))

Tactic:
simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]

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)) =
    ↑(#(univ.biUnion fun w => Finset.map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)))

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⟩
⊢ 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:
intro p hp

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⟩
p : G.Walk u v
hp :
  p ∈
    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)
⊢ p ∈ ⊥

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 ∈ 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))

Tactic:
rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy

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⟩
⊢ 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))

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⟩
p : G.Walk u v
hp :
  p ∈
    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)
⊢ p ∈ ⊥

Tactic:
simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk, exists_prop] at hp

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⟩
p : G.Walk u v
hp : (∃ a ∈ G.finsetWalkLength n x v, Walk.cons ⋯ a = p) ∧ ∃ a ∈ G.finsetWalkLength n y v, Walk.cons ⋯ a = p
⊢ p ∈ ⊥

Proof state:
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 ∈ ⊥

Tactic:
simp at hxy

Result:
no goals

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:
simp only [Nat.cast_sum, card_map, neighborFinset_def]

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.neighborSet u).toFinset, ↑(#(G.finsetWalkLength n x v)) =
    ∑ x : ↑(G.neighborSet u), ↑(#(G.finsetWalkLength n (↑x) v))

Proof state:
V : Type u_1
α : Type u_2
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 | p.length = n})

Tactic:
rw [card_set_walk_length_eq]

Result:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))