Commit 2026-04-08 19:05 43840861

chore(Data/Finset/Lattice/Fold): use to_dual (#37047) This PR uses the @[to_dual] attribute to generate dual lemmas about Finset.sup. The lemmas about sdiff and himp are skipped, as HeytingAlgebra is not yet tagged with @[to_dual]. To improve the consistency between dual lemmas, several changes are made:

• tag inf_insert with @[grind =]
• rename le_inf_const_le to le_inf_const
• tag inf_union with @[grind _=_]
• tag inf_mono_fun with @[grind ←]
• tag inf_mono with @[grind ←]
• tag inf_attach with @[simp]
• add le_inf_of_directed_le
• add inf_eq_top_of_isEmpty
• add inf_mem_of_nonempty
• add inf'_mono_fun
• rename comp_sup_eq_sup_comp_of_nonempty to apply_sup_eq_sup_comp_of_nonempty and add apply_inf_eq_inf_comp_of_nonempty