Theorem: List.get_Array_data (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
x : Array ?m.919
i : Fin x.data.length
⊢ x.data.length = x.size
Tactic:
simp
State after:
no goals

State before:
α✝ : Type u_1
x : Array α✝
i : Fin x.data.length
⊢ x.data.get i = x.get (Fin.cast ⋯ i)
Tactic:
rfl
State after:
no goals