ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
A : i < length L
⊢ j < length (drop i L)
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
⊢ j < length (drop i L)
have A : i < L.length := lt_of_le_of_lt (Nat.le.intro rfl) h
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length (take i L ++ drop i L)
A : i < length L
⊢ j < length (drop i L)
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
A : i < length L
⊢ j < length (drop i L)
rw [(take_append_drop i L).symm] at h
no goals
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length (take i L ++ drop i L)
A : i < length L
⊢ j < length (drop i L)
simpa only [le_of_lt A, min_eq_left, add_lt_add_iff_left, length_take,
  length_append] using h
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
⊢ nthLe L (i + j) h = nthLe (drop i L) j (_ : j < length (drop i L))
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
⊢ get L { val := i + j, isLt := h } = get (drop i L) { val := j, isLt := (_ : j < length (drop i L)) }
rw [← nthLe_eq, ← nthLe_eq]
no goals
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
⊢ nthLe L (i + j) h = nthLe (drop i L) j (_ : j < length (drop i L))
rw [nthLe_of_eq (take_append_drop i L).symm h, nthLe_append_right] <;>
simp [min_eq_left (show i ≤ length L from le_trans (by simp) (le_of_lt h))]
no goals
ι : Type ?u.209291
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i j : ℕ
h : i + j < length L
⊢ i ≤ i + j
simp