Order.Hom.Order mathlib4#1152

Stream: mathlib4

[Ruben Van de Velde]

There's a comment here how

-- -- @[simp, norm_cast]
-- theorem coe_infᵢ {ι : Sort _} [CompleteLattice β] (f : ι → α →o β) :
--     ((⨅ i, f i : α →o β) : α → β) = ⨅ i, f i := by
--   rfl

is a syntactic tautology now. I haven't been following if that's actually supposed to be the case now. Could someone who knows chime in?

[Yaël Dillies]

That defintely should not be a syntactic tautology. Try (⨅ i, f i : α →o β) = ⨅ i, (f i : α → β).

[Kevin Buzzard]

If a ported lemma name does not mention coe or to_fun and it's being marked as a syntactic tautology then it's almost certainly a victim of the new parsing rules and needs to be rebracketed.

[Ruben Van de Velde]

Feel free to push a fix if you have one, I'm on mobile ATM