Zulip Chat Archive

Stream: mathlib4

Topic: Order.Hom.Order mathlib4#1152


Ruben Van de Velde (Dec 22 2022 at 10:53):

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 (Dec 22 2022 at 10:54):

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

Kevin Buzzard (Dec 22 2022 at 11:45):

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 (Dec 22 2022 at 12:16):

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


Last updated: Dec 20 2023 at 11:08 UTC