Unfold Notation

Stream: new members

[Marcus Rossel]

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]

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

[Alex J. Best]

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