!4#3287

Stream: mathlib4

[Jeremy Tan]

!4#3287 can somebody help fix the last error here?

theorem adjMatrix_vecMul_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
    ((G.adjMatrix α).vecMul vec) v = ∑ u in G.neighborFinset v, vec u := by
  rw [← dotProduct_adjMatrix, vecMul]
  refine' congr rfl _; ext
  rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

[Jeremy Tan]

Apparently the proof starts to diverge from mathlib3 at rv [vecMul], when it for some reason generates a let:

(let j := v;
  vec ⬝ᵥ fun i => adjMatrix α G i j) =
  (fun u => vec u) ⬝ᵥ adjMatrix α G v

[Jeremy Tan]

The subsequent refine' congr rfl _ turns this into a veritable mess. How can I subsume the let?

[Ruben Van de Velde]

try rw → simp only?

[Jeremy Tan]

Right, that worked, thanks