Theorem: Fin.length_elementList (Algdata/Data/Fin/Basic.lean)

State before:
n : Nat
⊢ List.length (Fin.elementList n) = n
Tactic:
induction n
State after:
case zero

⊢ List.length (Fin.elementList Nat.zero) = Nat.zero

case succ
n✝ : Nat
n_ih✝ : List.length (Fin.elementList n✝) = n✝
⊢ List.length (Fin.elementList (Nat.succ n✝)) = Nat.succ n✝

State before:
⊢ List.length (Fin.elementList Nat.zero) = Nat.zero
Tactic:
case zero => rfl
State after:
no goals

State before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
Tactic:
case succ n h_ind => unfold Fin.elementList; unfold List.length; rw [List.length_map, h_ind]
State after:
no goals

State before:
⊢ List.length (Fin.elementList Nat.zero) = Nat.zero
Tactic:
rfl
State after:
no goals

State before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
Tactic:
unfold Fin.elementList
State after:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
      ({ val := 0, isLt := (_ : 0 < Nat.succ n) } ::
        List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) =
    Nat.succ n

State before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
      ({ val := 0, isLt := (_ : 0 < Nat.succ n) } ::
        List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) =
    Nat.succ n
Tactic:
unfold List.length
State after:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
        (List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) +
      1 =
    Nat.succ n

State before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
        (List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) +
      1 =
    Nat.succ n
Tactic:
rw [List.length_map, h_ind]
State after:
no goals