case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : ℕ
hi : i < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (Fin.succ (↑(Fin.natAdd m) { val := i, isLt := hi })) =
    b (Fin.succ { val := i, isLt := hi })
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : Fin n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b (Fin.succ (↑(Fin.natAdd m) i)) =
    b (Fin.succ i)
cases' i with i hi
no goals
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : ℕ
hi : i < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (Fin.succ (↑(Fin.natAdd m) { val := i, isLt := hi })) =
    b (Fin.succ { val := i, isLt := hi })
simp only [Matrix.vecAppend_eq_ite, add_assoc, Nat.not_lt_zero, Fin.natAdd_mk,
  add_lt_iff_neg_left, add_tsub_cancel_left, Fin.succ_mk, dif_neg, not_false_iff, Fin.val_mk]