no goals
α : Type u_1
a : α
m n : Nat
l : List α
h : n < length (set l m a)
⊢ get (set l m a) { val := n, isLt := h } = if m = n then a else get l { val := n, isLt := (_ : n < length l) }
if h : m = n then subst m; simp else simp [h]
α : Type u_1
a : α
n : Nat
l : List α
h : n < length (set l n a)
⊢ get (set l n a) { val := n, isLt := h } = if n = n then a else get l { val := n, isLt := (_ : n < length l) }
α : Type u_1
a : α
m n : Nat
l : List α
h✝ : n < length (set l m a)
h : m = n
⊢ get (set l m a) { val := n, isLt := h✝ } = if m = n then a else get l { val := n, isLt := (_ : n < length l) }
subst m
no goals
α : Type u_1
a : α
n : Nat
l : List α
h : n < length (set l n a)
⊢ get (set l n a) { val := n, isLt := h } = if n = n then a else get l { val := n, isLt := (_ : n < length l) }
simp
no goals
α : Type u_1
a : α
m n : Nat
l : List α
h✝ : n < length (set l m a)
h : ¬m = n
⊢ get (set l m a) { val := n, isLt := h✝ } = if m = n then a else get l { val := n, isLt := (_ : n < length l) }
simp [h]