-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast?

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[min n l.length - 1]? = if n = 0 then none else l[n - 1]?.or l.getLast?

Tactic:
rw [if_neg (by omega)]

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[min n l.length - 1]? = l[n - 1]?.or l.getLast?

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[(if n ≤ l.length then n else l.length) - 1]? = l[n - 1]?.or l.getLast?

Tactic:
split

Result:
case isTrue.isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : n ≤ l.length
⊢ l[n - 1]? = l[n - 1]?.or l.getLast?

case isTrue.isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1]? = l[n - 1]?.or l.getLast?

Proof state:
case isTrue.isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : n ≤ l.length
⊢ l[n - 1]? = l[n - 1]?.or l.getLast?

Tactic:
rw [getElem?_eq_getElem (by omega)]

Result:
case isTrue.isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : n ≤ l.length
⊢ some l[n - 1] = (some l[n - 1]).or l.getLast?

Proof state:
case isTrue.isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1]? = l[n - 1]?.or l.getLast?

Tactic:
rw [← getLast?_eq_getElem?, getElem?_eq_none (by omega)]

Result:
case isTrue.isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : ¬n ≤ l.length
⊢ l.getLast? = none.or l.getLast?

Proof state:
case isFalse.hc
α : Type u_1
n : Nat
l : List α
h✝ : ¬min n l.length - 1 < n
⊢ n = 0

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬min n l.length - 1 < n
⊢ none = if n = 0 then none else l[n - 1]?.or l.getLast?

Tactic:
rw [if_pos]

Result:
case isFalse.hc
α : Type u_1
n : Nat
l : List α
h✝ : ¬min n l.length - 1 < n
⊢ n = 0

Proof state:
case isTrue.isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : ¬n ≤ l.length
⊢ l.getLast? = none.or l.getLast?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (take n l).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast?

Tactic:
rw [getLast?_eq_getElem?, getElem?_take, length_take]

Result:
α : Type u_1
n : Nat
l : List α
⊢ (if min n l.length - 1 < n then l[min n l.length - 1]? else none) = if n = 0 then none else l[n - 1]?.or l.getLast?

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ ¬n = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : n ≤ l.length
⊢ n - 1 < l.length

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : n ≤ l.length
⊢ some l[n - 1] = (some l[n - 1]).or l.getLast?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝¹ : min n l.length - 1 < n
h✝ : ¬n ≤ l.length
⊢ l.length ≤ n - 1

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[min n l.length - 1]? = l[n - 1]?.or l.getLast?

Tactic:
rw [Nat.min_def]

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[(if n ≤ l.length then n else l.length) - 1]? = l[n - 1]?.or l.getLast?

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (if min n l.length - 1 < n then l[min n l.length - 1]? else none) = if n = 0 then none else l[n - 1]?.or l.getLast?

Tactic:
split

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : min n l.length - 1 < n
⊢ l[min n l.length - 1]? = if n = 0 then none else l[n - 1]?.or l.getLast?

case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬min n l.length - 1 < n
⊢ none = if n = 0 then none else l[n - 1]?.or l.getLast?