Theorem: List.length_fins (LeanSAT/Upstream/ToStd.lean)

State before:
n : Nat
⊢ length (fins n) = n
Tactic:
unfold fins
State after:
n : Nat
⊢ length (fins.finsAux n n ⋯ []) = n

State before:
n : Nat
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
suffices ∀ i (hi : i ≤ n) acc, length (fins.finsAux n i hi acc) = length acc + i
  by have := this n (Nat.le_refl _) []; simp at this; exact this
State after:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i

State before:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
Tactic:
intro i hi acc
State after:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n i hi acc) = length acc + i

State before:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n i hi acc) = length acc + i
Tactic:
induction i generalizing acc <;>
  (unfold fins.finsAux; simp_all [Nat.succ_add, Nat.add_succ])
State after:
no goals

State before:
n : Nat
this : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
have := this n (Nat.le_refl _) []
State after:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = length [] + n
⊢ length (fins.finsAux n n ⋯ []) = n

State before:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = length [] + n
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
simp at this
State after:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = n
⊢ length (fins.finsAux n n ⋯ []) = n

State before:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = n
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
exact this
State after:
no goals

State before:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n (Nat.succ n✝) hi acc) = length acc + Nat.succ n✝
Tactic:
unfold fins.finsAux
State after:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n n✝ ⋯ ({ val := n✝, isLt := hi } :: acc)) = length acc + Nat.succ n✝

State before:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n n✝ ⋯ ({ val := n✝, isLt := hi } :: acc)) = length acc + Nat.succ n✝
Tactic:
simp_all [Nat.succ_add, Nat.add_succ]
State after:
no goals