Unfolding a `:=` of a structure

Stream: lean4

[Yves Jäckle]

Hello!
How does one unfold a := defined in a structure ?
Ie. how do I prove the lemma in this MWE:

import Mathlib

variable {α : Type*} (G : SimpleGraph α)
variable [Fintype α] [DecidableEq α] [DecidableRel G.Adj]

-- Vertice Set (V), Edge Set (E), Graphs order (n)
local notation "V" => @Finset.univ α _
local notation "E" => G.edgeFinset
local notation "n" => Fintype.card α

open Finset SimpleGraph

-- "Value" of an edge = product of its vertices weight
def vp (w : α → NNReal) (e : Sym2 α) :=
  Quot.liftOn e (λ pair : α × α => w pair.1 * w pair.2)
    (by intros x y h; cases h;
        · apply refl
        · apply mul_comm)

-- f(w) in the informal proof
structure FunToMax where
  w : α → NNReal
  h_w : ∑ v in V, w v = 1
  fw := ∑ e in G.edgeFinset, vp w e


lemma FunToMax.fw_def (W : FunToMax G) : W.fw = ∑ e ∈ G.edgeFinset, vp W.w e := by
  -- exact rfl --fails
  unfold FunToMax.fw
  --dsimp!
  --unfold FunToMax.3
  sorry

[Ilmārs Cīrulis]

I was caught by this once, I believe. As far as I remember, it was pointed out to me that := in structure doesn't work as I expected - it defines default value if none is given or smth like that. :(

Let me find the thread... to check that what I have said isn't a hallucination.

[Edward van de Meent]

yup, that's exactly right

[Edward van de Meent]

when declaring a structure (i.e. creating the type), using := means to provide a default value to a field.

[Edward van de Meent]

you may instead want to define FunToMax.fw as a function.