case h.mk
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i => cons a v (↑(finRotate (n + 1)) i)
ext ⟨i, h⟩
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })

case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
case h.mk
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
by_cases h' : i < n
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ _root_.cast (_ : α = α) (v (castLT { val := i, isLt := h } h')) =
    cases a v { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
no goals
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ _root_.cast (_ : α = α) (v (castLT { val := i, isLt := h } h')) =
    cases a v { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
rfl
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
have h'' : n = i := by
  simp only [not_lt] at h'
  exact (Nat.eq_of_le_of_lt_succ h' h).symm
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a { val := n, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := n, isLt := h })
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
subst h''
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ _root_.cast (_ : α = α) a = cases a v { val := 0, isLt := (_ : 0 < Nat.succ n) }
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a { val := n, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := n, isLt := h })
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
no goals
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ _root_.cast (_ : α = α) a = cases a v { val := 0, isLt := (_ : 0 < Nat.succ n) }
rfl
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i
simp only [not_lt] at h'
no goals
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i
exact (Nat.eq_of_le_of_lt_succ h' h).symm