fold as opposite to unfold

Stream: new members

[kana]

There is an unfold tactic. Is there a tactic to fold again?

def pair {A : Type} (x : A) := (x, x)

example : pair 1 = pair 2 := begin
  unfold pair,
  have pair_def : ∀{A} (x:A), pair x = (x, x) := by intros; unfold pair,
  rw ←pair_def,
end

[Eric Rodriguez]

you could change specifically, but I think most of the times we just make an auxillary lemma called lemma pair_def

[Eric Rodriguez]

something like

lemma pair_def {A : Type} (x : A) : pair x = (x, x) := rfl

[Eric Rodriguez]

(your have could be by intros; refl or even λ _ _, rfl)

[Eric Wieser]

Does rw ←pair work?

[kana]

Oh yes, rw <-pair really works, thanks!

[Eric Wieser]

@Eric Rodriguez, pair_def is almost never needed because pair gets a secret equation lemma containing the same statement

[Eric Rodriguez]

feel like I've seen it a fair bit in mathlib though, what's with that?

[Mario Carneiro]

sometimes the secret equation lemma is not stated the way we want. Sometimes you can fix that by writing the original definition differently but if that isn't good enough we can use a *_def lemma to state an arbitrary theorem not constrained by the grammar of the equation compiler