Analogue of `fin_cases` for `Set (Fin n)` / `FinSet (Fin n)`

Stream: new members

[Li Xuanji]

I have two related questions:

import Mathlib

example
  (I : Fin 2)
: I = 0 ∨ I = 1 := by
  fin_cases I <;> simp

example
  (I : Finset (Fin 2))
: I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  fin_cases I
  left; rfl
  right; left; rfl
  right; right; left; rfl
  right; right; right; rfl

example
  (I : Set (Fin 2))
: I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  sorry

1. Can the proof of the second example be made shorter?
2. How do I prove the third example?

[Niels Voss]

For 1., you can do fin_cases I <;> decide

[Niels Voss]

For 2., I think the reason this is difficult is that I is essentially a function Fin 2 -> Prop, which is basically a pair of propositions. There's no algorithm to determine whether an arbitrary proposition is true or false, so this prevents tactics like decide from working. I'm trying to think of an alternative

[Kenny Lau]

there is no decide, but that doesn't mean a tactic is not possible...

[Kenny Lau]

or maybe first convert it to Finset so you can decide

[Kenny Lau]

@Li Xuanji

import Mathlib

example (I : Fin 2) : I = 0 ∨ I = 1 := by
  decide +revert

example (I : Finset (Fin 2)) : I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  decide +revert

example (I : Set (Fin 2)) : I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  obtain ⟨I, rfl⟩ := Fintype.finsetEquivSet.surjective I
  simp_rw [Equiv.apply_eq_iff_eq_symm_apply]
  simpa using by decide +revert

[Li Xuanji]

Thanks! I am not familiar with decide +revert - for learning purposes, is there a way to write the proof like this?

example (I : Finset (Fin 2)) : I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  <some manual reverts here>
  decide

[Aaron Liu]

import Mathlib

example (I : Finset (Fin 2)) : I = {} ∨ I = {0} ∨ I = {1} ∨ I = {0, 1} := by
  revert I
  decide

[Li Xuanji]

:wave: I'm back with another similar question, which is how to solve the sorry in the third example here

import Mathlib


example (I : Finset (Finset (Fin 2))) :
    I = {} ∨
    I = {{}} ∨ I = {{0}} ∨ I = {{1}} ∨ I = {{0, 1}} ∨
    I = {{}, {0}} ∨ I = {{}, {1}} ∨ I = {{}, {0, 1}} ∨
    I = {{0}, {1}} ∨ I = {{0}, {0, 1}} ∨ I = {{1}, {0, 1}} ∨
    I = {{}, {0}, {1}} ∨ I = {{}, {0}, {0, 1}} ∨ I = {{}, {1}, {0, 1}} ∨
    I = {{0}, {1}, {0, 1}} ∨
    I = {{}, {0}, {1}, {0, 1}} := by
  decide +revert

example (I : Set (Finset (Fin 2))) :
    I = {} ∨
    I = {{}} ∨ I = {{0}} ∨ I = {{1}} ∨ I = {{0, 1}} ∨
    I = {{}, {0}} ∨ I = {{}, {1}} ∨ I = {{}, {0, 1}} ∨
    I = {{0}, {1}} ∨ I = {{0}, {0, 1}} ∨ I = {{1}, {0, 1}} ∨
    I = {{}, {0}, {1}} ∨ I = {{}, {0}, {0, 1}} ∨ I = {{}, {1}, {0, 1}} ∨
    I = {{0}, {1}, {0, 1}} ∨
    I = {{}, {0}, {1}, {0, 1}} := by
  obtain ⟨I, rfl⟩ := Fintype.finsetEquivSet.surjective I
  simp_rw [Equiv.apply_eq_iff_eq_symm_apply]
  simpa using by decide +revert

example (I : Set (Set (Fin 2))) :
    I = {} ∨
    I = {{}} ∨ I = {{0}} ∨ I = {{1}} ∨ I = {{0, 1}} ∨
    I = {{}, {0}} ∨ I = {{}, {1}} ∨ I = {{}, {0, 1}} ∨
    I = {{0}, {1}} ∨ I = {{0}, {0, 1}} ∨ I = {{1}, {0, 1}} ∨
    I = {{}, {0}, {1}} ∨ I = {{}, {0}, {0, 1}} ∨ I = {{}, {1}, {0, 1}} ∨
    I = {{0}, {1}, {0, 1}} ∨
    I = {{}, {0}, {1}, {0, 1}} := by
  sorry

(I swear I'm not trolling and these Set (Set X)) come up in point-set topology :sweat_smile: )

My attempt: I think I understand how the finsetEquivSet proof is working, but I don't quite see if there's an easy way to apply it to the "inner set" in the example. I also tried rewriting the "outer set" and then using fin_cases to try to reduce it to 4 goals about Set (Fin 2), but that didn't work.

[Robin Arnez]

import Mathlib

example (I : Set (Set (Fin 2))) :
    I = {} ∨
    I = {{}} ∨ I = {{0}} ∨ I = {{1}} ∨ I = {{0, 1}} ∨
    I = {{}, {0}} ∨ I = {{}, {1}} ∨ I = {{}, {0, 1}} ∨
    I = {{0}, {1}} ∨ I = {{0}, {0, 1}} ∨ I = {{1}, {0, 1}} ∨
    I = {{}, {0}, {1}} ∨ I = {{}, {0}, {0, 1}} ∨ I = {{}, {1}, {0, 1}} ∨
    I = {{0}, {1}, {0, 1}} ∨
    I = {{}, {0}, {1}, {0, 1}} := by
  obtain ⟨I, rfl⟩ := (Fintype.finsetEquivSet.trans (Equiv.Set.congr Fintype.finsetEquivSet)).surjective I
  simp_rw [Equiv.apply_eq_iff_eq_symm_apply]
  simpa [Set.image_insert_eq] using by decide +revert