feat: lemmas to simplify equalities with Option-typed dependent if-then-else

[wupr]

Closes #4013.

Add dite_some_none_eq_none and dite_some_none_eq_some, analogous to the existing ite_some_none_eq_none and ite_some_none_eq_some.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4037 build failed against this PR. (2024-04-30 23:01:45) View Log
• 💥 Mathlib branch lean-pr-testing-4037 build failed against this PR. (2024-04-30 23:20:16) View Log
• 💥 Mathlib branch lean-pr-testing-4037 build failed against this PR. (2024-05-01 13:09:54) View Log
• ✅ Mathlib branch lean-pr-testing-4037 has successfully built against this PR. (2024-05-01 14:09:19) View Log
• ✅ Mathlib branch lean-pr-testing-4037 has successfully built against this PR. (2024-05-01 14:51:25) View Log

[nomeata]

Hmm, looks like this breaks mathlib, this might need diagnosing

[wupr]

It looks like the problem could be with the use of a non-final simp in Mathlib. But I think I need to merge the new commits in nightly-with-mathlib first.

[wupr]

The errors was thrown in Mathlib/Data/FinEnum.lean at the third line below:

instance Subtype.finEnum [FinEnum α] (p : α → Prop) [DecidablePred p] : FinEnum { x // p x } :=
  ofList ((toList α).filterMap fun x => if h : p x then some ⟨_, h⟩ else none)
    (by rintro ⟨x, h⟩; simp; exists x; simp [*])

But the proof can be simplified as follows now:

instance Subtype.finEnum [FinEnum α] (p : α → Prop) [DecidablePred p] : FinEnum { x // p x } :=
  ofList ((toList α).filterMap fun x => if h : p x then some ⟨_, h⟩ else none)
    (by simp)

There may be other problems like this and I'm trying to compile Mathlib locally to identify them.

Where should I push the fix? To the lean-pr-testing-4037 branch on Mathlib?

[nomeata]

Where should I push the fix? To the lean-pr-testing-4037 branch on Mathlib?

Exactly! Just keep pushing fixed until mathlib is happy, then we can see if the changes needed are benign

[semorrison]

Changes to Mathlib look fine, so lets proceed!