no goals
ι : Type ?u.111227
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < length (set l i a)
⊢ j < length l
simpa using hj
no goals
ι : Type ?u.111227
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
i j : ℕ
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, ← List.get?_eq_get, List.get?_set_ne _ _ h, List.get?_eq_get]