ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ nthLe l (length l - 1 - n) hn' = nthLe (reverse l) n hn
ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ nthLe (reverse l) n hn = nthLe l (length l - 1 - n) hn'
rw [eq_comm]
case h.e'_2
ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ nthLe l (length l - 1 - n) hn' =
    nthLe (reverse (reverse l)) (length (reverse l) - 1 - n)
      (_ : length (reverse l) - 1 - n < length (reverse (reverse l)))
ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ nthLe l (length l - 1 - n) hn' = nthLe (reverse l) n hn
convert nthLe_reverse l.reverse n (by simpa) hn using 1
no goals
case h.e'_2
ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ nthLe l (length l - 1 - n) hn' =
    nthLe (reverse (reverse l)) (length (reverse l) - 1 - n)
      (_ : length (reverse l) - 1 - n < length (reverse (reverse l)))
simp
no goals
ι : Type ?u.97720
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
hn : n < length (reverse l)
hn' : length l - 1 - n < length l
⊢ length (reverse l) - 1 - n < length (reverse (reverse l))
simpa