-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast?_range' (n : Nat) : (range' s n).getLast? = if n = 0 then none else some (s + n - 1)

Proof state:
case pos
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : n = 0
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
rw [if_pos h]

Result:
case pos
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : n = 0
⊢ some (none.getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Proof state:
case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
rw [if_neg h]

Result:
case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ some ((some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Proof state:
case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ s + 1 + n - 1 = s + (n + 1) - 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
by_cases h : n = 0

Result:
case pos
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : n = 0
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Proof state:
case zero
s : Nat
⊢ (range' s 0).getLast? = if 0 = 0 then none else some (s + 0 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case pos
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : n = 0
⊢ some (none.getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
simp [h]

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
⊢ (range' s (n + 1)).getLast? = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
rw [range'_succ, getLast?_cons, ih]

Result:
case succ
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
⊢ some ((if n = 0 then none else some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Proof state:
case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ some ((some (s + 1 + n - 1)).getD s) = if n + 1 = 0 then none else some (s + (n + 1) - 1)

Tactic:
simp

Result:
case neg
n : Nat
ih : ∀ {s : Nat}, (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
s : Nat
h : ¬n = 0
⊢ s + 1 + n - 1 = s + (n + 1) - 1