Theorem: Array.head?_toListRev (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toListRev.head? = a.back?
Tactic:
cases a.size.eq_zero_or_pos
State after:
case inl
C : Type u_1
α : Type u_2
a : Array α
h✝ : a.size = 0
⊢ a.toListRev.head? = a.back?

case inr
C : Type u_1
α : Type u_2
a : Array α
h✝ : a.size > 0
⊢ a.toListRev.head? = a.back?

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.toListRev.head? = a.back?
Tactic:
case inl h =>
  rw [toListRev_eq, back?, ← get?_data]
  simp [List.length_eq_zero.mp h]
State after:
no goals

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.toListRev.head? = a.back?
Tactic:
case inr h =>
  rw [← List.get?_zero, get?_toListRev _ _ h, Nat.sub_zero]
  rfl
State after:
no goals

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.toListRev.head? = a.back?
Tactic:
rw [toListRev_eq, back?, ← get?_data]
State after:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.data.reverse.head? = a.data.get? (a.size - 1)

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.data.reverse.head? = a.data.get? (a.size - 1)
Tactic:
simp [List.length_eq_zero.mp h]
State after:
no goals

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.toListRev.head? = a.back?
Tactic:
rw [← List.get?_zero, get?_toListRev _ _ h, Nat.sub_zero]
State after:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.get? (a.size - 1) = a.back?

State before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.get? (a.size - 1) = a.back?
Tactic:
rfl
State after:
no goals