dot notation seeing through defs

Stream: lean4

[Kevin Buzzard]

Porting logic.function.conjugate (edit: before noticing that Jon Eugster had done it). This doesn't work in Lean 4

namespace Function

variable {α : Type _} {β : Type _} {γ : Type _}

def Semiconj (f : α → β) (ga : α → α) (gb : β → β) : Prop :=
  ∀ x, f (ga x) = gb (f x)

namespace Semiconj

variable {f : α → β} {ga ga' : α → α} {gb gb' : β → β}

theorem comp_right (h : Semiconj f ga gb) (h' : Semiconj f ga' gb') : Semiconj f (ga ∘ ga') (gb ∘ gb') := fun x =>
  sorry

end Semiconj

def Commute (f g : α → α) : Prop := Semiconj f g g

namespace Commute

variable {f g g' : α → α}

theorem comp_right (h : Commute f g) (h' : Commute f g') : Commute f (g ∘ g') :=
h.comp_right h' -- fails to show termination

end Commute

end Function

but it worked in Lean 3. I'm assuming h.comp_right is being interpreted as Commute.comp_right in Lean 4 and as Semiconj.comp_right in Lean 3. I can work around with Semiconj.comp_right h h'. (erroneous claim about next lemma in same file deleted)

[Mario Carneiro]

Yes, this is expected behavior. You just have to refer to Semiconj.comp_right

[Kyle Miller]

It wouldn't work correctly in this case, but another way (I presume) you're expected to handle this is to export names into a namespace, since dot notation does look at aliases.

For example,

namespace Commute
export Semiconj (comp_right)
end Commute

The reason this wouldn't work correctly here is that the Commute.comp_right you get yields a Semiconj rather than a Commute.