Dealing with f (h ▸ b)

Stream: lean4

[Tomas Skrivan]

Can I somehow rewrite f (h ▸ b) to (h ▸ f b)? I'm not even sure it is meaningful as I do not fully understand what ▸ does. Concretely, in my case f = PSigma.fst and I would like to reduce PSigma.fst (h ▸ {fst := x, snd := y}) to h ▸ x. How can I achieve that?

[Mario Carneiro]

Assuming that the statement typechecks, you should be able to prove this with cases h; rfl

[Mario Carneiro]

What is the type of h in your example?

[Mario Carneiro]

This is the sort of goal you want to avoid having in the first place

[Tomas Skrivan]

The concrete term is:

PSigma.fst
      ((_ : Impl (subs (comp swap (comp (comp HAdd.hAdd) HAdd.hAdd)) _root_.id) = Impl fun x y => x + y + x) ▸
        { fst := fun x x_1 => x + x_1 + _root_.id x,
          snd :=
            (_ :
            subs (comp swap (comp (comp HAdd.hAdd) HAdd.hAdd)) _root_.id =
              subs (comp swap (comp (comp HAdd.hAdd) HAdd.hAdd)) _root_.id) })
      x y

where

def Impl {α} (a : α) := (f : α) ×' (f = a)

[Mario Carneiro]

Do you have a #mwe?

[Tomas Skrivan]

I will try to produce one, but it will take me some time. For now, I have managed to avoid the problem as you have suggested :)