case mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) j = get { val := val✝, property := property✝ } j
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ get (set v i a) j = get v j
cases v
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
j : Fin n
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝, isLt := isLt✝ } ≠ j
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) j =
    get { val := val✝¹, property := property✝ } j
case mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) j = get { val := val✝, property := property✝ } j
cases i
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ get (set { val := val✝², property := property✝ } { val := val✝¹, isLt := isLt✝¹ } a) { val := val✝, isLt := isLt✝ } =
    get { val := val✝², property := property✝ } { val := val✝, isLt := isLt✝ }
case mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
j : Fin n
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝, isLt := isLt✝ } ≠ j
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) j =
    get { val := val✝¹, property := property✝ } j
cases j
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ 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✝ }) =
    List.get val✝²
      (↑(Fin.cast (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ get (set { val := val✝², property := property✝ } { val := val✝¹, isLt := isLt✝¹ } a) { val := val✝, isLt := isLt✝ } =
    get { val := val✝², property := property✝ } { val := val✝, isLt := isLt✝ }
simp [Vector.set, Vector.get_eq_get, List.get_set_of_ne (Fin.vne_of_ne h)]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get val✝²
      {
        val :=
          ↑(↑(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✝ }),
        isLt :=
          (_ :
            ↑(↑(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✝ }) <
              List.length val✝²) } =
    List.get val✝²
      (↑(Fin.cast (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })

case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(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✝ })
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ 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✝ }) =
    List.get val✝²
      (↑(Fin.cast (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
rw [List.get_set_of_ne]
case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(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✝ })
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get val✝²
      {
        val :=
          ↑(↑(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✝ }),
        isLt :=
          (_ :
            ↑(↑(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✝ }) <
              List.length val✝²) } =
    List.get val✝²
      (↑(Fin.cast (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })

case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(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✝ })
. rfl
no goals
case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(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✝ })
. simpa using h
no goals
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get val✝²
      {
        val :=
          ↑(↑(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✝ }),
        isLt :=
          (_ :
            ↑(↑(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✝ }) <
              List.length val✝²) } =
    List.get val✝²
      (↑(Fin.cast (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
rfl
no goals
case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type ?u.58625
γ : Type ?u.58628
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(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✝ })
simpa using h