Commit 2025-12-24 12:03 91bd394a

View on Github →

feat(Order/Lattice): use @[to_dual] (#33142) This PR tags Lattice and DistribLattice with @[to_dual]

  • I removed @[simp] from ofDual_max because ofDual_sup is a strictly stronger simp lemma.
  • I added a missing @[to_dual] tag in some other file that I needed for this.
  • I skipped the part about monotonicity, since that still depends on #32438

Estimated changes

deleted theorem Function.update_inf
deleted theorem Pi.inf_apply
deleted theorem Pi.inf_def
deleted theorem Prod.fst_inf
deleted theorem Prod.inf_def
deleted theorem Prod.mk_inf_mk
deleted theorem Prod.snd_inf
deleted theorem Prod.swap_inf
deleted theorem Subtype.coe_inf
deleted theorem Subtype.mk_inf_mk
modified theorem inf_eq_sup
deleted theorem inf_ind
deleted theorem inf_le_iff
modified theorem inf_left_le_sup_left
modified theorem inf_left_le_sup_right
deleted theorem inf_lt_iff
deleted theorem inf_right_le_sup_left
modified theorem inf_right_le_sup_right
added theorem inf_sup_le
deleted theorem le_inf_sup
modified theorem le_sup_inf
deleted theorem lt_inf_iff
deleted theorem min_min_min_comm
deleted theorem ofDual_inf
modified theorem ofDual_max
deleted theorem ofDual_min
deleted theorem sup_eq_inf
deleted theorem sup_inf_self
deleted theorem toDual_inf
modified theorem toDual_max
deleted theorem toDual_min