Unfolding a definition

Stream: new members

[Lauri Oksanen]

Is there any difference between rw [def] and unfold def? If yes, is there a reason to prefer one over the other? Also, is there a way to unfold the definition of a subset to something more readable than Set.instHasSubset.1? (I am looking for a way other than directly proving A ⊆ B ↔ ∀ x, x ∈ A → x ∈ B.)

Here is some code for context:

import Mathlib

inductive X : Type
  | a : X

open X Function

def f : X → ℕ
  | a => 0

example : Injective f := by
  rw [Injective]
  tauto

example : Injective f := by
  unfold Injective
  tauto

variable (A : Set X)

example : A ⊆ A := by
  rw [Subset]
  tauto

example : A ⊆ A := by
  unfold Subset
  tauto

[Ruben Van de Velde]

Is there not a docs#Set.subset_def lemma?

[Luigi Massacci]

Indeed it's that one. @Lauri Oksanen in general you are not really supposed to unfold definitions (especially for very basic objects) but rather use their attached API, such as the lemma @Ruben Van de Velde pointed out. Unfolding will often result in nasty looking stuff, and is also quite brittle as a strategy, as the details of definitions are liable to change often (to something mathematically equivalent of course). Aside from being a good coding practice it's good mathematics, thinking in terms of universal properties and so on

[Lauri Oksanen]

Thanks a lot!