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) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (Fin.succ (↑(Fin.castAdd n) { val := i, isLt := hi })) =
    a (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 m
h : a (Fin.last m) = b 0
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b (Fin.succ (↑(Fin.castAdd n) i)) =
    a (Fin.succ i)
cases' i with i hi
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) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ (if h : i + 1 < m then a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) }
    else
      b
        { val := i + 1 - m,
          isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) }) =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
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) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ ↑Fin.castSucc) b
      (Fin.succ (↑(Fin.castAdd n) { val := i, isLt := hi })) =
    a (Fin.succ { val := i, isLt := hi })
simp only [Matrix.vecAppend_eq_ite, hi, Fin.succ_mk, Function.comp_apply, Fin.castSucc_mk,
  Fin.val_mk, Fin.castAdd_mk]
case mk.inl
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : i + 1 < m
⊢ a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) } = a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }

case mk.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
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) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ (if h : i + 1 < m then a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) }
    else
      b
        { val := i + 1 - m,
          isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) }) =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
split_ifs with h_1
no goals
case mk.inl
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : i + 1 < m
⊢ a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) } = a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
rfl
case mk.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
case mk.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
have : i + 1 = m := le_antisymm hi (le_of_not_gt h_1)
no goals
case mk.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
calc
  b ⟨i + 1 - m, by simp [this]⟩ = b 0 := congr_arg b (by simp [Fin.ext_iff, this])
  _ = a (Fin.last _) := h.symm
  _ = _ := congr_arg a (by simp [Fin.ext_iff, this])
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ i + 1 - m < Nat.succ n
simp [this]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ { val := i + 1 - m, isLt := (_ : i + 1 - m < Nat.succ n) } = 0
simp [Fin.ext_iff, this]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ Fin.last m = { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
simp [Fin.ext_iff, this]