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

State before:
n : Nat
⊢ fins (Nat.succ n) = map Fin.castSucc (fins n) ++ [Fin.last n]
Tactic:
unfold fins
State after:
n : Nat
⊢ fins.finsAux (Nat.succ n) (Nat.succ n) ⋯ [] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]

State before:
n : Nat
⊢ fins.finsAux (Nat.succ n) (Nat.succ n) ⋯ [] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
conv => lhs; unfold fins.finsAux
State after:
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]

State before:
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
suffices ∀ i (hi : i ≤ n) acc,
    fins.finsAux n.succ i (trans hi (Nat.le_succ _)) (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
  by have := this n (Nat.le_refl _) []; simpa using this
State after:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]

State before:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Tactic:
intro i hi acc
State after:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]

State before:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Tactic:
induction i generalizing acc with
| zero => unfold fins.finsAux; simp
| succ i ih =>
  unfold fins.finsAux
  replace ih := ih (Nat.le_of_lt hi) (⟨i,hi⟩ :: acc)
  simpa using ih
State after:
no goals

State before:
n : Nat
this :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
have := this n (Nat.le_refl _) []
State after:
n : Nat
this✝ :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
this :
  fins.finsAux (Nat.succ n) n ⋯ (map Fin.castSucc [] ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]

State before:
n : Nat
this✝ :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
this :
  fins.finsAux (Nat.succ n) n ⋯ (map Fin.castSucc [] ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
simpa using this
State after:
no goals

State before:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) Nat.zero ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n Nat.zero hi acc) ++ [Fin.last n]
Tactic:
unfold fins.finsAux
State after:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ map Fin.castSucc acc ++ [Fin.last n] = map Fin.castSucc acc ++ [Fin.last n]

State before:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ map Fin.castSucc acc ++ [Fin.last n] = map Fin.castSucc acc ++ [Fin.last n]
Tactic:
simp
State after:
no goals

State before:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) (Nat.succ i) ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n (Nat.succ i) hi acc) ++ [Fin.last n]
Tactic:
unfold fins.finsAux
State after:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]

State before:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Tactic:
replace ih := ih (Nat.le_of_lt hi) (⟨i,hi⟩ :: acc)
State after:
case succ
n i : Nat
hi : Nat.succ i ≤ n
acc : List (Fin n)
ih :
  fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc ({ val := i, isLt := hi } :: acc) ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]

State before:
case succ
n i : Nat
hi : Nat.succ i ≤ n
acc : List (Fin n)
ih :
  fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc ({ val := i, isLt := hi } :: acc) ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Tactic:
simpa using ih
State after:
no goals