Zulip Chat Archive

Stream: general

Topic: equality by components


view this post on Zulip Reid Barton (Feb 27 2018 at 15:54):

If my goal is of the form ⟨x, y⟩ = ⟨x', y'⟩, is there a tactic that will replace it with two new goals x = x' and y = y'?

view this post on Zulip Reid Barton (Feb 27 2018 at 15:56):

oh, congr did it.

view this post on Zulip Reid Barton (Feb 27 2018 at 16:21):

I'm also wondering how I could do this when the left and/or right hand side is not already a constructor application, and I want to eta expand first. (But in my actual case the right hand side was just a variable, and I could use induction.)

view this post on Zulip Mario Carneiro (Feb 27 2018 at 17:54):

Lean doesn't have definitional eta for products fyi


Last updated: May 11 2021 at 13:22 UTC