namespace of decl influences simp behavior

Stream: lean4

[Matthew Ballard]

I find this crazy. Hom.bar is closed by simp but bar is not. They are same up to the name.

universe v u

class Quiver (V : Type u) where
  Hom : V → V → Sort v

infixr:10 " ⟶ " => Quiver.Hom

structure Opposite (α : Sort u) :=
  op :: unop : α

notation:max α "ᵒᵖ" => Opposite α

open Opposite

namespace Quiver

instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶  unop a)ᵒᵖ⟩

abbrev Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := Opposite.op f

abbrev Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f

variable (C : Type u) [Quiver.{v} C]

@[simp]
theorem Hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f := rfl

theorem Hom.bar {X Y : Cᵒᵖ} (f : X ⟶  Y) : op (unop f) = f := by simp -- works
theorem bar {X Y : Cᵒᵖ} (f : X ⟶ Y) : op (unop f) = f := by simp -- fails

[Matthew Ballard]

Should I not find this crazy?

[Matthew Ballard]

This is on commit 82401938 in core

[Matthew Ballard]

Ok. I guess op and unop are parsed as Quiver.Hom.op and Quiver.Hom.unop in Hom.bar despite what the hover tells me.

[Matthew Ballard]

instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun ⟨a⟩ ⟨b⟩ => (b ⟶  a)ᵒᵖ⟩

makes everything work