Theorem: Fin.snoc_castSucc (SetTheory/Formula.lean)

State before:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ snoc l x (castSucc k) = l k
Tactic:
rw [Fin.snoc, dif_pos]
State after:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ l { val := (castSucc k).val, isLt := ?hc } = l k

case hc
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ (castSucc k).val < n

State before:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ l { val := (castSucc k).val, isLt := ?hc } = l k

case hc
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ (castSucc k).val < n
Tactic:
rfl
State after:
no goals