no goals
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i : Fin (length (take j L))
⊢ length (take j L) ≤ length L
simp [le_refl]
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i✝ : Fin (length (take j L))
i : ℕ
hi : i < length (take j L)
⊢ get (take j L) { val := i, isLt := hi } =
    get L { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < length L) }
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i : Fin (length (take j L))
⊢ get (take j L) i = get L { val := ↑i, isLt := (_ : ↑i < length L) }
let ⟨i, hi⟩ := i
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i✝ : Fin (length (take j L))
i : ℕ
hi✝ : i < length (take j L)
hi : i < j ∧ i < length L
⊢ get (take j L) { val := i, isLt := hi✝ } =
    get L { val := ↑{ val := i, isLt := hi✝ }, isLt := (_ : ↑{ val := i, isLt := hi✝ } < length L) }
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i✝ : Fin (length (take j L))
i : ℕ
hi : i < length (take j L)
⊢ get (take j L) { val := i, isLt := hi } =
    get L { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < length L) }
simp at hi
no goals
ι : Type ?u.167475
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
j : ℕ
i✝ : Fin (length (take j L))
i : ℕ
hi✝ : i < length (take j L)
hi : i < j ∧ i < length L
⊢ get (take j L) { val := i, isLt := hi✝ } =
    get L { val := ↑{ val := i, isLt := hi✝ }, isLt := (_ : ↑{ val := i, isLt := hi✝ } < length L) }
rw [get_take L _ hi.1]