case mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
i : Fin n
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) i = a
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
v : Vector α n
i : Fin n
a : α
⊢ get (set v i a) i = a
cases v
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) { val := val✝, isLt := isLt✝ } = a
case mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
i : Fin n
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) i = a
cases i
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.cast
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝¹ val✝ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝¹, property := property✝ }) (↑{ val := val✝, isLt := isLt✝ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    a
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) { val := val✝, isLt := isLt✝ } = a
simp [Vector.set, get_eq_get]
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.cast (_ : n = List.length (List.set val✝¹ val✝ a))) { val := val✝, isLt := isLt✝ }) =
    a
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.cast
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝¹ val✝ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝¹, property := property✝ }) (↑{ val := val✝, isLt := isLt✝ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    a
dsimp
no goals
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.57781
γ : Type ?u.57784
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.cast (_ : n = List.length (List.set val✝¹ val✝ a))) { val := val✝, isLt := isLt✝ }) =
    a
exact List.get_set_eq _ _ _ _