Using 'case zero' in induction

Stream: new members

[Aeacus Sheng]

Hi, I'm trying to show that if α is FinEnum, then α → Bool is also FinEnum in the following attempt:

instance FinEnumToBool.finEnum [FinEnum α] : FinEnum (α → Bool) := {
  card := 2^(FinEnum.card α),
  equiv := by
    induction FinEnum.card α with
    | zero =>
      have: FinEnum.card α = 0 := by sorry
      sorry
    | succ n ih => sorry
}

As you can see, I'm trying to construct the equivalence between 2^(FinEnum.card α) and α → Bool by induction on the cardinality of α. In the zero case, I think I should be able to use the case hypothesis: FinEnum.card α = 0 and derive that α is empty (and proceed from there, if possible.) But couldn't find a way to access it or prove it. It seems that lean automatically replaced the 'FinEnum.card α' in the goal with 0, but does not supply it in the proof. Does anyone know how to get it? Thanks!

[Daniel Weber]

You can do

instance FinEnumToBool.finEnum [FinEnum α] : FinEnum (α → Bool) := {
  card := 2^(FinEnum.card α),
  equiv := by
    generalize h : FinEnum.card α = c
    induction c generalizing α with
    | zero =>
      have: FinEnum.card α = 0 := h
      sorry
    | succ n ih => sorry
}

[Daniel Weber]

(deleted)

[Aeacus Sheng]

Daniel Weber said:

You can do

instance FinEnumToBool.finEnum [FinEnum α] : FinEnum (α → Bool) := {
  card := 2^(FinEnum.card α),
  equiv := by
    generalize h : FinEnum.card α = c
    induction c generalizing α with
    | zero =>
      have: FinEnum.card α = 0 := h
      sorry
    | succ n ih => sorry
}

Thanks!

[Daniel Weber]

By the way, instead of writing := { .. } you can do

instance FinEnumToBool.finEnum [FinEnum α] : FinEnum (α → Bool) where
  card := 2^(FinEnum.card α)
  equiv := by
    generalize h : FinEnum.card α = c
    induction c generalizing α with
    | zero =>
      have: FinEnum.card α = 0 := h
      sorry
    | succ n ih => sorry