Stream: new members

Topic: Unfold Notation

Marcus Rossel (Jan 15 2021 at 16:23):

Say I have the following:

structure some_type := (x : int) (y : int)

instance equiv : has_equiv some_type := ⟨λ l r, l.x = r.x⟩

lemma eq_imp_equiv {s s' : some_type} : s = s' → s ≈ s' :=
begin
-- ⊢ s = s' → s ≈ s'
end


How do I unfold the ≈ in the goal?
Thanks :blush:

Alex J. Best (Jan 15 2021 at 16:59):

 simp only [(≈)], is the way I usually unfold notation

Alex J. Best (Jan 15 2021 at 17:01):

However, much of the time this isn't necessary to prove the theorem, just to see what you're trying to prove!

Last updated: May 13 2021 at 18:26 UTC