Using let to define structures locally

Stream: new members

[VayusElytra]

Hello, I am curious how one can write local definitions of structures into a proof.
Here's an instance of my problem:

structure dummyStructure where
  val1 : ℕ
  val2 : ℕ

lemma dummyLemma : Prop :=
  let a : dummyStructure where
    val1 := 1
    val2 := 2
  sorry

This gives the error that the token where is unexpected. Why does let not work here and what should I be using to define a structure locally in the middle of a proof then?

I think just writing

  let a : dummyStructure := ⟨1, 2⟩

works, but if I have anything more complicated than natural numbers in my structure this'll be very annoying to use...

[Ruben Van de Velde]

let a := { val1 := 1, val2 := 2 }

[VayusElytra]

thank you!

[VayusElytra]

i am a little curious why where does not work here while it is fine to use in a def for instance...