n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑(insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl })) =
    ↑(insertNth a (↑Fin.castSucc i) (insertNth b j { val := l, property := hl }))
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl }) =
    insertNth a (↑Fin.castSucc i) (insertNth b j { val := l, property := hl })
refine' Subtype.eq _
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ List.insertNth (↑j + 1) b (List.insertNth (↑i) a l) = List.insertNth (↑i) a (List.insertNth (↑j) b l)
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑(insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl })) =
    ↑(insertNth a (↑Fin.castSucc i) (insertNth b j { val := l, property := hl }))
simp only [insertNth_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑i ≤ ↑j

case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ List.length l
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ List.insertNth (↑j + 1) b (List.insertNth (↑i) a l) = List.insertNth (↑i) a (List.insertNth (↑j) b l)
apply List.insertNth_comm
no goals
case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑i ≤ ↑j
assumption
case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ n
case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ List.length l
rw [hl]
no goals
case x
n : ℕ
α : Type u_1
β : Type ?u.56356
γ : Type ?u.56359
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ n
exact Nat.le_of_succ_le_succ j.2