α : Type ?u.120711
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < length l
⊢ j < length l
α : Type ?u.120711
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < length (set l i a)
⊢ j < length l
simp at hj
no goals
α : Type ?u.120711
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < length l
⊢ j < length l
exact hj
no goals
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < length (set l i a)
⊢ get (set l i a) { val := j, isLt := hj } = get l { val := j, isLt := (_ : j < length l) }
rw [← Option.some_inj, ← get?_eq_get, get?_set_ne _ _ h, get?_eq_get]