ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : length l ≤ 0
⊢ reverse l = []
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
⊢ 0 < length l
contrapose! hl
no goals
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : length l ≤ 0
⊢ reverse l = []
simpa [length_eq_zero] using hl
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
hl' : optParam (0 < length l) (_ : 0 < length l)
⊢ get l
      {
        val :=
          length l - 1 - ↑{ val := length (reverse l) - 1, isLt := (_ : length (reverse l) - 1 < length (reverse l)) },
        isLt := ?hn' } =
    get l { val := 0, isLt := hl' }

case hn'
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
hl' : optParam (0 < length l) (_ : 0 < length l)
⊢ length l - 1 - ↑{ val := length (reverse l) - 1, isLt := (_ : length (reverse l) - 1 < length (reverse l)) } <
    length l
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
hl' : optParam (0 < length l) (_ : 0 < length l)
⊢ getLast (reverse l) hl = get l { val := 0, isLt := hl' }
rw [getLast_eq_get, get_reverse']
no goals
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
hl' : optParam (0 < length l) (_ : 0 < length l)
⊢ get l
      {
        val :=
          length l - 1 - ↑{ val := length (reverse l) - 1, isLt := (_ : length (reverse l) - 1 < length (reverse l)) },
        isLt := ?hn' } =
    get l { val := 0, isLt := hl' }
simp
no goals
case hn'
ι : Type ?u.484228
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
hl : reverse l ≠ []
hl' : optParam (0 < length l) (_ : 0 < length l)
⊢ length l - 1 - ↑{ val := length (reverse l) - 1, isLt := (_ : length (reverse l) - 1 < length (reverse l)) } <
    length l
simpa using hl'