case mk
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : ℕ
hi : i < m
⊢ addCases hleft hright (↑(castAdd n) { val := i, isLt := hi }) = hleft { val := i, isLt := hi }
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin m
⊢ addCases hleft hright (↑(castAdd n) i) = hleft i
cases' i with i hi
case mk
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : ℕ
hi : i < m
⊢ (_ :
        ↑(castAdd n)
            (castLT (↑(castAdd n) { val := i, isLt := hi }) (_ : ↑(↑(castAdd n) { val := i, isLt := hi }) < m)) =
          ↑(castAdd n) { val := i, isLt := hi }) ▸
      hleft (castLT (↑(castAdd n) { val := i, isLt := hi }) (_ : ↑(↑(castAdd n) { val := i, isLt := hi }) < m)) =
    hleft { val := i, isLt := hi }
case mk
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : ℕ
hi : i < m
⊢ addCases hleft hright (↑(castAdd n) { val := i, isLt := hi }) = hleft { val := i, isLt := hi }
rw [addCases, dif_pos (castAdd_lt _ _)]
no goals
case mk
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : ℕ
hi : i < m
⊢ (_ :
        ↑(castAdd n)
            (castLT (↑(castAdd n) { val := i, isLt := hi }) (_ : ↑(↑(castAdd n) { val := i, isLt := hi }) < m)) =
          ↑(castAdd n) { val := i, isLt := hi }) ▸
      hleft (castLT (↑(castAdd n) { val := i, isLt := hi }) (_ : ↑(↑(castAdd n) { val := i, isLt := hi }) < m)) =
    hleft { val := i, isLt := hi }
rfl