feat: add forall_fin_zero and exists_fin_zero

[fgdorais]

This PR adds lemmas forall_fin_zero and exists_fin_zero. It also marks lemmas forall_fin_zero, forall_fin_one, forall_fin_two, exists_fin_zero, exists_fin_one, exists_fin_two with simp attribute.

Closes #10629

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dfd3d185300df044fa087d3fa166cb6fb3bd8269 --onto 7d55c033e1f0ad8cb7c2b9ab72e5db40ce192222. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-30 19:45:03)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dfd3d185300df044fa087d3fa166cb6fb3bd8269 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-30 19:45:04)

[digama0]

this needs benchmarking, I think the reason it doesn't exist is because it has a too-generic discrimination tree key

[fgdorais]

I'd be happy to see a benchmark but this suggests it's not too generic:

#discr_tree_simp_key forall_fin_zero -- ∀  (Fin 0)
#discr_tree_simp_key exists_fin_zero -- @Exists (Fin 0) _

See also the RFC discussion #10629

[TwoFX]

!bench

[leanprover-radar]

Benchmark results for 107bef7 against dfd3d18 are in! @TwoFX

[leanprover-bot]

Here are the benchmark results for commit 107bef7.
There were significant changes against commit dfd3d18:

  Benchmark   Metric                       Change
  ==========================================================
+ stdlib      let-to-have transformation    -2.0%  (-32.8 σ)
+ stdlib      process pre-definitions       -3.3% (-118.8 σ)

[TwoFX]

@fgdorais, this PR looks fine to me but it's still a draft, is it still waiting for something?

[fgdorais]

The RFC hasn't been approved.