Automatic projections in theorem definition

Stream: lean4

[Pavel Klimov]

How do I force to avoid renaming of projections? Now I don't know how can I write have statement so I could use it in rw tactic. :frown:

structure qwe where
a : Int
b : Int

theorem test (x : qwe): x.1 = x.a := rfl

#check test

It outputs theorem conclusion as x.a = x.a so if in my context something has .1 I cant rewrite it using rw.

Edit: I want to add context. My real case is not so simple. It changes name of projection somewhere inside theorem.

[Aaron Liu]

structure qwe where
a : Int
b : Int

#check qwe.a.eq_def

[Pavel Klimov]

It doesn't answer the question. I want to define theorem which I can apply in rw tactic. The one above doesn't work because it says it can't find pattern. And, indeed there is no pattern with .field_name, there is only pattern with .1.

[Robin Arnez]

I think he means to use rw [← qwe.a.eq_def]? Anyways, if you have an actual .1 in your context then probably something went wrong.

[Robin Arnez]

Did you try something like simp [qwe.a]?