dsimp を simp から独立させる

[Seasawher]

dsimp へのリンクを貼りたいことがあるのと，定義を展開するだけのタクティクには独特な需要があるので

[Seasawher]

dsimp は simp の派生というよりも，unfold のより高度なバージョンかもしれない

simp 属性が付けられた補題は dsimp の挙動に影響するのだろうか？

もし unfold も紹介することがあれば，unfold との関連にも着目すべきかも

[Seasawher]

unfold は既に紹介していたので，間違いなく dsimp との差異は問題になる

[Seasawher]

dsimp と unfold の違いが現れるケース（のMathlibに依存しない例）

see: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/unfold.20vs.20dsimp/near/423612903

-- α の部分集合を表す型
def Set (α : Type) := α → Prop

-- 部分集合の共通部分を取る操作
def Set.inter {α : Type} (s t : Set α) : Set α := fun x => s x ∧ t x

-- ∩ という記法を使えるようにする
instance (α : Type) : Inter (Set α) where
  inter := Set.inter

variable (s t : Set α)

example : s ∩ u = u ∩ s := by
  dsimp [(· ∩ ·)]

  -- 記法の部分だけを展開できる
  show s.inter u = u.inter s
  sorry

example : s ∩ u = u ∩ s := by
  dsimp [Inter.inter]

  show s.inter u = u.inter s
  sorry

example : s ∩ u = u ∩ s := by
  unfold Inter.inter

  -- 展開結果の中にインスタンスが入り込んでしまう
  show (instInterSet α).1 s u = (instInterSet α).1 u s
  sorry