ι : Type ?u.212813
α : 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.212813
α : 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.212813
α : 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.212813
α : 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.212813
α : 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