Unfolding one field of a struct

Stream: lean4

[Bolton Bailey]

Suppose I have a structure with some fields very simple and some fields being very complicated values. I would like to be able to unfold the simple fields so that I can reason about them, while not unfolding the complicated ones, because they will clutter my view. Is there any way of doing this without defining specific lemmas for all the fields I want to unfold?

import Mathlib.LinearAlgebra.Lagrange

structure foobar where
  a : ℤ
  b : ℤ

def baz : foobar := {
  a := 1,
  b := 2 + 2 * 37 ^ 37 - 59 + 34
}

lemma foo : baz.a + baz.a + baz.b * (baz.a - 1) = 2 := by
  rw [baz] -- unfolds baz.b definition, which I don't want

Is there some name for the fact that baz.a = 1 that I can use to rewrite with here?

[Arthur Adjedj]

You can do :

theorem foo : baz.a + baz.a + baz.b * (baz.a - 1) = 2 := by
  have : baz.a = 1 := by rfl
  rw [this]

There is probably a better way to do it.

[Alex J. Best]

There is no autogenerated lemma of that form, it is true by defeq so you can do what Arthur says or even

rw [show baz.a = 1 from rfl]

or maybe even

change baz.a with 1

(untested) which should do the same thing

[Kyle Miller]

import Lean

structure foobar where
  a : Int
  b : Int

def baz : foobar where
  a := 1
  b := 2 + 2 * 37 ^ 37 - 59 + 34

-- setting to 37 to prevent `conv` from closing the resulting goal by `rfl`
theorem foo : baz.a + baz.a + baz.b * (baz.a - 1) = 37 := by
  conv =>
    pattern (occs := *) baz.a
    rw [baz]
  /-
  ⊢ { a := 1, b := 2 + 2 * 37 ^ 37 - 59 + 34 }.a + { a := 1, b := 2 + 2 * 37 ^ 37 - 59 + 34 }.a +
      baz.b * ({ a := 1, b := 2 + 2 * 37 ^ 37 - 59 + 34 }.a - 1) = 37
  -/
  done

[Kyle Miller]

(@Alex J. Best change ... with ... hasn't been implemented yet)

[Bolton Bailey]

Ok thanks, I'll think about these options