awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h : A.IsAdjMatrix
⊢ toGraph (A := A.compl) ⋯ = h.toGraphᶜ
have Adj : ∀ (v w : V), (toGraph (A := A.compl) sorry).Adj v w ↔ h.toGraphᶜ.Adj v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h : A.IsAdjMatrix
v w : V
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
have Adj : ∀ (h_1 : A v w = 0), (toGraph (A := A.compl) sorry).Adj v w ↔ h.toGraphᶜ.Adj v w
Tactic: rcases h.zero_or_one v w with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h : A.IsAdjMatrix
v w : V
Adj : ∀ (h_1 : A v w = 0), (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
have Adj₁ : ∀ (h_1 : A v w = 1), (toGraph (A := A.compl) sorry).Adj v w ↔ h.toGraphᶜ.Adj v w
Tactic: rcases h.zero_or_one v w with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 0
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
have pos : ∀ (hvw : v = w), (toGraph (A := A.compl) sorry).Adj v w ↔ h_1.toGraphᶜ.Adj v w
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 0
pos : ∀ (hvw : v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
have neg : ∀ (hvw : ¬v = w), (toGraph (A := A.compl) sorry).Adj v w ↔ h_1.toGraphᶜ.Adj v w
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 1
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
have pos : ∀ (hvw : v = w), (toGraph (A := A.compl) sorry).Adj v w ↔ h_1.toGraphᶜ.Adj v w
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 1
pos : ∀ (hvw : v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
have neg : ∀ (hvw : ¬v = w), (toGraph (A := A.compl) sorry).Adj v w ↔ h_1.toGraphᶜ.Adj v w
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : Zero α
inst_1 : One α
⊢ Eq (α := Matrix V V α) (adjMatrix α ⊥) 0
have a : ∀ (i j : V), adjMatrix α ⊥ i j = 0 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : Ring α
⊢ Eq (α := Matrix V V α) (adjMatrix α ⊤) ((of : (a : V → V → α) → Matrix V V α) fun (i j : V) ↦ if i = j then 0 else 1)
have a : ∀ (i j : V), adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : Ring α
i j : V
⊢ adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
have a : i = j → adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
Tactic: cases eq_or_ne i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : Ring α
i j : V
a : i = j → adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
⊢ adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
have a₁ : i ≠ j → adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
Tactic: cases eq_or_ne i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G
have a : ∀ (i j : V), (adjMatrix α G)ᵀ i j = adjMatrix α G i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
⊢ (adjMatrix α G).diag = 0
have h : ∀ (x : V), (adjMatrix α G).diag x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
⊢ IsAdjMatrix.toGraph (A := adjMatrix α G) ⋯ = G
have Adj : ∀ (x x_1 : V), (IsAdjMatrix.toGraph (A := adjMatrix α G) sorry).Adj x x_1 ↔ G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
x x_1 : V
⊢ (IsAdjMatrix.toGraph (A := adjMatrix α G) ⋯).Adj x x_1 ↔ G.Adj x x_1
have Adj : ¬G.Adj x x_1 → False ↔ G.Adj x x_1
Tactic: simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (hypothesis)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
H : SimpleGraph V
inst_4 : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ
have this : Gᶜ = H
Tactic: have := h.compl_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
H : SimpleGraph V
inst_4 : DecidableRel H.Adj
h : IsCompl G H
this : Gᶜ = H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ
have subst : ∀ [inst_5 : DecidableRel Gᶜ.Adj] (h : IsCompl G Gᶜ), adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ
Tactic: subst this
Cleared hypotheses: H, inst_4, h, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : AddGroup α
inst_1 : One α
inst_2 : DecidableEq V
⊢ adjMatrix α (completeGraph V) = HSub.hSub (α := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1
have a : ∀ (i j : V),
  adjMatrix α (completeGraph V) i j =
    HSub.hSub (α := Matrix V V α) (β := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u
have rw : (fun (j : V) ↦ adjMatrix α G v j) ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
Tactic: rw [mulVec, adjMatrix_dotProduct]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
rw : (fun (j : V) ↦ adjMatrix α G v j) ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u
have rw₁ : Eq.{u_1 + 1} (α := α) (∑ u ∈ G.neighborFinset v, vec u) (∑ u ∈ G.neighborFinset v, vec u)
Tactic: rw [mulVec, adjMatrix_dotProduct]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u
have simp : (vec ⬝ᵥ fun (i : V) ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v
Tactic: simp only [← dotProduct_adjMatrix, vecMul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun (i : V) ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v
have refine : (fun (i : V) ↦ adjMatrix α G i v) = adjMatrix α G v
Tactic: refine congr rfl ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun (i : V) ↦ adjMatrix α G i v) = adjMatrix α G v
have h : ∀ (x : V), adjMatrix α G x v = adjMatrix α G v x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x
have h : adjMatrix α G x v = (adjMatrix α G)ᵀ x v
Tactic: rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
x : V
h : adjMatrix α G x v = (adjMatrix α G)ᵀ x v
⊢ adjMatrix α G x v = adjMatrix α G v x
have h₁ : adjMatrix α G x v = adjMatrix α G x v
Tactic: rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = (↑(Fintype.card.{u_2} (↑{p : G.Walk u v | p.length = n} : Type u_2)) : α)
have rw : (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
Tactic: rw [card_set_walk_length_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
u v : V
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
have zero : HPow.hPow (β := ℕ) (adjMatrix α G) 0 u u = (↑(#(G.finsetWalkLength 0 u u)) : α)
Tactic: obtain rfl | h := eq_or_ne u v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
u v : V
zero : HPow.hPow (β := ℕ) (adjMatrix α G) 0 u u = (↑(#(G.finsetWalkLength 0 u u)) : α)
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
have zero₁ : ∀ (h : u ≠ v), HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
Tactic: obtain rfl | h := eq_or_ne u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : 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)) : α)
have succ : Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
  (↑(card.{u_2} (α := G.Walk u v)
        (Finset.biUnion univ fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
          Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons sorry p, inj' := sorry }
            (G.finsetWalkLength n (↑w : V) v))) :
    α)
Tactic: simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(card.{u_2} (α := G.Walk u v)
          (Finset.biUnion univ fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
            Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑w : V) v))) :
      α)
have succ : Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
  (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
        card (α := G.Walk u v)
          (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons sorry p, inj' := sorry }
            (G.finsetWalkLength n (↑u_1 : V) v))) :
    α)
Tactic: rw [Finset.card_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
succ :
  Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(card.{u_2} (α := G.Walk u v)
          (Finset.biUnion univ fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
            Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑w : V) v))) :
      α)
have succ₁ : (↑univ : Set (↑(G.neighborSet u) : Type u_2)).PairwiseDisjoint (α := Finset (G.Walk u v))
  fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
  Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons sorry p, inj' := sorry }
    (G.finsetWalkLength n (↑w : V) v)
Tactic: rw [Finset.card_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
⊢ Eq.{u_1 + 1} (α := α) (∑ x ∈ G.neighborFinset u, (↑(#(G.finsetWalkLength n x v)) : α))
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)
have succ : Eq.{u_1 + 1} (α := α) (↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) : α)
  (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
        card (α := G.Walk u v)
          (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons sorry p, inj' := sorry }
            (G.finsetWalkLength n (↑u_1 : V) v))) :
    α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
u v : V
⊢ Eq.{u_1 + 1} (α := α) (↑(∑ x ∈ G.neighborFinset u, #(G.finsetWalkLength n x v)) : α)
    (↑(∑ u_1 : (↑(G.neighborSet u) : Type u_2),
          card (α := G.Walk u v)
            (Finset.map (α := G.Walk (↑u_1 : V) v) { toFun := fun (p : G.Walk (↑u_1 : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
              (G.finsetWalkLength n (↑u_1 : V) v))) :
      α)
have succ : Eq.{u_1 + 1} (α := α) (∑ x ∈ (G.neighborSet u).toFinset, (↑(#(G.finsetWalkLength n x v)) : α))
  (∑ x : (↑(G.neighborSet u) : Type u_2), (↑(card (α := G.Walk (↑x : V) v) (G.finsetWalkLength n (↑x : V) v)) : α))
Tactic: simp only [Nat.cast_sum, card_map, neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : 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 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
⊢ Function.onFun (β := Finset (G.Walk u v)) Disjoint
    (fun (w : (↑(G.neighborSet u) : Type u_2)) ↦
      Finset.map (α := G.Walk (↑w : V) v) { toFun := fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p, inj' := ⋯ }
        (G.finsetWalkLength n (↑w : V) v))
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy)
have succ : LE.le (α := Finset (G.Walk u v))
  (Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v)
      { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ↦ Walk.cons sorry p,
        inj' := sorry }
      (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ⊓
    Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v)
      { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v) ↦ Walk.cons sorry p,
        inj' := sorry }
      (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v))
  ⊥
Tactic: rw [Function.onFun, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (hypothesis)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : 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 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy
p : G.Walk u v
hp :
  Membership.mem (γ := Finset (G.Walk u v))
    (Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx) : V) v) ⊓
      Finset.map (α := G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v)
        { toFun := fun (p : G.Walk (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v) ↦ Walk.cons ⋯ p,
          inj' := ⋯ }
        (G.finsetWalkLength n (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) y hy) : V) v))
    p
⊢ Membership.mem (γ := Finset (G.Walk u v)) ⊥ p
have hp₁ : (∃ a ∈ G.finsetWalkLength n x v, Walk.cons sorry a = p) ∧ ∃ a ∈ G.finsetWalkLength n y v, Walk.cons sorry a = p
Tactic: simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : 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 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) 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
⊢ Membership.mem (γ := Finset (G.Walk u v)) ⊥ p
have succ : ∀ px ∈ G.finsetWalkLength n x v,
  ∀ (py : G.Walk y v) (hpy : py ∈ G.finsetWalkLength n y v)
    (hp : Eq (α := G.Walk u v) (Walk.cons sorry py) (Walk.cons sorry px)),
    Membership.mem (γ := Finset (G.Walk u v)) ⊥ (Walk.cons sorry px)
Tactic: obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (hypothesis)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : 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 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) 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 : Eq (α := G.Walk u v) (Walk.cons ⋯ py) (Walk.cons ⋯ px)
hy₁ : x ∈ G.neighborSet u
⊢ Membership.mem (γ := Finset (G.Walk u v)) ⊥ (Walk.cons ⋯ px)
have hxy₁ : Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hx ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet u) x hy₁
Tactic: cases hp
Cleared hypotheses: y, hy, hxy, py, hpy, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : DecidableEq V
inst_3 : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = (↑(#(G.finsetWalkLength n u v)) : α)
have zero : ∀ (u v : V), HPow.hPow (β := ℕ) (adjMatrix α G) 0 u v = (↑(#(G.finsetWalkLength 0 u v)) : α)
Tactic: induction n generalizing u v with
  | zero => obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]
  | succ n ih =>
    simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]
    rw [Finset.card_biUnion]
    · norm_cast
      simp only [Nat.cast_sum, card_map, neighborFinset_def]
      apply Finset.sum_toFinset_eq_subtype
    -- Disjointness for card_bUnion
    · rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
      rw [Function.onFun, disjoint_iff_inf_le]
      intro p hp
      simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk] at hp
      obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
      cases hp
      simp at hxy
Cleared hypotheses: n, u, v