Commit 2026-02-21 14:17 378b908c

feat(Order/Interval/Set/Basic): use to_dual (#35162) This PR tags basic theorems about Ioo, Ioc, Ico and Icc with to_dual. This is the other half of #33964. Notes:

• I decided to add the theorems Ico_subset_Ioo and Icc_subset_Ioc, because they were missing.
• For some proofs, the cast insertion heuristic failed, and I had to modify the proof slightly in order to make it work with to_dual. The two kinds of fixes were replacing fun ⟨hx₁, hx₁⟩ ↦ with fun hx ↦ and then using hx.1 and hx.2, and inserting an explicit rewrite using mem_Ioo in order to eliminate the defEq abuse. I should investigate how to fix this, but that shouldn't block this PR.
• There were some theorems that hold by rfl, but their dual does not. This confused the @[defEq] attribute, because we were erroneously setting it for these dual theorems. I've modified it so that it will first check if the attribute is applicable.
• left_notMem_Ioc and left_notMem_Ioo used to have explicit arguments. I made these implicit which lines up with their dual version, and their Finset counterparts.