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

State before:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ snoc l x (last n) = x
Tactic:
simp only [snoc]
State after:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : (last n).val < n then l { val := (last n).val, isLt := h } else x) = x

State before:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : (last n).val < n then l { val := (last n).val, isLt := h } else x) = x
Tactic:
aesop
State after:
no goals