Theorem: SizedArray.back_eq_back'_val (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ back x = Array.back' x.val (_ : Array.size x.val > 0)
Tactic:
dsimp [back, Array.back']
State after:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[Array.size x.val - 1]

State before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[Array.size x.val - 1]
Tactic:
simp only [x.size_eq]
State after:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[n + 1 - 1]

State before:
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[n + 1 - 1]
Tactic:
rfl
State after:
no goals