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) → α
val✝ : ℕ
isLt✝ : val✝ < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (↑Fin.castSucc (↑(Fin.natAdd m) { val := val✝, isLt := isLt✝ })) =
    b (↑Fin.castSucc { val := val✝, isLt := isLt✝ })
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.castSucc (↑(Fin.natAdd m) i)) =
    b (↑Fin.castSucc i)
cases i
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) → α
val✝ : ℕ
isLt✝ : val✝ < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (↑Fin.castSucc (↑(Fin.natAdd m) { val := val✝, isLt := isLt✝ })) =
    b (↑Fin.castSucc { val := val✝, isLt := isLt✝ })
simp only [Matrix.vecAppend_eq_ite, Nat.not_lt_zero, Fin.natAdd_mk, add_lt_iff_neg_left,
  add_tsub_cancel_left, dif_neg, Fin.castSucc_mk, not_false_iff, Fin.val_mk]