case a
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
a✝ : α
⊢ a✝ ∈ get? (drop i L) j ↔ a✝ ∈ get? L (i + j)
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
⊢ get? (drop i L) j = get? L (i + j)
ext
case a
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
a✝ : α
⊢ (∃ h, get L { val := i + j, isLt := (_ : i + ↑{ val := j, isLt := (_ : j < length (drop i L)) } < length L) } = a✝) ↔
    ∃ h, get L { val := i + j, isLt := h } = a✝
case a
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
a✝ : α
⊢ a✝ ∈ get? (drop i L) j ↔ a✝ ∈ get? L (i + j)
simp only [get?_eq_some, get_drop', Option.mem_def]
no goals
case a
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
a✝ : α
⊢ (∃ h, get L { val := i + j, isLt := (_ : i + ↑{ val := j, isLt := (_ : j < length (drop i L)) } < length L) } = a✝) ↔
    ∃ h, get L { val := i + j, isLt := h } = a✝
constructor <;> exact fun ⟨h, ha⟩ => ⟨by simpa [lt_tsub_iff_left] using h, ha⟩
no goals
ι : Type ?u.214450
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
a✝ : α
x✝ : ∃ h, get L { val := i + j, isLt := h } = a✝
h : i + j < length L
ha : get L { val := i + j, isLt := h } = a✝
⊢ j < length (drop i L)
simpa [lt_tsub_iff_left] using h